diff options
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 3d6d3e1b3..5e6f43277 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -53,8 +53,7 @@ so = SmtOpts() def usage(): - print(""" -yosys-smtbmc [options] <yosys_smt2_output> + print(os.path.basename(sys.argv[0]) + """ [options] <yosys_smt2_output> -t <num_steps> -t <skip_steps>:<num_steps> @@ -1158,6 +1157,8 @@ def smt_forall_assert(): global asserts_cache_dirty asserts_cache_dirty = False + assert (len(smt.modinfo[topmod].maximize) + len(smt.modinfo[topmod].minimize) <= 1) + def make_assert_expr(asserts_cache): expr = list() for lst in asserts_cache: @@ -1236,6 +1237,18 @@ def smt_forall_assert(): smt.write("".join(assert_expr)) + if len(smt.modinfo[topmod].maximize) > 0: + for s in states: + if s in used_states_db: + smt.write("(maximize (|%s| %s))\n" % (smt.modinfo[topmod].maximize.copy().pop(), s)) + break + + if len(smt.modinfo[topmod].minimize) > 0: + for s in states: + if s in used_states_db: + smt.write("(minimize (|%s| %s))\n" % (smt.modinfo[topmod].minimize.copy().pop(), s)) + break + def smt_push(): global asserts_cache_dirty asserts_cache_dirty = True |