diff --git a/src/dvsim/flow/formal.py b/src/dvsim/flow/formal.py index 71677596..2b624ed8 100644 --- a/src/dvsim/flow/formal.py +++ b/src/dvsim/flow/formal.py @@ -4,6 +4,7 @@ from collections.abc import Sequence from pathlib import Path +from typing import cast import hjson from tabulate import tabulate @@ -41,6 +42,10 @@ def __init__(self, flow_cfg_file, hjson_data, args, mk_config) -> None: # Default not to publish child cfg results. self.publish_report = hjson_data.get("publish_report", False) self.sub_flow = hjson_data["sub_flow"] + # The coverage columns this cfg's tool measured, filled in by get_coverage once a report + # has been read. Empty until then, and on a cfg whose flow collects no coverage at all, + # which is what makes summary_header below the fallback rather than the answer. + self.cov_header: list[str] = [] self.summary_header = ["name", "pass_rate", "formal_cov", "stimuli_cov", "checker_cov"] self.results_title = self.name.upper() + " Formal " + self.sub_flow.upper() + " Results" @@ -123,33 +128,70 @@ def get_coverage(self, result): results_str = "No coverage information found\n" summary = ["N/A", "N/A", "N/A"] else: - cov_header = ["formal", "stimuli", "checker"] + # The columns are whatever the tool's own report parser wrote, not a fixed set. + # A formal engine reports the coverage it measures under its own names: JasperGold + # gives formal, stimuli and checker, VC Formal gives stimuli, coi and proof, and only + # stimuli is common. Naming them here fixed one engine's vocabulary and raised + # KeyError: 'formal' on every VC Formal run with cov: true, after the job had already + # passed and written its results. + cov_header = list(formal_coverage) + if not cov_header: + # A parser that wrote the key and no columns measured nothing, which is the same + # thing to report as no key at all. Falling through instead would tabulate an + # empty table and contribute no cells to a row the summary expects three of. + return "No coverage information found\n", ["N/A", "N/A", "N/A"] + cov_colalign = ("center",) * len(cov_header) - cov_table = [cov_header] - cov_table.append( - [formal_coverage["formal"], formal_coverage["stimuli"], formal_coverage["checker"]], + cov_table = [cov_header, [formal_coverage[name] for name in cov_header]] + summary.extend(formal_coverage[name] for name in cov_header) + # The cross-cfg summary table is one row per cfg under one header, so the columns this + # cfg's tool measured have to reach the primary cfg that renders it. Setting + # self.summary_header would not: get_coverage runs on a child cfg and + # gen_results_summary reads the header off the primary, which no child touches. + self.cov_header = list(cov_header) + results_str = tabulate( + cov_table, + headers="firstrow", + tablefmt="pipe", + colalign=cov_colalign, ) - summary.append(formal_coverage["formal"]) - summary.append(formal_coverage["stimuli"]) - summary.append(formal_coverage["checker"]) + return results_str, summary - if len(cov_table) > 1: - results_str = tabulate( - cov_table, - headers="firstrow", - tablefmt="pipe", - colalign=cov_colalign, - ) + def formal_cfgs(self) -> "Sequence[FormalCfg]": + """Return this cfg's children as the formal cfgs they are. - else: - results_str = "No content in formal_coverage\n" - summary = ["N/A", "N/A", "N/A"] - return results_str, summary + `FlowCfg` types the list for every flow, so the formal-only attributes the two methods + below read off a child are invisible to a type checker without narrowing it here. + """ + return cast("Sequence[FormalCfg]", self.cfgs) + + def resolve_summary_header(self) -> list[str]: + """Return the summary header naming the coverage columns the cfgs actually measured. + + Each cfg's own tool decides what it measures and under what names, and get_coverage + records that on the cfg. One table cannot carry two vocabularies, so cfgs disagreeing is + reported rather than silently resolved in favour of whichever came first: a single `-t` + makes them agree today, and the error is what says so if that ever stops being true. + """ + cfgs = self.formal_cfgs() + measured = {tuple(cfg.cov_header) for cfg in cfgs if cfg.cov_header} + if not measured: + return self.summary_header + if len(measured) > 1: + log.error( + "The cfgs of %s measured different coverage columns, %s, so one summary header " + "cannot name them all. Reporting the columns of %s.", + self.name, + sorted(measured), + cfgs[0].name, + ) + columns = next(iter(measured)) if len(measured) == 1 else tuple(cfgs[0].cov_header) + return ["name", "pass_rate", *(f"{name}_cov" for name in columns)] 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 results_summary will only contain the passing rate and the coverage percentages the + # cfgs' own tool measured, under the names that tool's report parser wrote. results_str = "## " + self.results_title + " (Summary)\n\n" results_str += "### " + self.timestamp_long + "\n" if self.revision: @@ -157,13 +199,17 @@ def gen_results_summary(self): results_str += "### Branch: " + self.branch + "\n" results_str += "\n" + self.summary_header = self.resolve_summary_header() colalign = ("center",) * len(self.summary_header) table = [self.summary_header] - for cfg in self.cfgs: + # One cell per column beyond name, so a missing result stays aligned with a header whose + # width follows the tool rather than being three coverage columns wide by assumption. + missing = ["N/A"] * (len(self.summary_header) - 2) + for cfg in self.formal_cfgs(): try: table.append(cfg.result_summary[cfg.name]) except KeyError as e: - table.append([cfg.name, "ERROR", "N/A", "N/A", "N/A"]) + table.append([cfg.name, "ERROR", *missing]) log.exception("cfg: %s could not find generated results_summary: %s", cfg.name, e) if len(table) > 1: self.results_summary_md = results_str + tabulate( diff --git a/tests/flow/__init__.py b/tests/flow/__init__.py new file mode 100644 index 00000000..3cd84c9d --- /dev/null +++ b/tests/flow/__init__.py @@ -0,0 +1,5 @@ +# Copyright lowRISC contributors (OpenTitan project). +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +"""Tests for the flow configurations.""" diff --git a/tests/flow/test_formal.py b/tests/flow/test_formal.py new file mode 100644 index 00000000..12e7b1f8 --- /dev/null +++ b/tests/flow/test_formal.py @@ -0,0 +1,223 @@ +# Copyright lowRISC contributors (OpenTitan project). +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +"""Test reporting a formal run. + +The two methods under test are exercised on stand-ins rather than on a `FormalCfg`, because +building one needs a config tree, and between them they touch only the handful of attributes the +fakes below carry. The stand-ins borrow the real methods, so what runs is the shipped code. + +The distinction the fakes preserve is the one that matters here: `get_coverage` runs on a child +cfg and `gen_results_summary` on the primary that renders the cross-cfg table. A test that drives +only the child cannot see whether a column name reaches the table at all. +""" + +import logging +from collections.abc import Iterator + +import pytest +from hamcrest import assert_that, contains_string, equal_to, has_length, is_not + +from dvsim.flow.formal import FormalCfg + +__all__ = () + +# The proof-completeness columns each engine measures, under the names its own report parser +# writes. Only stimuli is common, so neither set can stand in for the other. +JASPERGOLD = {"formal": "79.44 %", "stimuli": "96.06 %", "checker": "78.75 %"} +VCFORMAL = {"stimuli": "12.00 %", "coi": "34.00 %", "proof": "56.00 %"} + +# What the VC Formal flow reports today: its fpv.tcl collects nothing, so the parser answers N/A +# under all three of its own column names. Kept distinct from VCFORMAL because all-N/A values +# coincide with the no-coverage fallback and cannot on their own show which branch ran. +VCFORMAL_COLLECTED_NOTHING = {"stimuli": "N/A", "coi": "N/A", "proof": "N/A"} + +FALLBACK_HEADER = ["name", "pass_rate", "formal_cov", "stimuli_cov", "checker_cov"] + + +class FakeChildCfg: + """A child cfg, carrying only what `get_coverage` reads and writes.""" + + get_coverage = FormalCfg.get_coverage + + def __init__(self, name: str = "hmac") -> None: + """Initialise a child cfg as `FormalCfg.__init__` leaves one.""" + self.name = name + self.cov_header: list[str] = [] + self.summary_header = list(FALLBACK_HEADER) + self.result_summary: dict[str, list[str]] = {} + + def report(self, result: dict[str, dict[str, str]]) -> list[str]: + """Read a run's result the way `_gen_results_for_cfg` does, and return the summary row.""" + _, summary = self.get_coverage(result) + self.result_summary[self.name] = [self.name, "89.36 %", *summary] + return summary + + +class FakePrimaryCfg: + """A primary cfg, carrying only what `gen_results_summary` reads.""" + + formal_cfgs = FormalCfg.formal_cfgs + gen_results_summary = FormalCfg.gen_results_summary + resolve_summary_header = FormalCfg.resolve_summary_header + + def __init__(self, cfgs: list[FakeChildCfg]) -> None: + """Initialise a primary cfg over already-reported children.""" + self.name = "top_earlgrey_fpv_ip" + self.cfgs = cfgs + self.summary_header = list(FALLBACK_HEADER) + self.results_title = "TOP_EARLGREY_FPV_IP Formal FPV Results" + self.timestamp_long = "timestamp" + self.revision = "" + self.branch = "master" + self.results_summary_md = "" + + +@pytest.fixture +def dvsim_log(caplog: pytest.LogCaptureFixture) -> Iterator[pytest.LogCaptureFixture]: + """Capture dvsim's own logger, which deliberately does not propagate.""" + logger = logging.getLogger("dvsim") + logger.addHandler(caplog.handler) + caplog.set_level(logging.ERROR, logger="dvsim") + yield caplog + logger.removeHandler(caplog.handler) + + +def reported(*results: dict[str, dict[str, str]]) -> FakePrimaryCfg: + """Return a primary cfg whose children have each reported one run.""" + children = [] + for index, result in enumerate(results): + child = FakeChildCfg(name=f"cfg{index}") + child.report(result) + children.append(child) + return FakePrimaryCfg(children) + + +class TestCoverageColumns: + """Test that a run's own coverage columns are what gets reported.""" + + @staticmethod + @pytest.mark.parametrize( + ("engine", "coverage"), + [("jaspergold", JASPERGOLD), ("vcformal", VCFORMAL)], + ) + def test_reports_the_columns_a_run_measured( + engine: str, + coverage: dict[str, str], + ) -> None: + """Naming the columns in dvsim fixed one engine's vocabulary and raised KeyError.""" + results_str, summary = FakeChildCfg().get_coverage({"coverage": coverage}) + + assert_that(summary, equal_to(list(coverage.values())), engine) + for column in coverage: + assert_that(results_str, contains_string(column), engine) + + @staticmethod + def test_records_the_columns_for_the_table_the_primary_cfg_renders() -> None: + """The child is where the columns are known and the primary is where they are needed.""" + child = FakeChildCfg() + + child.get_coverage({"coverage": VCFORMAL}) + + assert_that(child.cov_header, equal_to(["stimuli", "coi", "proof"])) + + @staticmethod + def test_says_so_when_a_run_measured_no_coverage() -> None: + """A formal flow that collects nothing leaves the key out entirely.""" + results_str, summary = FakeChildCfg().get_coverage({}) + + assert_that(results_str, contains_string("No coverage information found")) + assert_that(summary, equal_to(["N/A", "N/A", "N/A"])) + + @staticmethod + def test_says_so_when_a_run_reported_no_columns() -> None: + """An empty coverage key measured nothing, so it reports as nothing rather than as a row. + + Falling through would tabulate an empty table and contribute no cells at all to a summary + row, leaving it short of the header instead of saying the run collected nothing. + """ + child = FakeChildCfg() + + results_str, summary = child.get_coverage({"coverage": {}}) + + assert_that(results_str, contains_string("No coverage information found")) + assert_that(summary, equal_to(["N/A", "N/A", "N/A"])) + assert_that(child.cov_header, equal_to([])) + + +class TestSummaryTable: + """Test the cross-cfg summary table, which is where a column name is finally read.""" + + @staticmethod + @pytest.mark.parametrize( + ("engine", "coverage", "columns"), + [ + ("jaspergold", JASPERGOLD, ["formal_cov", "stimuli_cov", "checker_cov"]), + ("vcformal", VCFORMAL, ["stimuli_cov", "coi_cov", "proof_cov"]), + ( + "vcformal collecting nothing", + VCFORMAL_COLLECTED_NOTHING, + ["stimuli_cov", "coi_cov", "proof_cov"], + ), + ], + ) + def test_names_the_columns_the_cfgs_tool_measured( + engine: str, + coverage: dict[str, str], + columns: list[str], + ) -> None: + """Recording the header on the child alone left this table naming another engine's columns. + + `get_coverage` runs on the child and this table is rendered by the primary, so a header + set on the child never reached it and VC Formal's stimuli, coi and proof figures were + printed under JasperGold's formal, stimuli and checker headings. Both engines report three + columns, so nothing misaligned and nothing failed. + """ + primary = reported({"coverage": coverage}) + + table = primary.gen_results_summary() + + assert_that(primary.summary_header, equal_to(["name", "pass_rate", *columns]), engine) + for value in coverage.values(): + assert_that(table, contains_string(value), engine) + + @staticmethod + def test_keeps_the_fallback_header_when_no_cfg_measured_coverage() -> None: + """Nothing to follow, so the header stays as `__init__` set it.""" + primary = reported({}) + + primary.gen_results_summary() + + assert_that(primary.summary_header, equal_to(FALLBACK_HEADER)) + + @staticmethod + def test_reports_cfgs_that_measured_different_columns( + dvsim_log: pytest.LogCaptureFixture, + ) -> None: + """One table cannot carry two vocabularies, so a clash is said rather than resolved. + + A single `-t` makes every cfg in a run share an engine today. This is what says so if + that ever stops being true, instead of labelling one engine's figures with the other's + column names. + """ + primary = reported({"coverage": JASPERGOLD}, {"coverage": VCFORMAL}) + + primary.gen_results_summary() + + assert_that(dvsim_log.text, contains_string("different coverage columns")) + assert_that(primary.summary_header, has_length(len(FALLBACK_HEADER))) + + @staticmethod + def test_a_cfg_missing_its_results_stays_aligned_with_the_header( + dvsim_log: pytest.LogCaptureFixture, + ) -> None: + """The placeholder row follows the header's width rather than assuming three columns.""" + primary = reported({"coverage": VCFORMAL}) + primary.cfgs[0].result_summary.clear() + + table = primary.gen_results_summary() + + assert_that(dvsim_log.text, contains_string("could not find generated results_summary")) + assert_that(table, contains_string("ERROR")) + assert_that(table, is_not(contains_string("formal_cov")))