diff options
| author | Andrew Zonenberg <azonenberg@drawersteak.com> | 2017-01-15 09:43:15 -0800 |
|---|---|---|
| committer | Andrew Zonenberg <azonenberg@drawersteak.com> | 2017-01-15 09:43:15 -0800 |
| commit | 0c83a30f950d766ddd09bb744ee93e2433095b5c (patch) | |
| tree | ebcd15a0e73b9737d64a723a20214960d033e467 /backends/smt2/smtbmc.py | |
| parent | ac90de73becaeac034b226def9c387645698c363 (diff) | |
| parent | 78f65f89ffc1d5c5237009c19e84e625ce3085aa (diff) | |
| download | yosys-0c83a30f950d766ddd09bb744ee93e2433095b5c.tar.gz yosys-0c83a30f950d766ddd09bb744ee93e2433095b5c.tar.bz2 yosys-0c83a30f950d766ddd09bb744ee93e2433095b5c.zip | |
Merge https://github.com/cliffordwolf/yosys
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 2 |
1 files changed, 2 insertions, 0 deletions
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)) |