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

Add support for "yosys-smtbmc -c --append"

Browse source
This commit is contained in:
Clifford Wolf 2017-02-25 23:41:40 +01:00
parent d6858ad15b
commit 38bf458037
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
backends/smt2/smtbmc.py
View file

@ -872,6 +872,18 @@ elif covermode:
smt.write("(pop 1)") smt.write("(pop 1)")
break 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))) reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
assert len(reached_covers) == len(cover_desc) assert len(reached_covers) == len(cover_desc)
@ -891,7 +903,7 @@ elif covermode:
if print_failed_asserts(i, extrainfo=" (step %d)" % i): if print_failed_asserts(i, extrainfo=" (step %d)" % i):
found_failed_assert = True found_failed_assert = True
write_trace(0, step+1, "%d" % coveridx) write_trace(0, step+1+append_steps, "%d" % coveridx)
if found_failed_assert: if found_failed_assert:
break break