riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

smtbmc: Make cover mode respect --keep-going 

As cover mode by default stops looking for further traces when an
assertion fails, it should respect --keep-going.
This commit is contained in:
Jannis Harder 2023-06-23 10:27:38 +02:00
parent f9257d3192
commit f9744fdfcd
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
backends/smt2/smtbmc.py
View File

@ -174,6 +174,8 @@ def help():
further failed assertions. To output multiple traces
covering all found failed assertions, the character '%' is
replaced in all dump filenames with an increasing number.
In cover mode, don't stop when a cover trace contains a failed
assertion.
--check-witness
check that the used witness file contains sufficient
@ -1739,7 +1741,7 @@ elif covermode:
smt_pop()
smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
if found_failed_assert:
if found_failed_assert and not keep_going:
break
if "1" not in cover_mask: