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

Fix $initstate handling bug in yosys-smtbmc

Browse source
This commit is contained in:
Clifford Wolf 2017-01-11 14:14:12 +01:00
parent 8953a55cd8
commit b7cfb7dbd2
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
backends/smt2/smtbmc.py
View file

@ -789,6 +789,7 @@ else: # not tempind
for i in range(1, step_size): for i in range(1, step_size):
if step+i < num_steps: if step+i < num_steps:
smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod)) smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod))
smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step+i))
smt.write("(assert (|%s_u| s%d))" % (topmod, step+i)) smt.write("(assert (|%s_u| s%d))" % (topmod, step+i))
smt.write("(assert (|%s_h| s%d))" % (topmod, step+i)) smt.write("(assert (|%s_h| s%d))" % (topmod, step+i))
smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i))
@ -812,6 +813,7 @@ else: # not tempind
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)
smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod)) 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_u| s%d))" % (topmod, i))
smt.write("(assert (|%s_h| 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_t| s%d s%d))" % (topmod, i-1, i))