From c7e4785a8a503e95065329eee3f6e20db46954a0 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Tue, 22 Mar 2022 16:16:02 +0100
Subject: [PATCH] junit: handle multiple asserts failing with the same trace
---
sbysrc/sby_engine_smtbmc.py | 11 ++++++-----
tests/2props1trace.sby | 22 ++++++++++++++++++++++
2 files changed, 28 insertions(+), 5 deletions(-)
create mode 100644 tests/2props1trace.sby
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 492e2a5..4605408 100644
--- 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
@@ -186,7 +186,7 @@ def run(mode, task, engine_idx, engine):
cell_name = match[3]
prop = task.design_hierarchy.find_property_by_cellname(cell_name)
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)
@@ -194,13 +194,14 @@ def run(mode, task, engine_idx, engine):
cell_name = match[2]
prop = task.design_hierarchy.find_property_by_cellname(cell_name)
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
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