From 0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7 Mon Sep 17 00:00:00 2001
From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Sun, 8 Mar 2020 06:34:47 +0000
Subject: Add support for optimizing exists-forall problems.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 examples/smtbmc/Makefile | 11 +++++++++--
 examples/smtbmc/demo9.v  | 13 +++++++++++++
 2 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 examples/smtbmc/demo9.v

(limited to 'examples')

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
+
-- 
cgit v1.2.3