diff options
| -rw-r--r-- | backends/smt2/smt2.cc | 8 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 14 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 12 | ||||
| -rw-r--r-- | examples/smtbmc/Makefile | 11 | ||||
| -rw-r--r-- | examples/smtbmc/demo9.v | 13 |
5 files changed, 55 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 081dcda99..3e08ce37b 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -536,6 +536,14 @@ struct Smt2Worker if (cell->attributes.count("\\reg")) infostr += " " + cell->attributes.at("\\reg").decode_string(); decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str())); + if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){ + decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter)); + log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str()); + } + else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){ + decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter)); + log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str()); + } makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))); if (cell->type == "$anyseq") ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter)); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 3d6d3e1b3..630464419 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1158,6 +1158,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 +1238,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 diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 34bf7ef38..4c691716e 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -101,6 +101,8 @@ class SmtModInfo: self.cells = dict() self.asserts = dict() self.covers = dict() + self.maximize = set() + self.minimize = set() self.anyconsts = dict() self.anyseqs = dict() self.allconsts = dict() @@ -502,6 +504,12 @@ class SmtIo: if fields[1] == "yosys-smt2-cover": self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-maximize": + self.modinfo[self.curmod].maximize.add(fields[2]) + + if fields[1] == "yosys-smt2-minimize": + self.modinfo[self.curmod].minimize.add(fields[2]) + if fields[1] == "yosys-smt2-anyconst": self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) @@ -696,7 +704,9 @@ class SmtIo: if msg is not None: print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True) - result = self.read() + result = "" + while result not in ["sat", "unsat"]: + result = self.read() if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile index 96fa058d6..61994f942 100644 --- a/examples/smtbmc/Makefile +++ b/examples/smtbmc/Makefile @@ -1,5 +1,5 @@ -all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 +all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 demo1: demo1.smt2 yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2 @@ -28,6 +28,9 @@ demo7: demo7.smt2 demo8: demo8.smt2 yosys-smtbmc -s z3 -t 1 -g demo8.smt2 +demo9: demo9.smt2 + yosys-smtbmc -s z3 -t 1 -g demo9.smt2 + demo1.smt2: demo1.v yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2' @@ -52,6 +55,9 @@ demo7.smt2: demo7.v demo8.smt2: demo8.v yosys -ql demo8.yslog -p 'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2' +demo9.smt2: demo9.v + yosys -ql demo9.yslog -p 'read_verilog -formal demo9.v; prep -top demo9 -nordff; write_smt2 -stbv -wires demo9.smt2' + clean: rm -f demo1.yslog demo1.smt2 demo1.vcd rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd @@ -61,6 +67,7 @@ clean: rm -f demo6.yslog demo6.smt2 rm -f demo7.yslog demo7.smt2 rm -f demo8.yslog demo8.smt2 + rm -f demo9.yslog demo9.smt2 -.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 clean +.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 clean diff --git a/examples/smtbmc/demo9.v b/examples/smtbmc/demo9.v new file mode 100644 index 000000000..f0b91e2ca --- /dev/null +++ b/examples/smtbmc/demo9.v @@ -0,0 +1,13 @@ +module demo9; + (* maximize *) wire[7:0] h = $anyconst; + wire [7:0] i = $allconst; + + wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011); + wire trigger = (t0 > h) && (h < 8'b00000100); + + always @* begin + assume(trigger == 1'b1); + cover(1); + end +endmodule + |