Merge pull request #145 from nakengelhardt/fix_junit_tracefile

junit: handle multiple asserts failing with the same trace

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index ab0c7e5f243ca17b43a319b100e73865256ddb3a..a9c5c804226ea14f084c79d4de605d031b4e2ab4 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -155,7 +155,7 @@ def run(mode, task, engine_idx, engine):
         task.induction_procs.append(proc)
 
     proc_status = None
-    last_prop = None
+    last_prop = []
 
     def output_callback(line):
         nonlocal proc_status
@@ -187,7 +187,7 @@ def run(mode, task, engine_idx, engine):
             cell_name = match[3]
             prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
-            last_prop = prop
+            last_prop.append(prop)
             return line
 
         match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
@@ -195,13 +195,14 @@ def run(mode, task, engine_idx, engine):
             cell_name = match[2]
             prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "PASS"
-            last_prop = prop
+            last_prop.append(prop)
             return line
 
         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
+            for p in last_prop:
+                p.tracefile = match[1]
+            last_prop = []
             return line
 
         match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)

diff --git a/tests/2props1trace.sby b/tests/2props1trace.sby
new file mode 100644 (file)
index 0000000..8f51fde
--- /dev/null
+++ b/tests/2props1trace.sby
@@ -0,0 +1,22 @@
+[options]
+mode bmc
+depth 1
+expect fail
+
+[engines]
+smtbmc
+
+[script]
+read -sv top.sv
+prep -top top
+
+[file top.sv]
+module top(
+input foo,
+input bar
+);
+always @(*) begin
+       assert (foo);
+       assert (bar);
+end
+endmodule