mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 18:05:24 +00:00
Code Activity

smtbmc: Add --check-witness mode

Browse source 
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
This commit is contained in:
Jannis Harder 2022-08-02 17:04:34 +02:00
parent efd5b86eb9
commit 475267ac25
1 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
backends/smt2/smtbmc.py
View file

@ -54,6 +54,7 @@ smtctop = None
noinit = False noinit = False
binarymode = False binarymode = False
keep_going = False keep_going = False
check_witness = False
so = SmtOpts() so = SmtOpts()
@ -170,6 +171,10 @@ def usage():
covering all found failed assertions, the character '%' is covering all found failed assertions, the character '%' is
replaced in all dump filenames with an increasing number. replaced in all dump filenames with an increasing number.
--check-witness
check that the used witness file contains sufficient
constraints to force an assertion failure.
""" + so.helpmsg()) """ + so.helpmsg())
sys.exit(1) sys.exit(1)
@ -178,7 +183,7 @@ try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
"dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit", "binary", "keep-going"]) "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"])
except: except:
usage() usage()
@ -257,6 +262,8 @@ for o, a in opts:
binarymode = True binarymode = True
elif o == "--keep-going": elif o == "--keep-going":
keep_going = True keep_going = True
elif o == "--check-witness":
check_witness = True
elif so.handle(o, a): elif so.handle(o, a):
pass pass
else: else:
@ -1774,6 +1781,7 @@ else: # not tempind, covermode
smt_assert("(not %s)" % active_assert_expr) smt_assert("(not %s)" % active_assert_expr)
else: else:
active_assert_expr = "true"
smt_assert("false") smt_assert("false")
@ -1781,6 +1789,17 @@ else: # not tempind, covermode
if retstatus != "FAILED": if retstatus != "FAILED":
print("%s BMC failed!" % smt.timestamp()) print("%s BMC failed!" % smt.timestamp())
if check_witness:
print_msg("Checking witness constraints...")
smt_pop()
smt_push()
smt_assert(active_assert_expr)
if smt_check_sat() != "sat":
retstatus = "PASSED"
check_witness = False
num_steps = -1
break
if append_steps > 0: if append_steps > 0:
for i in range(last_check_step+1, last_check_step+1+append_steps): for i in range(last_check_step+1, last_check_step+1+append_steps):
print_msg("Appending additional step %d." % i) print_msg("Appending additional step %d." % i)
@ -1873,6 +1892,8 @@ else: # not tempind, covermode
print_anyconsts(0) print_anyconsts(0)
write_trace(0, num_steps, '%') write_trace(0, num_steps, '%')
if check_witness:
retstatus = "FAILED"
smt.write("(exit)") smt.write("(exit)")
smt.wait() smt.wait()