parse solver location output for assert failures (cover not functional yet)

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index f3b78eaa6d0d4deed1c57ae599a4828f7b9e1152..8d6cfc9e8ff947cc92057cb4fdb040469053cf7e 100644 (file)
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -478,7 +478,7 @@ def run_task(taskname):
             print(f'</properties>', file=f)
             if solver_gives_line:
                 for check in checks:
-                    print(f'<testcase classname="{junit_tc_name}" name="" time="{task.total_time}">', file=f) # name required
+                    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":
                         print(f'<skipped />', file=f)
                     elif check.status == "FAIL":

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 840f2152d59ba58994021b6edaf9201774f32f87..ec4e0a10df2afed88c8bb4601ee6ea2416fb0c34 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -222,8 +222,9 @@ class SbyTask:
         self.reusedir = reusedir
         self.status = "UNKNOWN"
         self.total_time = 0
-        self.expect = []
+        self.expect = list()
         self.design_hierarchy = None
+        self.precise_prop_status = False
 
         yosys_program_prefix = "" ##yosys-program-prefix##
         self.exe_paths = {
@@ -371,6 +372,9 @@ class SbyTask:
                 print(f"# running in {self.workdir}/src/", file=f)
                 for cmd in self.script:
                     print(cmd, file=f)
+                # assumptions at this point: hierarchy has been run and a top module has been designated
+                print("hierarchy -simcheck", file=f)
+                print(f"""write_json ../model/design.json""", file=f)
                 if model_name == "base":
                     print("memory_nordff", file=f)
                 else:
@@ -392,8 +396,6 @@ class SbyTask:
                 print("opt -keepdc -fast", file=f)
                 print("check", file=f)
                 print("hierarchy -simcheck", file=f)
-                # FIXME: can using design and design_nomem in the same task happen?
-                print(f"""write_json ../model/design{"" if model_name == "base" else "_nomem"}.json""", file=f)
                 print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f)
 
             proc = SbyProc(
@@ -407,9 +409,9 @@ class SbyTask:
 
             def instance_hierarchy_callback(retcode):
                 assert retcode == 0
-                assert self.design_hierarchy == None # verify this assumption
-                with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f:
-                    self.design_hierarchy = design_hierarchy(f)
+                if self.design_hierarchy == None:
+                    with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f:
+                        self.design_hierarchy = design_hierarchy(f)
 
             proc.exit_callback = instance_hierarchy_callback
 

diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index 79c4dddc9b6b05cbf3abeec755c4e294e4d0d2cf..7551ac716dec96b4fa6b161fc5d2755d86da729d 100644 (file)
--- a/sbysrc/sby_design.py
+++ b/sbysrc/sby_design.py
@@ -28,7 +28,7 @@ class SbyProperty:
         COVER = auto()
         LIVE = auto()
 
-        def __repr__(self):
+        def __str__(self):
             return self.name
 
         @classmethod
@@ -50,6 +50,9 @@ class SbyProperty:
     status: str = field(default="UNKNOWN")
     tracefile: str = field(default="")
 
+    def __repr__(self):
+        return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\""
+
 @dataclass
 class SbyModule:
     name: str
@@ -57,13 +60,35 @@ class SbyModule:
     submodules: dict = field(default_factory=dict)
     properties: list = field(default_factory=list)
 
+    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)
-        for submod in self.submodules:
+        for submod in self.submodules.values():
             l.extend(submod.get_property_list())
         return l
 
+    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
+        path = hierarchy.split('.')
+        mod = path.pop(0)
+        if self.name != mod:
+            raise ValueError(f"{self.name} is not the first module in hierarchical path {hierarchy}.")
+        try:
+            mod_hier = self
+            while path:
+                mod = path.pop(0)
+                mod_hier = mod_hier.submodules[mod]
+        except KeyError:
+            raise KeyError(f"Could not find {hierarchy} in design hierarchy!")
+        try:
+            prop = next(p for p in mod_hier.properties if location in p.location)
+        except StopIteration:
+            raise KeyError(f"Could not find assert at {location} in properties list!")
+        return prop
+
 def design_hierarchy(filename):
     design_json = json.load(filename)
     def make_mod_hier(instance_name, module_name, hierarchy=""):

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index da2e31c1e655918c3fdad842dfede128993b3400..b736e312049362501330a94f564f212f2698ec36 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -32,6 +32,7 @@ def run(mode, task, engine_idx, engine):
     basecase_only = False
     induction_only = False
     random_seed = None
+    task.precise_prop_status = True
 
     opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
@@ -154,9 +155,11 @@ def run(mode, task, engine_idx, engine):
         task.induction_procs.append(proc)
 
     proc_status = None
+    last_prop = None
 
     def output_callback(line):
         nonlocal proc_status
+        nonlocal last_prop
 
         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
         if match:
@@ -178,6 +181,28 @@ 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)
+        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)})"
+            prop.status = "FAIL"
+            last_prop = prop
+            return line
+
+        match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) in step \d+.", line)
+        if match:
+            location = match[1]
+
+        match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
+        if match and last_prop:
+            last_prop.tracefile = match[1]
+            last_prop = None
+
         return line
 
     def exit_callback(retcode):

diff --git a/tests/submod_props.sby b/tests/submod_props.sby
new file mode 100644 (file)
index 0000000..33a3a00
--- /dev/null
+++ b/tests/submod_props.sby
@@ -0,0 +1,30 @@
+[tasks]
+bmc
+cover
+
+[options]
+bmc: mode bmc
+cover: mode cover
+
+expect fail
+
+[engines]
+smtbmc boolector
+
+[script]
+read_verilog -sv test.sv
+prep -top top
+
+[file test.sv]
+module test(input foo);
+always @* assert(foo);
+always @* assert(!foo);
+always @* cover(foo);
+always @* cover(!foo);
+endmodule
+
+module top();
+test test_i (
+.foo(1'b1)
+);
+endmodule