Wrong assumption reported in summary

sby reports that a wrong assumption has failed when you have a design where you instantiate a module two times and the assertion in the second module fails.

For example, if you have the following two modules:

// mod.v
module mod (
    input x,
    input y);

    always @(*)
        c_mod: assert(x == y);

endmodule

// main.v
module main();

    mod m1(1, 1);
    mod m2(1, 0);

endmodule

where the main is the top module and you run a bounded model check with smtbmc + z3 engine with the following .sby file [1], you get the following output:

sby -f test.sby 
...
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Solver: z3
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Assert failed in main.m2: c_mod
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY 17:12:41 [test_t_bmc] engine_0: ##   0:00:00  Status: failed
...
SBY 17:12:41 [test_t_bmc] summary: engine_0 (smtbmc z3) returned FAIL
SBY 17:12:41 [test_t_bmc] summary: counterexample trace: test_t_bmc/engine_0/trace.vcd
SBY 17:12:41 [test_t_bmc] summary:   failed assertion main.m1.c_mod at mod.v:6.9-6.30 in step 0
SBY 17:12:41 [test_t_bmc] DONE (FAIL, rc=2)
SBY 17:12:41 The following tasks failed: ['t_bmc']

You can see that yosys-smtbmc reports that the assertion has failed in main.m2 where in summary sby reports that it has failed in main.m1.

This problem is present in SBY yosys-0.43 and probably in SBY yosys-0.44. (I only tested it with SBY yosys-0.43.)

Cause

It seems that a problem lies in the use of find_property_by_cellname function, in sby_engine_smtbmc.py, to find the right property that has failed in design hierarchy (design.hiarchy). In the case above, we have two instantiations of the same module which means that in the design hierarchy we'll have two properties with the same name (one in m1 and the other in m2). Because find_property_by_cellname only uses the name (c_mod) to find the property, it will always return the property from m1 regardless if the property fails in m1 or in m2.

Suggestion solution: Consider the entire path (including the module's names) when searching for the property in the design hierarchy. The following solution worked for me.

diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index d93d17d..a08519d 100644
--- a/sbysrc/sby_design.py
+++ b/sbysrc/sby_design.py
@@ -166,6 +166,11 @@ class SbyModule:
                 return prop
         raise KeyError(f"No such property: {cell_name}")

+    def find_property_by_path(self, path):
+        for prop in self:
+            if pretty_path(prop.path) == path:
+                return prop
+        raise KeyError(f"No such property: {path}")

 @dataclass
 class SbyDesign:
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 5fb0b89..6db0d11 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -231,7 +231,9 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line)
         if match:
             cell_name = match[3] or match[2]
-            prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+            mod_path = match[1]
+            path = mod_path + "." + cell_name.translate(str.maketrans(smt2_trans))
+            prop = task.design.hierarchy.find_property_by_path(path)
             prop.status = "FAIL"
             task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))                                                        
             last_prop.append(prop)

P.S.: I'm not completely sure what is the reason for the name translation and if it should also be applied to the entire path.

[1]

[tasks]
t_bmc

[options]
t_bmc:
mode bmc
--

[engines]
smtbmc z3

[script]
read -formal mod.v
read -formal main.v
prep -top main

[files]
./src/mod.v
./src/main.v

YosysHQ / sby

Wrong assumption reported in summary #296

Cause