[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/hw/formal/formal_conn.sh b/hw/formal/formal_conn.sh
index 4fb0e3a..b6a550d 100755
--- a/hw/formal/formal_conn.sh
+++ b/hw/formal/formal_conn.sh
@@ -91,7 +91,7 @@
if [ "${tool}" == "jg" ]; then
jg ${batch} \
- ${REPO_PATH}/hw/formal/tools/jaspergold/fconn.tcl \
+ ${REPO_PATH}/hw/formal/tools/jaspergold/conn.tcl \
-proj {REPO_PATH}/hw/formal/jgproject \
-allow_unsupported_OS \
-command exit \
diff --git a/hw/formal/tools/dvsim/common_conn_cfg.hjson b/hw/formal/tools/dvsim/common_conn_cfg.hjson
index 2d6270b..8379db7 100644
--- a/hw/formal/tools/dvsim/common_conn_cfg.hjson
+++ b/hw/formal/tools/dvsim/common_conn_cfg.hjson
@@ -2,53 +2,18 @@
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
{
- flow: fpv
- sub_flow: fconn
- fpv_root: "{proj_root}/hw/formal"
- flow_makefile: "{fpv_root}/tools/dvsim/fpv.mk"
-
- import_cfgs: [// common server configuration for results upload
- "{proj_root}/hw/data/common_project_cfg.hjson",
- "{fpv_root}/tools/{tool}/{tool}.hjson"]
-
- tool: "jaspergold"
-
- // Default directory structure for the output
- dut: "{name}"
- build_dir: "{scratch_path}/{build_mode}"
-
- // we rely on Fusesoc to generate the filelist for fpv
- sv_flist_gen_cmd: fusesoc
-
- // TODO: switch the tool to formal once the corresponding edalize backend is avaiable
-
- sv_flist_gen_opts: ["--cores-root {proj_root}",
- "run",
- "--flag=fileset_{design_level}",
- "--tool=icarus",
- "--target=default",
- "--build-root={build_dir}",
- "--setup {fusesoc_core}"]
- sv_flist_gen_dir: "{build_dir}/default-icarus"
+ sub_flow: conn
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_formal_cfg.hjson"]
// Vars that need to exported to the env
exports: [
- { TOP: "{dut}" },
- { COV: "{cov}" },
- { CSV_PATH: "{csv_path}"}
+ {CSV_PATH: "{csv_path}"}
]
- report_cmd: "python3 {fpv_root}/tools/{tool}/parse-fpv-report.py"
- // TODO: the output name should be conn.log instead of fpv.log
- report_opts: ["--logpath={build_dir}/fpv.log",
- "--reppath={build_dir}/results.hjson",
- "--cov={cov}",
- "--dut={name}"]
-
// Connectivity test should all be in top_level design
overrides: [
{
- name: design_level
+ name: design_level
value: "top"
}
]
diff --git a/hw/formal/tools/dvsim/common_formal_cfg.hjson b/hw/formal/tools/dvsim/common_formal_cfg.hjson
new file mode 100644
index 0000000..2a2fd12
--- /dev/null
+++ b/hw/formal/tools/dvsim/common_formal_cfg.hjson
@@ -0,0 +1,46 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+{
+ flow: formal
+ formal_root: "{proj_root}/hw/formal"
+ flow_makefile: "{formal_root}/tools/dvsim/formal.mk"
+
+ import_cfgs: [// common server configuration for results upload
+ "{proj_root}/hw/data/common_project_cfg.hjson",
+ "{formal_root}/tools/{tool}/{tool}.hjson"]
+
+ tool: "jaspergold"
+
+ // Default directory structure for the output
+ dut: "{name}"
+ build_dir: "{scratch_path}/{build_mode}"
+
+ // we rely on Fusesoc to generate the filelist for formal
+ sv_flist_gen_cmd: fusesoc
+
+ // TODO: switch the tool to formal once the corresponding edalize backend is avaiable
+
+ sv_flist_gen_opts: ["--cores-root {proj_root}",
+ "run",
+ "--flag=fileset_{design_level}",
+ "--tool=icarus",
+ "--target=default",
+ "--build-root={build_dir}",
+ "--setup {fusesoc_core}"]
+ sv_flist_gen_dir: "{build_dir}/default-icarus"
+
+ report_cmd: "python3 {formal_root}/tools/{tool}/parse-formal-report.py"
+ report_opts: ["--logpath={build_dir}/{sub_flow}.log",
+ "--reppath={build_dir}/results.hjson",
+ "--cov={cov}",
+ "--dut={name}"]
+
+ // Vars that need to exported to the env
+ exports: [
+ { TOP: "{dut}" },
+ { COV: "{cov}" },
+ {sub_flow: "{sub_flow}"}
+ ]
+}
+
diff --git a/hw/formal/tools/dvsim/common_fpv_cfg.hjson b/hw/formal/tools/dvsim/common_fpv_cfg.hjson
index c6ffc55..fbb5c77 100644
--- a/hw/formal/tools/dvsim/common_fpv_cfg.hjson
+++ b/hw/formal/tools/dvsim/common_fpv_cfg.hjson
@@ -2,44 +2,6 @@
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
{
- flow: fpv
- sub_flow: fpv
- fpv_root: "{proj_root}/hw/formal"
- flow_makefile: "{fpv_root}/tools/dvsim/fpv.mk"
-
- import_cfgs: [// common server configuration for results upload
- "{proj_root}/hw/data/common_project_cfg.hjson",
- "{fpv_root}/tools/{tool}/{tool}.hjson"]
-
- tool: "jaspergold"
-
- // Default directory structure for the output
- dut: "{name}"
- build_dir: "{scratch_path}/{build_mode}"
-
- // we rely on Fusesoc to generate the filelist for fpv
- sv_flist_gen_cmd: fusesoc
-
- // TODO: switch the tool to formal once the corresponding edalize backend is avaiable
-
- sv_flist_gen_opts: ["--cores-root {proj_root}",
- "run",
- "--flag=fileset_{design_level}",
- "--tool=icarus",
- "--target=formal",
- "--build-root={build_dir}",
- "--setup {fusesoc_core}"]
- sv_flist_gen_dir: "{build_dir}/formal-icarus"
-
- // Vars that need to exported to the env
- exports: [
- { FPV_TOP: "{dut}" },
- { COV: "{cov}" }
- ]
-
- report_cmd: "python3 {fpv_root}/tools/{tool}/parse-fpv-report.py"
- report_opts: ["--logpath={build_dir}/fpv.log",
- "--reppath={build_dir}/results.hjson",
- "--cov={cov}",
- "--dut={name}"]
+ sub_flow: "fpv"
+ import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_formal_cfg.hjson"]
}
diff --git a/hw/formal/tools/dvsim/fpv.mk b/hw/formal/tools/dvsim/formal.mk
similarity index 96%
rename from hw/formal/tools/dvsim/fpv.mk
rename to hw/formal/tools/dvsim/formal.mk
index acf93b3..1f19882 100644
--- a/hw/formal/tools/dvsim/fpv.mk
+++ b/hw/formal/tools/dvsim/formal.mk
@@ -25,7 +25,7 @@
do_build: pre_build
@echo "[make]: do_build"
- cd ${sv_flist_gen_dir} && ${build_cmd} ${build_opts} 2>&1 | tee ${build_dir}/fpv.log
+ cd ${sv_flist_gen_dir} && ${build_cmd} ${build_opts} 2>&1 | tee ${build_dir}/${sub_flow}.log
post_build: do_build
@echo "[make]: post_build"
diff --git a/hw/formal/tools/jaspergold/fconn.tcl b/hw/formal/tools/jaspergold/conn.tcl
similarity index 100%
rename from hw/formal/tools/jaspergold/fconn.tcl
rename to hw/formal/tools/jaspergold/conn.tcl
diff --git a/hw/formal/tools/jaspergold/jaspergold.hjson b/hw/formal/tools/jaspergold/jaspergold.hjson
index 058cf05..c2531b3 100644
--- a/hw/formal/tools/jaspergold/jaspergold.hjson
+++ b/hw/formal/tools/jaspergold/jaspergold.hjson
@@ -3,7 +3,7 @@
// SPDX-License-Identifier: Apache-2.0
{
build_cmd: "{job_prefix} jg"
- build_opts: ["-batch {fpv_root}/tools/{tool}/{sub_flow}.tcl",
+ build_opts: ["-batch {formal_root}/tools/{tool}/{sub_flow}.tcl",
"-proj jgproject",
"-allow_unsupported_OS",
"-command exit"]
diff --git a/hw/formal/tools/jaspergold/parse-fpv-report.py b/hw/formal/tools/jaspergold/parse-formal-report.py
similarity index 83%
rename from hw/formal/tools/jaspergold/parse-fpv-report.py
rename to hw/formal/tools/jaspergold/parse-formal-report.py
index a1a1a76..a8832f6 100644
--- a/hw/formal/tools/jaspergold/parse-fpv-report.py
+++ b/hw/formal/tools/jaspergold/parse-formal-report.py
@@ -50,7 +50,7 @@
return '{0:.2f} %'.format(round(pc, 2))
-def parse_fpv_message(str_buffer):
+def parse_message(str_buffer):
'''Parse error, warnings, and failed properties from the log file'''
err_warn_patterns = [("errors", r"^ERROR: .*"),
("errors", r"^\[ERROR.*"),
@@ -62,7 +62,7 @@
return extract_messages(str_buffer, err_warn_patterns)
-def parse_fpv_summary(str_buffer):
+def get_summary(str_buffer):
'''Count errors, warnings, and property status from the log file'''
message_patterns = [("errors", r"^ERROR: .*"),
("errors", r"^\[ERROR.*"),
@@ -73,25 +73,25 @@
("covered", r"^\[\d+\].*covered.*"),
("undetermined", r"^\[\d+\].*undetermined.*"),
("unreachable", r"^\[\d+\].*unreachable.*")]
- fpv_summary = extract_messages_count(str_buffer, message_patterns)
+ summary = extract_messages_count(str_buffer, message_patterns)
- fpv_summary["pass_rate"] = format_percentage(fpv_summary["proven"],
- fpv_summary["cex"] + fpv_summary["undetermined"])
- fpv_summary["cov_rate"] = format_percentage(fpv_summary["covered"], fpv_summary["unreachable"])
+ summary["pass_rate"] = format_percentage(summary["proven"],
+ summary["cex"] + summary["undetermined"])
+ summary["cov_rate"] = format_percentage(summary["covered"], summary["unreachable"])
- return fpv_summary
+ return summary
def get_results(logpath):
- '''Parse FPV log file and extract info to a dictionary'''
+ '''Parse log file and extract info to a dictionary'''
try:
with Path(logpath).open() as f:
results = OrderedDict()
full_file = f.read()
- results["messages"] = parse_fpv_message(full_file)
- fpv_summary = parse_fpv_summary(full_file)
- if fpv_summary:
- results["fpv_summary"] = fpv_summary
+ results["messages"] = parse_message(full_file)
+ summary = get_summary(full_file)
+ if summary:
+ results["summary"] = summary
return results
except IOError as err:
@@ -103,7 +103,7 @@
def get_cov_results(logpath, dut_name):
- '''Parse FPV coverage information from the log file'''
+ '''Parse coverage information from the log file'''
try:
with Path(logpath).open() as f:
full_file = f.read()
@@ -131,7 +131,7 @@
def main():
parser = argparse.ArgumentParser(
description=
- '''This script parses the JasperGold FPV log to extract below information.
+ '''This script parses the JasperGold formal log to extract below information.
"messages": {
"errors" : []
@@ -140,7 +140,7 @@
"undetermined": [],
"unreachable" : [],
},
- "fpv_summary": {
+ "summary": {
"errors" : 0
"warnings" : 2
"proven" : 20,
@@ -152,7 +152,7 @@
"cover_rate" : "90 %"
},
If coverage is enabled, this script will also parse the coverage result:
- "fpv_coverage": {
+ "coverage": {
stimuli: "90 %",
coi : "90 %",
proof : "80 %"
@@ -164,9 +164,7 @@
''')
parser.add_argument('--logpath',
type=str,
- default="fpv.log",
- help=('FPV log file path. Defaults to `fpv.log` '
- 'under the current script directory.'))
+ help=('The path of the formal log file that will be parsed.'))
parser.add_argument('--reppath',
type=str,
@@ -190,7 +188,7 @@
results = get_results(args.logpath)
if args.cov:
- results["fpv_coverage"] = get_cov_results(args.logpath, args.dut)
+ results["coverage"] = get_cov_results(args.logpath, args.dut)
with Path(args.reppath).open("w") as results_file:
hjson.dump(results,
@@ -200,16 +198,16 @@
use_decimal=True)
# return nonzero status if any errors or property failures are present
- # TODO: currently allow FPV warnings
+ # TODO: currently allow warnings
err_msgs = results["messages"]
n_errors = len(err_msgs["errors"])
n_failures = (len(err_msgs.get("cex")) + len(err_msgs.get("undetermined")) +
len(err_msgs.get("unreachable")))
if n_errors > 0 or n_failures > 0:
- log.info("Found %d FPV errors, %d FPV property failures", n_errors, n_failures)
+ log.info("Found %d errors, %d failures", n_errors, n_failures)
return 1
- log.info("FPV logfile parsed succesfully")
+ log.info("Formal logfile parsed succesfully")
return 0
diff --git a/hw/top_earlgrey/fpv/chip_fconn_cfg.hjson b/hw/top_earlgrey/formal/chip_fconn_cfg.hjson
similarity index 83%
rename from hw/top_earlgrey/fpv/chip_fconn_cfg.hjson
rename to hw/top_earlgrey/formal/chip_fconn_cfg.hjson
index 82e1045..94085a9 100644
--- a/hw/top_earlgrey/fpv/chip_fconn_cfg.hjson
+++ b/hw/top_earlgrey/formal/chip_fconn_cfg.hjson
@@ -9,7 +9,7 @@
fusesoc_core: lowrisc:systems:top_earlgrey
- csv_path: "{proj_root}/hw/top_earlgrey/fpv/fconn_csvs/top_earlgrey_conn.csv"
+ csv_path: "{proj_root}/hw/top_earlgrey/formal/fconn_csvs/top_earlgrey_conn.csv"
// TODO: reduce run time and turn on coverage
cov: false
diff --git a/hw/top_earlgrey/fpv/fconn_csvs/top_earlgrey_conn.csv b/hw/top_earlgrey/formal/fconn_csvs/top_earlgrey_conn.csv
similarity index 100%
rename from hw/top_earlgrey/fpv/fconn_csvs/top_earlgrey_conn.csv
rename to hw/top_earlgrey/formal/fconn_csvs/top_earlgrey_conn.csv
diff --git a/hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson b/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson
similarity index 100%
rename from hw/top_earlgrey/fpv/top_earlgrey_fpv_cfgs.hjson
rename to hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson
diff --git a/util/dvsim/CfgFactory.py b/util/dvsim/CfgFactory.py
index a258985..2064fbb 100644
--- a/util/dvsim/CfgFactory.py
+++ b/util/dvsim/CfgFactory.py
@@ -7,7 +7,7 @@
from CfgJson import load_hjson
-import FpvCfg
+import FormalCfg
import LintCfg
import SimCfg
import SynCfg
@@ -36,7 +36,7 @@
classes = [
LintCfg.LintCfg,
SynCfg.SynCfg,
- FpvCfg.FpvCfg,
+ FormalCfg.FormalCfg,
SimCfg.SimCfg
]
found_cls = None
diff --git a/util/dvsim/FpvCfg.py b/util/dvsim/FormalCfg.py
similarity index 78%
rename from util/dvsim/FpvCfg.py
rename to util/dvsim/FormalCfg.py
index c191abf..2a80fa6 100644
--- a/util/dvsim/FpvCfg.py
+++ b/util/dvsim/FormalCfg.py
@@ -12,18 +12,18 @@
from utils import VERBOSE, subst_wildcards
-class FpvCfg(OneShotCfg):
- """Derivative class for FPV purposes.
+class FormalCfg(OneShotCfg):
+ """Derivative class for running formal tools.
"""
- flow = 'fpv'
+ 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() + " FPV Results"
+ 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.
@@ -59,61 +59,61 @@
output_str += "\n```\n"
return output_str
- def get_fpv_summary_results(self, result):
+ def get_summary(self, result):
summary = []
- fpv_summary = result.get("fpv_summary")
- if fpv_summary is None:
- results_str = "No fpv_summary found\n"
+ 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(fpv_summary["errors"]) + " E ",
- str(fpv_summary["warnings"]) + " W ",
- str(fpv_summary["proven"]) + " G ",
- str(fpv_summary["cex"]) + " E ",
- str(fpv_summary["undetermined"]) + " W ",
- str(fpv_summary["covered"]) + " G ",
- str(fpv_summary["unreachable"]) + " E ",
- fpv_summary["pass_rate"],
- fpv_summary["cov_rate"]
+ 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(fpv_summary["pass_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 fpv_summary\n"
+ results_str = "No content in summary\n"
summary.append("N/A")
return results_str, summary
- def get_fpv_coverage_results(self, result):
+ def get_coverage(self, result):
summary = []
- fpv_coverage = result.get("fpv_coverage")
- if fpv_coverage is None:
- results_str = "No fpv_coverage found\n"
+ 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([
- fpv_coverage["stimuli"],
- fpv_coverage["coi"],
- fpv_coverage["proof"]
+ formal_coverage["stimuli"],
+ formal_coverage["coi"],
+ formal_coverage["proof"]
])
- summary.append(fpv_coverage["stimuli"])
- summary.append(fpv_coverage["coi"])
- summary.append(fpv_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 fpv_coverage\n"
+ results_str = "No content in formal_coverage\n"
summary = ["N/A", "N/A", "N/A"]
return results_str, summary
@@ -122,7 +122,7 @@
# 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 summary of FPV results")
+ log.info("Create a result summary")
results_str = "## " + self.results_title + " (Summary)\n\n"
results_str += "### " + self.timestamp_long + "\n"
@@ -153,7 +153,7 @@
error_message = ""
for cfg in self.cfgs:
- email_result = cfg.result.get("fpv_summary")
+ email_result = cfg.result.get("summary")
if email_result is not None:
email_table.append([
cfg.name,
@@ -169,9 +169,9 @@
])
messages = cfg.result.get("messages")
if messages is not None:
- # TODO: temp disable printing out "fpv_warnings" in results_summary
- # Will clean up FPV warnings first, then display "fpv_warnings"
- error = self.parse_dict_to_str(messages, ["fpv_warnings"])
+ # 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
@@ -185,7 +185,7 @@
def _gen_results(self, results):
# This function is called after the regression and looks for
- # results.hjson file with aggregated results from the FPV run.
+ # results.hjson file with aggregated results from the formal logfile.
# The hjson file is required to follow this format:
# {
# "messages": {
@@ -196,7 +196,7 @@
# "unreachable" : [],
# },
#
- # "fpv_summary": {
+ # "summary": {
# "errors" : 0
# "warnings" : 2
# "proven" : 20,
@@ -212,8 +212,8 @@
# covered, and unreachable.
#
# If coverage was enabled then results.hjson will also have an item that
- # shows FPV coverage. It will have the following format:
- # "fpv_coverage": {
+ # shows formal coverage. It will have the following format:
+ # "coverage": {
# stimuli: "90 %",
# coi : "90 %",
# proof : "80 %"
@@ -223,14 +223,14 @@
if self.revision:
results_str += "### " + self.revision + "\n"
results_str += "### Branch: " + self.branch + "\n"
- results_str += "### FPV Tool: " + self.tool.upper() + "\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("FPV only supports mode 'default', but found these modes: %s", mode_names)
+ 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}) +
@@ -246,15 +246,15 @@
}
}
- fpv_result_str, fpv_summary = self.get_fpv_summary_results(self.result)
- results_str += fpv_result_str
- summary += fpv_summary
+ 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_fpv_coverage_results(self.result)
+ cov_result_str, cov_summary = self.get_coverage(self.result)
results_str += cov_result_str
summary += cov_summary
@@ -277,9 +277,9 @@
return self.results_md
def _publish_results(self):
- '''This does nothing: detailed messages from FPV runs are not published
+ '''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), but not anything more detailed.
+ results (as in gen_results_summary).
'''
return
