From b7cfb7dbd250a8595589f86e1b38b67015c7b9c5 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 11 Jan 2017 14:14:12 +0100 Subject: [PATCH] Fix $initstate handling bug in yosys-smtbmc --- backends/smt2/smtbmc.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 8dbb047aa..ecee6795e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -789,6 +789,7 @@ else: # not tempind for i in range(1, step_size): if step+i < num_steps: 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_h| s%d))" % (topmod, 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): 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)) -- 2.30.2