diff options
author | Jannis Harder <me@jix.one> | 2022-08-02 17:04:34 +0200 |
---|---|---|
committer | Jannis Harder <me@jix.one> | 2022-08-16 13:37:30 +0200 |
commit | 475267ac254f6f5ec2202b58c26d8ea82c9d2e4a (patch) | |
tree | 2f1ed0b092e799d271321ac910a0ea505ad2913d /backends/smt2 | |
parent | efd5b86eb9c56d293c608d378ee90beea53784b5 (diff) | |
download | yosys-475267ac254f6f5ec2202b58c26d8ea82c9d2e4a.tar.gz yosys-475267ac254f6f5ec2202b58c26d8ea82c9d2e4a.tar.bz2 yosys-475267ac254f6f5ec2202b58c26d8ea82c9d2e4a.zip |
smtbmc: Add --check-witness mode
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
Diffstat (limited to 'backends/smt2')
-rw-r--r-- | backends/smt2/smtbmc.py | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index b8ea22aaf..3714e2918 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -54,6 +54,7 @@ smtctop = None noinit = False binarymode = False keep_going = False +check_witness = False so = SmtOpts() @@ -170,6 +171,10 @@ def usage(): covering all found failed assertions, the character '%' is 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()) sys.exit(1) @@ -178,7 +183,7 @@ try: 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", "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: usage() @@ -257,6 +262,8 @@ for o, a in opts: binarymode = True elif o == "--keep-going": keep_going = True + elif o == "--check-witness": + check_witness = True elif so.handle(o, a): pass else: @@ -1774,6 +1781,7 @@ else: # not tempind, covermode smt_assert("(not %s)" % active_assert_expr) else: + active_assert_expr = "true" smt_assert("false") @@ -1781,6 +1789,17 @@ else: # not tempind, covermode if retstatus != "FAILED": 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: for i in range(last_check_step+1, last_check_step+1+append_steps): print_msg("Appending additional step %d." % i) @@ -1873,6 +1892,8 @@ else: # not tempind, covermode print_anyconsts(0) write_trace(0, num_steps, '%') + if check_witness: + retstatus = "FAILED" smt.write("(exit)") smt.wait() |