Added examples/smtbmc

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
new file mode 100644 (file)
index 0000000..48c81a4
--- /dev/null
+++ b/examples/smtbmc/Makefile
@@ -0,0 +1,13 @@
+
+demo1: demo1.smt2
+       yosys-smtbmc -c demo1.vcd demo1.smt2
+       yosys-smtbmc -i -c demo1.vcd demo1.smt2
+
+demo1.smt2: demo1.v
+       yosys -p 'read_verilog -formal demo1.v; prep -top demo1; write_smt2 -wires -mem -bv demo1.smt2'
+
+clean:
+       rm -f demo1.smt2
+
+.PHONY: demo1 clean
+

diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
new file mode 100644 (file)
index 0000000..59e4978
--- /dev/null
+++ b/examples/smtbmc/demo1.v
@@ -0,0 +1,17 @@
+module demo1(input clk, input addtwo, output iseven);
+       reg [3:0] cnt = 0;
+       wire [3:0] next_cnt;
+
+       inc inc_inst (addtwo, iseven, cnt, next_cnt);
+
+       always @(posedge clk)
+               cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
+       
+       assert property (cnt != 15);
+       // initial expect ((iseven && addtwo) || cnt == 9);
+endmodule
+
+module inc(input addtwo, output iseven, input [3:0] a, output [3:0] y);
+       assign iseven = !a[0];
+       assign y = a + (addtwo ? 2 : 1);
+endmodule