[formal/conn] Support dvsim to publish regression result summary This PR adds following support: 1. Add sub-flow to output path to better distinguish different formal sub-flows. 2. Add a switch `publish_child_cfg_result` to publish result summary when not running from batch cfgs (thus no result summary). 3. Add a URL path to top-level connectivity test dashboard. Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/_index.md b/hw/_index.md index cc6d88f..057d383 100644 --- a/hw/_index.md +++ b/hw/_index.md
@@ -43,7 +43,7 @@ * [Design specification]({{< relref "hw/top_earlgrey/doc" >}}) * [dv document]({{< relref "hw/top_earlgrey/doc/dv" >}}) * [DV simulation results, with coverage (nightly)](https://reports.opentitan.org/hw/top_earlgrey/dv/latest/results.html) - * FPV results (nightly) (TBD) + * [Connectivity results (nightly)](https://reports.opentitan.org/hw/top_earlgrey/conn/jaspergold/latest/results.html) * [AscentLint results (nightly)](https://reports.opentitan.org/hw/top_earlgrey/lint/ascentlint/latest/results.html) * [Verilator lint results (nightly)](https://reports.opentitan.org/hw/top_earlgrey/lint/verilator/latest/results.html) * [Style lint results (nightly)](https://reports.opentitan.org/hw/top_earlgrey/lint/veriblelint/latest/results.html)
diff --git a/hw/formal/tools/dvsim/common_formal_cfg.hjson b/hw/formal/tools/dvsim/common_formal_cfg.hjson index e4f899a..3d446fc 100644 --- a/hw/formal/tools/dvsim/common_formal_cfg.hjson +++ b/hw/formal/tools/dvsim/common_formal_cfg.hjson
@@ -48,4 +48,12 @@ { COV: "{cov}" }, { sub_flow: "{sub_flow}"} ] + + overrides: [ + // Add formal sub_flow to the scratch path + { + name: scratch_path + value: "{scratch_base_path}/{dut}-{flow}-{sub_flow}-{tool}" + } + ] }
diff --git a/hw/formal/tools/dvsim/common_fpv_cfg.hjson b/hw/formal/tools/dvsim/common_fpv_cfg.hjson index fbb5c77..3b62408 100644 --- a/hw/formal/tools/dvsim/common_fpv_cfg.hjson +++ b/hw/formal/tools/dvsim/common_fpv_cfg.hjson
@@ -2,6 +2,6 @@ // Licensed under the Apache License, Version 2.0, see LICENSE for details. // SPDX-License-Identifier: Apache-2.0 { - sub_flow: "fpv" + sub_flow: fpv import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_formal_cfg.hjson"] }
diff --git a/hw/top_earlgrey/formal/chip_conn_cfg.hjson b/hw/top_earlgrey/formal/chip_conn_cfg.hjson index 9abec45..a01226f 100644 --- a/hw/top_earlgrey/formal/chip_conn_cfg.hjson +++ b/hw/top_earlgrey/formal/chip_conn_cfg.hjson
@@ -13,4 +13,8 @@ // TODO: reduce run time and turn on coverage cov: false + + rel_path: "hw/top_earlgrey/{sub_flow}/{tool}" + + publish_report: true }
diff --git a/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson b/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson index 9875b88..6650bff 100644 --- a/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson +++ b/hw/top_earlgrey/formal/top_earlgrey_fpv_cfgs.hjson
@@ -2,8 +2,11 @@ // Licensed under the Apache License, Version 2.0, see LICENSE for details. // SPDX-License-Identifier: Apache-2.0 { + // TODO: flow and sub_flow should not needed here. Update dvsim to support it. flow: formal + sub_flow: fpv + // This is the primary cfg hjson for FPV. It imports ALL individual FPV // cfgs of the IPs and the full chip used in top_earlgrey. This enables to run // them all as a regression in one shot.
diff --git a/util/dvsim/FormalCfg.py b/util/dvsim/FormalCfg.py index 4ce5dbb..a906881 100644 --- a/util/dvsim/FormalCfg.py +++ b/util/dvsim/FormalCfg.py
@@ -22,8 +22,15 @@ super().__init__(flow_cfg_file, hjson_data, args, mk_config) self.header = ["name", "errors", "warnings", "proven", "cex", "undetermined", "covered", "unreachable", "pass_rate", "cov_rate"] + + # Default not to publish child cfg results. + if "publish_report" in hjson_data: + self.publish_report = hjson_data["publish_report"] + else: + self.publish_report = False + self.sub_flow = hjson_data['sub_flow'] self.summary_header = ["name", "pass_rate", "stimuli_cov", "coi_cov", "prove_cov"] - self.results_title = self.name.upper() + " Formal Results" + self.results_title = self.name.upper() + " Formal " + self.sub_flow.upper() + " Results" def parse_dict_to_str(self, input_dict, excl_keys = []): # This is a helper function to parse dictionary items into a string. @@ -242,7 +249,7 @@ } } - results_str += "\n\n## Formal Results\n" + results_str += "\n\n## Formal " + self.sub_flow.upper() + " Results\n" formal_result_str, formal_summary = self.get_summary(self.result) results_str += formal_result_str summary += formal_summary @@ -278,9 +285,16 @@ 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 + ''' our agreement with tool vendors allows us to publish the summary results (as in gen_results_summary). + + In default this method does nothing: detailed messages from each child + cfg will not be published. + If the publish_report argument is set to true, this method will only + publish a result summary of the child cfg. ''' - return + if self.publish_report: + self.publish_results_md = self.gen_results_summary() + super()._publish_results() + else: + return