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

Merge pull request #3816 from jix/smtbmc-cover-keepgoing

This commit is contained in:
Jannis Harder 2023-06-26 16:35:52 +02:00 committed by GitHub
parent b87af9cec0 f9744fdfcd
commit 6be5f6449c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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: