Add support for optimizing exists-forall problems.

Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 081dcda999afe06411a48c90166b9a1ce1fa60b1..3e08ce37be55bef7b3cff66589a712242e8b7e99 100644 (file)
--- 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 3d6d3e1b39d93217e543c51c71ded4a83eac2616..63046441960db76e5453e0304354b301477c5ec7 100644 (file)
--- 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 34bf7ef38eea2b251efb035f1197ebf1c476214a..4c691716e609ad791e2eea84a9a3fc33249bacf5 100644 (file)
--- 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 96fa058d6fbeea1fa5d1da58a711a5385bff9d6f..61994f942fb524c07fc77072fa3ec4013b9c829e 100644 (file)
--- 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 (file)
index 0000000..f0b91e2
--- /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
+