[formal/script] Update generic formal flow naming from `fpv` to `formal`
This PR updates formal flow names. In current repo, all formal related
generic flow is called `fpv` instead of `flow`.
But as Sri suggested in PR #5770, the generic flow name should be
`formal`, and under formal we can have sub-flows such as `fpv`, `conn`,
`spv`, etc.
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/util/dvsim/FormalCfg.py b/util/dvsim/FormalCfg.py
new file mode 100644
index 0000000..2a80fa6
--- /dev/null
+++ b/util/dvsim/FormalCfg.py
@@ -0,0 +1,285 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+import logging as log
+from pathlib import Path
+
+import hjson
+from tabulate import tabulate
+
+from OneShotCfg import OneShotCfg
+from utils import VERBOSE, subst_wildcards
+
+
+class FormalCfg(OneShotCfg):
+ """Derivative class for running formal tools.
+ """
+
+ flow = 'formal'
+
+ def __init__(self, flow_cfg_file, hjson_data, args, mk_config):
+ super().__init__(flow_cfg_file, hjson_data, args, mk_config)
+ self.header = ["name", "errors", "warnings", "proven", "cex", "undetermined",
+ "covered", "unreachable", "pass_rate", "cov_rate"]
+ self.summary_header = ["name", "pass_rate", "stimuli_cov", "coi_cov", "prove_cov"]
+ self.results_title = self.name.upper() + " Formal Results"
+
+ def parse_dict_to_str(self, input_dict, excl_keys = []):
+ # This is a helper function to parse dictionary items into a string.
+ # This function has an optional input "excl_keys" for user to exclude
+ # printing out certain items according to their keys.
+ # Note this function did not sort the input dictionary's key value
+ # before printing the keys and items. If input dictionary is not an
+ # OrderedDictionary, print out key order is not predictable.
+ # This function works for Hjson lib outputs because the lib uses an
+ # OrderDict when it reads dictionaries.
+ # Example Input:
+ # {
+ # "unreachable": ["prop1, prop2, prop3"],
+ # "cex" : ["prop1"],
+ # }
+ # Example Output:
+ # string = "unreachable:
+ # ```
+ # prop1
+ # prop2
+ # prop3
+ # ```
+ # cex:
+ # ```
+ # prop1
+ # ```"
+ output_str = ""
+ for key, item in input_dict.items():
+ if (key not in excl_keys) and item:
+ output_str += "\n" + key + ":\n"
+ output_str += "```\n"
+ output_str += "\n".join(item)
+ output_str += "\n```\n"
+ return output_str
+
+ def get_summary(self, result):
+ summary = []
+ formal_summary = result.get("summary")
+ if formal_summary is None:
+ results_str = "No summary information found\n"
+ summary.append("N/A")
+ else:
+ colalign = ("center", ) * len(self.header)
+ table = [self.header]
+ table.append([
+ self.name,
+ str(formal_summary["errors"]) + " E ",
+ str(formal_summary["warnings"]) + " W ",
+ str(formal_summary["proven"]) + " G ",
+ str(formal_summary["cex"]) + " E ",
+ str(formal_summary["undetermined"]) + " W ",
+ str(formal_summary["covered"]) + " G ",
+ str(formal_summary["unreachable"]) + " E ",
+ formal_summary["pass_rate"],
+ formal_summary["cov_rate"]
+ ])
+ summary.append(formal_summary["pass_rate"])
+ if len(table) > 1:
+ results_str = tabulate(table, headers="firstrow", tablefmt="pipe",
+ colalign=colalign)
+ else:
+ results_str = "No content in summary\n"
+ summary.append("N/A")
+ return results_str, summary
+
+ def get_coverage(self, result):
+ summary = []
+ formal_coverage = result.get("coverage")
+ if formal_coverage is None:
+ results_str = "No coverage information found\n"
+ summary = ["N/A", "N/A", "N/A"]
+ else:
+ cov_header = ["stimuli", "coi", "proof"]
+ cov_colalign = ("center", ) * len(cov_header)
+ cov_table = [cov_header]
+ cov_table.append([
+ formal_coverage["stimuli"],
+ formal_coverage["coi"],
+ formal_coverage["proof"]
+ ])
+ summary.append(formal_coverage["stimuli"])
+ summary.append(formal_coverage["coi"])
+ summary.append(formal_coverage["proof"])
+
+ if len(cov_table) > 1:
+ results_str = tabulate(cov_table, headers="firstrow",
+ tablefmt="pipe", colalign=cov_colalign)
+
+ else:
+ results_str = "No content in formal_coverage\n"
+ summary = ["N/A", "N/A", "N/A"]
+ return results_str, summary
+
+ def gen_results_summary(self):
+ # Gathers the aggregated results from all sub configs
+ # The results_summary will only contain the passing rate and
+ # percentages of the stimuli, coi, and proven coverage
+ # The email_summary will contain all the information from results_md
+ log.info("Create a result summary")
+
+ results_str = "## " + self.results_title + " (Summary)\n\n"
+ results_str += "### " + self.timestamp_long + "\n"
+ if self.revision:
+ results_str += "### " + self.revision + "\n"
+ results_str += "### Branch: " + self.branch + "\n"
+ results_str += "\n"
+
+ colalign = ("center", ) * len(self.summary_header)
+ table = [self.summary_header]
+ for cfg in self.cfgs:
+ try:
+ table.append(cfg.result_summary[cfg.name])
+ except KeyError as e:
+ table.append([cfg.name, "ERROR", "N/A", "N/A", "N/A"])
+ log.error("cfg: %s could not find generated results_summary: %s", cfg.name, e)
+ if len(table) > 1:
+ self.results_summary_md = results_str + tabulate(
+ table, headers="firstrow", tablefmt="pipe", colalign=colalign)
+ else:
+ self.results_summary_md = results_str
+
+ log.info("[result summary]: %s", self.results_summary_md)
+
+ # Generate email results summary
+ colalign = ("left", ) + ("center", ) * (len(self.header) - 1)
+ email_table = [self.header]
+ error_message = ""
+
+ for cfg in self.cfgs:
+ email_result = cfg.result.get("summary")
+ if email_result is not None:
+ email_table.append([
+ cfg.name,
+ str(email_result["errors"]) + " E ",
+ str(email_result["warnings"]) + " W ",
+ str(email_result["proven"]) + " G ",
+ str(email_result["cex"]) + " E ",
+ str(email_result["undetermined"]) + " W ",
+ str(email_result["covered"]) + " G ",
+ str(email_result["unreachable"]) + " E ",
+ email_result["pass_rate"],
+ email_result["cov_rate"]
+ ])
+ messages = cfg.result.get("messages")
+ if messages is not None:
+ # TODO: temp disable printing out warnings in results_summary
+ # Will clean up formal warnings first, then display warnings
+ error = self.parse_dict_to_str(messages, ["warnings"])
+ if error:
+ error_message += "\n#### " + cfg.name + "\n"
+ error_message += error
+
+ if len(email_table) > 1:
+ self.email_summary_md = results_str + tabulate(
+ email_table, headers="firstrow", tablefmt="pipe", colalign=colalign)
+ self.email_summary_md += error_message
+
+ return self.results_summary_md
+
+ def _gen_results(self, results):
+ # This function is called after the regression and looks for
+ # results.hjson file with aggregated results from the formal logfile.
+ # The hjson file is required to follow this format:
+ # {
+ # "messages": {
+ # "errors" : []
+ # "warnings" : []
+ # "cex" : ["property1", "property2"...],
+ # "undetermined": [],
+ # "unreachable" : [],
+ # },
+ #
+ # "summary": {
+ # "errors" : 0
+ # "warnings" : 2
+ # "proven" : 20,
+ # "cex" : 5,
+ # "covered" : 18,
+ # "undetermined": 7,
+ # "unreachable" : 2,
+ # "pass_rate" : "90 %",
+ # "cover_rate" : "90 %"
+ # },
+ # }
+ # The categories for property results are: proven, cex, undetermined,
+ # covered, and unreachable.
+ #
+ # If coverage was enabled then results.hjson will also have an item that
+ # shows formal coverage. It will have the following format:
+ # "coverage": {
+ # stimuli: "90 %",
+ # coi : "90 %",
+ # proof : "80 %"
+ # }
+ results_str = "## " + self.results_title + "\n\n"
+ results_str += "### " + self.timestamp_long + "\n"
+ if self.revision:
+ results_str += "### " + self.revision + "\n"
+ results_str += "### Branch: " + self.branch + "\n"
+ results_str += "### Formal Tool: " + self.tool.upper() + "\n"
+ results_str += "### LogFile dir: " + self.scratch_path + "/default\n\n"
+
+ summary = [self.name] # cfg summary for publish results
+
+ if len(self.build_modes) != 1:
+ mode_names = [mode.name for mode in self.build_modes]
+ log.error("Formal only supports mode 'default', but found these modes: %s", mode_names)
+ else:
+ mode = self.build_modes[0]
+ result_data = Path(subst_wildcards(self.build_dir, {"build_mode": mode.name}) +
+ '/results.hjson')
+ try:
+ with open(result_data, "r") as results_file:
+ self.result = hjson.load(results_file, use_decimal=True)
+ except IOError as err:
+ log.warning("%s", err)
+ self.result = {
+ "messages": {
+ "errors": ["IOError: %s" % err],
+ }
+ }
+
+ formal_result_str, formal_summary = self.get_summary(self.result)
+ results_str += formal_result_str
+ summary += formal_summary
+
+ if self.cov:
+ results_str += "\n\n## Coverage Results\n"
+ results_str += ("### Coverage html file dir: " +
+ self.scratch_path + "/default/formal-icarus\n\n")
+ cov_result_str, cov_summary = self.get_coverage(self.result)
+ results_str += cov_result_str
+ summary += cov_summary
+
+ messages = self.result.get("messages")
+ if messages is not None:
+ results_str += self.parse_dict_to_str(messages)
+
+ # Write results to the scratch area
+ self.results_md = results_str
+ results_file = self.scratch_path + "/results_" + self.timestamp + ".md"
+ with open(results_file, 'w') as f:
+ f.write(self.results_md)
+
+ # Generate result summary
+ if not self.cov:
+ summary += ["N/A", "N/A", "N/A"]
+ self.result_summary[self.name] = summary
+
+ log.log(VERBOSE, "[results page]: [%s] [%s]", self.name, results_file)
+ return self.results_md
+
+ def _publish_results(self):
+ '''This does nothing: detailed messages from the logfile are not published
+
+ Our agreement with tool vendors allows us to publish the summary
+ results (as in gen_results_summary).
+ '''
+ return
