diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-02-25 23:41:40 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-02-25 23:41:40 +0100 |
| commit | 38bf458037a61d127422ef405230871f50dcd4e6 (patch) | |
| tree | 7395dead403e0a972b478446ef0563ec077adf97 /backends/smt2/smtbmc.py | |
| parent | d6858ad15b7be4c7f324a57b0d54cffd50826b3b (diff) | |
| download | yosys-38bf458037a61d127422ef405230871f50dcd4e6.tar.gz yosys-38bf458037a61d127422ef405230871f50dcd4e6.tar.bz2 yosys-38bf458037a61d127422ef405230871f50dcd4e6.zip | |
Add support for "yosys-smtbmc -c --append"
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 39ac181dd..92a9a1a21 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -872,6 +872,18 @@ elif covermode: smt.write("(pop 1)") break + if append_steps > 0: + for i in range(step+1, step+1+append_steps): + print_msg("Appending additional step %d." % i) + smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod)) + smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i)) + smt.write("(assert (|%s_u| s%d))" % (topmod, i)) + smt.write("(assert (|%s_h| s%d))" % (topmod, i)) + smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, i)) + print_msg("Re-solving with appended steps..") + assert smt.check_sat() == "sat" + reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) assert len(reached_covers) == len(cover_desc) @@ -891,7 +903,7 @@ elif covermode: if print_failed_asserts(i, extrainfo=" (step %d)" % i): found_failed_assert = True - write_trace(0, step+1, "%d" % coveridx) + write_trace(0, step+1+append_steps, "%d" % coveridx) if found_failed_assert: break |