handle status of cover properties

sbysrc/sby.py

@@ -20,7 +20,7 @@
 import argparse, os, sys, shutil, tempfile, re
 ##yosys-sys-path##
 from sby_core import SbyTask, SbyAbort, process_filename
-import time
+import time, platform
 
 class DictAction(argparse.Action):
     def __call__(self, parser, namespace, values, option_string=None):
@@ -458,7 +458,6 @@ def run_task(taskname):
             checks = task.design_hierarchy.get_property_list()
             junit_tests = len(checks)
             junit_errors = 1 if task.retcode == 16 else 0
-            solver_gives_line = task.status == "FAIL" and any(check.status != "UNKNOWN" for check in checks)
             junit_failures = 0
             if junit_errors == 0 and task.retcode != 0:
                 if solver_gives_line:
@@ -471,15 +470,17 @@ def run_task(taskname):
             junit_time = time.strftime('%Y-%m-%dT%H:%M:%S')
             print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
             print(f'<testsuites>', file=f)
-            #TODO: check with Micko if os.uname().nodename is sane enough in most places
-            print(f'<testsuite timestamp="{junit_time}" hostname="{os.uname().nodename}" package="" id="1" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{task.total_time}" skipped="{junit_tests - junit_failures}">', file=f)
+            print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="1" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{task.total_time}" skipped="{junit_tests - junit_failures}">', file=f)
             print(f'<properties>', file=f)
-            print(f'<property name="os" value="{os.name}"/>', file=f)
+            print(f'<property name="os" value="{platform.system()}"/>', file=f)
             print(f'</properties>', file=f)
-            if solver_gives_line:
+            if task.precise_prop_status:
                 for check in checks:
-                    print(f'<testcase classname="{junit_tc_name}" name="Property {check.type} in {check.hierarchy} at {check.location}" time="{task.total_time}">', file=f) # name required
-                    if check.status == "UNKNOWN":
+                    detail_attrs = f' type="{check.type}" location="{check.location}" id="{check.name}"'
+                    print(f'<testcase classname="{junit_tc_name}" name="Property {check.type} in {check.hierarchy} at {check.location}" time="{task.total_time}"{detail_attrs}>', file=f) # name required
+                    if check.status == "PASS":
+                        pass
+                    elif check.status == "UNKNOWN":
                         print(f'<skipped />', file=f)
                     elif check.status == "FAIL":
                         print(f'<failure type="{check.type}" message="Property in {check.hierarchy} at {check.location} failed. Trace file: {check.tracefile}" />', file=f)

sbysrc/sby_design.py

@@ -63,12 +63,14 @@ class SbyModule:
     def __repr__(self):
         return f"SbyModule<{self.name} : {self.type}, submodules={self.submodules}, properties={self.properties}>"
 
-    def get_property_list(self):
-        l = list()
-        l.extend(self.properties)
+    def __iter__(self):
+        for prop in self.properties:
+            yield prop
         for submod in self.submodules.values():
-            l.extend(submod.get_property_list())
-        return l
+            yield from submod.__iter__()
+
+    def get_property_list(self):
+        return [p for p in self if p.type != p.Type.ASSUME]
 
     def find_property(self, hierarchy, location):
         # FIXME: use that RE that works with escaped paths from https://stackoverflow.com/questions/46207665/regex-pattern-to-split-verilog-path-in-different-instances-using-python
@@ -89,6 +91,12 @@ class SbyModule:
             raise KeyError(f"Could not find assert at {location} in properties list!")
         return prop
 
+    def find_property_by_cellname(self, cell_name):
+        for prop in self:
+            if prop.name == cell_name:
+                return prop
+        raise KeyError(f"No such property: {cell_name}")
+
 def design_hierarchy(filename):
     design_json = json.load(filename)
     def make_mod_hier(instance_name, module_name, hierarchy=""):
@@ -121,7 +129,10 @@ def main():
     if len(sys.argv) != 2:
         print(f"""Usage: {sys.argv[0]} design.json""")
     with open(sys.argv[1]) as f:
-        print(design_hierarchy(f))
+        d = design_hierarchy(f)
+        print("Design Hierarchy:", d)
+        for p in d.get_property_list():
+            print("Property:", p)
 
 if __name__ == '__main__':
     main()

sbysrc/sby_engine_smtbmc.py

@@ -143,7 +143,7 @@ def run(mode, task, engine_idx, engine):
         task,
         procname,
         task.model(model_name),
-        f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
+        f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --cellinfo --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
         logfile=open(logfile_prefix + ".txt", "w"),
         logstderr=(not progress)
     )
@@ -181,22 +181,20 @@ def run(mode, task, engine_idx, engine):
             proc_status = "ERROR"
             return line
 
-        match = re.match(r"^## [0-9: ]+ Assert failed in (([a-z_][a-z0-9$_]*|\\\S*|\.)+): (\S*).*", line)
+        match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
         if match:
-            module_path = match[1]
-            location = match[3]
-            try:
-                prop = task.design_hierarchy.find_property(module_path, location)
-            except KeyError as e:
-                task.precise_prop_status = False
-                return line + f" (Warning: {str(e)})"
+            cell_name = match[3]
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
             prop.status = "FAIL"
             last_prop = prop
             return line
 
-        match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) in step \d+.", line)
+        match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
         if match:
-            location = match[1]
+            cell_name = match[2]
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop.status = "PASS"
+            last_prop = prop
 
         match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
         if match and last_prop:
@@ -231,6 +229,10 @@ def run(mode, task, engine_idx, engine):
                         excess_traces += 1
                     if excess_traces > 0:
                         task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
+            elif proc_status == "PASS" and mode == "bmc":
+                for prop in task.design_hierarchy:
+                    if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
+                        prop.status = "PASS"
 
             task.terminate()