mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 22:14:08 +00:00
Code Activity

Prefer the first tracefile for each failing assertion

Browse source
This commit is contained in:
Jannis Harder 2022-03-30 13:35:57 +02:00
parent 2e0087fd2f
commit b725bfed0c
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
sbysrc/sby_engine_smtbmc.py
View file

@ -210,7 +210,8 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
if match and last_prop:
for p in last_prop:
p.tracefile = match[1]
if not p.tracefile:
p.tracefile = match[1]
last_prop = []
return line

2
tests/keepgoing_multi_step.check.py
View file

@ -25,3 +25,5 @@ for task in ["keepgoing_multi_step_bmc", "keepgoing_multi_step_prove"]:
assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M)
assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M)
pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd"
assert re.search(pattern, open(f"{task}/{task}.xml").read())