11 files changed, 226 insertions, 0 deletions
diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore
new file mode 100644
index 00000000..a3f4f0f2
--- /dev/null
+++ b/examples/smtbmc/.gitignore
@@ -0,0 +1,22 @@
+demo1.smt2
+demo1.yslog
+demo2.smt2
+demo2.smtc
+demo2.vcd
+demo2.yslog
+demo2_tb
+demo2_tb.v
+demo2_tb.vcd
+demo3.smt2
+demo3.vcd
+demo3.yslog
+demo4.smt2
+demo4.vcd
+demo4.yslog
+demo5.smt2
+demo5.vcd
+demo5.yslog
+demo6.smt2
+demo6.yslog
+demo7.smt2
+demo7.yslog
diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
new file mode 100644
index 00000000..2f7060bd
--- /dev/null
+++ b/examples/smtbmc/Makefile
@@ -0,0 +1,59 @@
+
+all: demo1 demo2 demo3 demo4 demo5 demo6 demo7
+
+demo1: demo1.smt2
+	yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
+	yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
+
+demo2: demo2.smt2
+	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-smtc demo2.smtc --dump-vlogtb demo2_tb.v demo2.smt2
+	iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
+	vvp demo2_tb +vcd=demo2_tb.vcd
+
+demo3: demo3.smt2
+	yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2
+
+demo4: demo4.smt2
+	yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2
+
+demo5: demo5.smt2
+	yosys-smtbmc -g -t 50 --dump-vcd demo5.vcd demo5.smt2
+
+demo6: demo6.smt2
+	yosys-smtbmc -t 1 demo6.smt2
+
+demo7: demo7.smt2
+	yosys-smtbmc -t 10 demo7.smt2
+
+demo1.smt2: demo1.v
+	yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
+
+demo2.smt2: demo2.v
+	yosys -ql demo2.yslog -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires demo2.smt2'
+
+demo3.smt2: demo3.v
+	yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires demo3.smt2'
+
+demo4.smt2: demo4.v
+	yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires demo4.smt2'
+
+demo5.smt2: demo5.v
+	yosys -ql demo5.yslog -p 'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'
+
+demo6.smt2: demo6.v
+	yosys -ql demo6.yslog -p 'read_verilog demo6.v; prep -top demo6 -nordff; assertpmux; opt -keepdc -fast; write_smt2 -wires demo6.smt2'
+
+demo7.smt2: demo7.v
+	yosys -ql demo7.yslog -p 'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.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
+	rm -f demo3.yslog demo3.smt2 demo3.vcd
+	rm -f demo4.yslog demo4.smt2 demo4.vcd
+	rm -f demo5.yslog demo5.smt2 demo5.vcd
+	rm -f demo6.yslog demo6.smt2
+	rm -f demo7.yslog demo7.smt2
+
+.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 clean
+
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
new file mode 100644
index 00000000..567dde14
--- /dev/null
+++ b/examples/smtbmc/demo1.v
@@ -0,0 +1,19 @@
+module demo1(input clk, input addtwo, output iseven);
+	reg [3:0] cnt;
+	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;
+
+`ifdef FORMAL
+	assert property (cnt != 15);
+	initial assume (!cnt[2]);
+`endif
+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
diff --git a/examples/smtbmc/demo2.v b/examples/smtbmc/demo2.v
new file mode 100644
index 00000000..34745e89
--- /dev/null
+++ b/examples/smtbmc/demo2.v
@@ -0,0 +1,29 @@
+// Nothing to prove in this demo.
+// Just an example for memories, vcd dumps and vlog testbench dumps.
+
+`ifdef FORMAL
+`define assume(_expr_) assume(_expr_)
+`else
+`define assume(_expr_)
+`endif
+
+module demo2(input clk, input [4:0] addr, output reg [31:0] data);
+	reg [31:0] mem [0:31];
+	always @(posedge clk)
+		data <= mem[addr];
+
+	reg [31:0] used_addr = 0;
+	reg [31:0] used_dbits = 0;
+	reg initstate = 1;
+
+	always @(posedge clk) begin
+		initstate <= 0;
+		`assume(!used_addr[addr]);
+		used_addr[addr] <= 1;
+		if (!initstate) begin
+			`assume(data != 0);
+			`assume((used_dbits & data) == 0);
+			used_dbits <= used_dbits | data;
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo3.smtc b/examples/smtbmc/demo3.smtc
new file mode 100644
index 00000000..f5e017cf
--- /dev/null
+++ b/examples/smtbmc/demo3.smtc
@@ -0,0 +1,5 @@
+initial
+assume [rst]
+
+always -1
+assert (= [-1:mem] [mem])
diff --git a/examples/smtbmc/demo3.v b/examples/smtbmc/demo3.v
new file mode 100644
index 00000000..13b3a197
--- /dev/null
+++ b/examples/smtbmc/demo3.v
@@ -0,0 +1,18 @@
+// Whatever the initial content of this memory is at reset, it will never change
+// see demo3.smtc for assumptions and assertions
+
+module demo3(input clk, rst, input [15:0] addr, output reg [31:0] data);
+	reg [31:0] mem [0:2**16-1];
+	reg [15:0] addr_q;
+
+	always @(posedge clk) begin
+		if (rst) begin
+			data <= mem[0] ^ 123456789;
+			addr_q <= 0;
+		end else begin
+			mem[addr_q] <= data ^ 123456789;
+			data <= mem[addr] ^ 123456789;
+			addr_q <= addr;
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo4.smtc b/examples/smtbmc/demo4.smtc
new file mode 100644
index 00000000..2f91f816
--- /dev/null
+++ b/examples/smtbmc/demo4.smtc
@@ -0,0 +1,11 @@
+initial
+assume [rst]
+
+always -1
+assume (not [rst])
+assume (=> [-1:inv2] [inv2])
+
+final -2
+assume [-1:inv2]
+assume (not [-2:inv2])
+assert (= [r1] [r2])
diff --git a/examples/smtbmc/demo4.v b/examples/smtbmc/demo4.v
new file mode 100644
index 00000000..3f1b4727
--- /dev/null
+++ b/examples/smtbmc/demo4.v
@@ -0,0 +1,13 @@
+// Demo for "final" smtc constraints
+
+module demo4(input clk, rst, inv2, input [15:0] in, output reg [15:0] r1, r2);
+	always @(posedge clk) begin
+		if (rst) begin
+			r1 <= in;
+			r2 <= -in;
+		end else begin
+			r1 <= r1 + in;
+			r2 <= inv2 ? -(r2 - in) : (r2 - in);
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo5.v b/examples/smtbmc/demo5.v
new file mode 100644
index 00000000..63ace307
--- /dev/null
+++ b/examples/smtbmc/demo5.v
@@ -0,0 +1,18 @@
+// Demo for $anyconst
+
+module demo5 (input clk);
+	wire [7:0] step_size = $anyconst;
+	reg [7:0] state = 0, count = 0;
+	reg [31:0] hash = 0;
+
+	always @(posedge clk) begin
+		count <= count + 1;
+		hash <= ((hash << 5) + hash) ^ state;
+		state <= state + step_size;
+	end
+
+	always @* begin
+		if (count == 42)
+			assert(hash == 32'h A18FAC0A);
+	end
+endmodule
diff --git a/examples/smtbmc/demo6.v b/examples/smtbmc/demo6.v
new file mode 100644
index 00000000..62a72e2a
--- /dev/null
+++ b/examples/smtbmc/demo6.v
@@ -0,0 +1,14 @@
+// Demo for assertpmux
+
+module demo6 (input A, B, C, D, E, output reg Y);
+	always @* begin
+		Y = 0;
+		if (A != B) begin
+			(* parallel_case *)
+			case (C)
+				A: Y = D;
+				B: Y = E;
+			endcase
+		end
+	end
+endmodule
diff --git a/examples/smtbmc/demo7.v b/examples/smtbmc/demo7.v
new file mode 100644
index 00000000..75b3865c
--- /dev/null
+++ b/examples/smtbmc/demo7.v
@@ -0,0 +1,18 @@
+// Demo for memory initialization
+
+module demo7 (input [2:0] addr);
+	reg [15:0] memory [0:7];
+
+	initial begin
+		memory[0] = 1331;
+		memory[1] = 1331 + 1;
+		memory[2] = 1331 + 2;
+		memory[3] = 1331 + 4;
+		memory[4] = 1331 + 8;
+		memory[5] = 1331 + 16;
+		memory[6] = 1331 + 32;
+		memory[7] = 1331 + 64;
+	end
+
+	assert property (1000 < memory[addr] && memory[addr] < 2000);
+endmodule