fix: formal flow

Signed-off-by: James McCorrie <james.mccorrie@lowrisc.org>

Author: machshev

src/dvsim/flow/formal.py

@@ -1,6 +1,8 @@
 # Copyright lowRISC contributors (OpenTitan project).
 # Licensed under the Apache License, Version 2.0, see LICENSE for details.
 # SPDX-License-Identifier: Apache-2.0
+from collections.abc import Sequence
+from dvsim.job.data import CompletedJobStatus
 
 from pathlib import Path
 
@@ -176,41 +178,47 @@ def gen_results_summary(self):
 
         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": {
-        #      formal:  "90 %",
-        #      stimuli: "90 %",
-        #      checker: "80 %"
-        #   }
+    def _gen_results(self, results: Sequence[CompletedJobStatus]) -> None:
+        """Generate 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": {
+             formal:  "90 %",
+             stimuli: "90 %",
+             checker: "80 %"
+          }
+        """
+        # There should be just one job that has run for this config.
+        complete_job = results[0]
+
         results_str = "## " + self.results_title + "\n\n"
         results_str += "### " + self.timestamp_long + "\n"
         if self.revision:
@@ -222,7 +230,7 @@ def _gen_results(self, results):
         assert len(self.deploy) == 1
         mode = self.deploy[0]
 
-        if results[mode] == "P":
+        if complete_job.status == "P":
             result_data = Path(
                 subst_wildcards(self.build_dir, {"build_mode": mode.name}),
                 "results.hjson",
@@ -254,8 +262,8 @@ def _gen_results(self, results):
         else:
             summary += ["N/A", "N/A", "N/A"]
 
-        if results[mode] != "P":
-            results_str += "\n## List of Failures\n" + "".join(mode.launcher.fail_msg.message)
+        if complete_job.status != "P":
+            results_str += "\n## List of Failures\n" + "".join(complete_job.fail_msg.message)
 
         messages = self.result.get("messages")
         if messages is not None:

src/dvsim/flow/lint.py

@@ -4,6 +4,9 @@
 
 """Class describing lint configuration object."""
 
+from dvsim.job.data import CompletedJobStatus
+
+from collections.abc import Sequence
 from pathlib import Path
 
 from tabulate import tabulate
@@ -99,26 +102,26 @@ def gen_results_summary(self):
 
     # TODO(#9079): This way of parsing out messages into an intermediate
     # results.hjson file will be replaced by a native parser mechanism.
-    def _gen_results(self, results):
-        # '''
-        # The function is called after the regression has completed. It looks
-        # for a results.hjson file with aggregated results from the lint run.
-        # The hjson needs to have the following format:
-        #
-        # {
-        #     bucket_key: [str],
-        #     // other buckets according to message_buckets configuration
-        # }
-        #
-        # Each bucket key points to a list of signatures (strings).
-        # The bucket categories and severities are defined in the
-        # message_buckets class variable, and can be set via Hjson Dvsim
-        # config files.
-        #
-        # Note that if this is a primary config, the results will
-        # be generated using the _gen_results_summary function
-        # '''
-
+    def _gen_results(self, results: Sequence[CompletedJobStatus]) -> None:
+        """Generate results.
+
+        The function is called after the regression has completed. It looks
+        for a results.hjson file with aggregated results from the lint run.
+        The hjson needs to have the following format:
+
+        {
+            bucket_key: [str],
+            // other buckets according to message_buckets configuration
+        }
+
+        Each bucket key points to a list of signatures (strings).
+        The bucket categories and severities are defined in the
+        message_buckets class variable, and can be set via Hjson Dvsim
+        config files.
+
+        Note that if this is a primary config, the results will
+        be generated using the _gen_results_summary function
+        """
         # Generate results table for runs.
         results_str = f"## {self.results_title}\n\n"
         results_str += f"### {self.timestamp_long}\n"

src/dvsim/flow/one_shot.py

@@ -154,7 +154,7 @@ def _create_deploy_objects(self) -> None:
         self._create_dirs()
 
     @abstractmethod
-    def _gen_results(self):
+    def _gen_results(self, results: Sequence[CompletedJobStatus]) -> None:
         """Generate results for this config."""
 
     @abstractmethod