Added examples/smtbmc

2 files changed, 30 insertions, 0 deletions

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
new file mode 100644
index 000000000..48c81a463
--- /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
index 000000000..59e497825
--- /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