Added examples/smtbmc/demo2.v

3 files changed, 45 insertions, 3 deletions

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index 4a154c2f9..649c3f69b 100644
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -1,13 +1,24 @@
 
+all: demo1 demo2
+
 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-vlogtb demo2_tb.v demo2.smt2
+	iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
+	vvp demo2_tb +vcd=demo2_tb.vcd
+
 demo1.smt2: demo1.v
-	yosys -p 'read_verilog -formal demo1.v; prep -top demo1; write_smt2 -wires -mem -bv demo1.smt2'
+	yosys -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2'
+
+demo2.smt2: demo2.v
+	yosys -p 'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires -mem -bv demo2.smt2'
 
 clean:
-	rm -f demo1.smt2
+	rm -f demo1.smt2 demo1.vcd
+	rm -f demo2.smt2 demo2.vcd demo2_tb.v demo2_tb demo2_tb.vcd
 
 .PHONY: demo1 clean
 
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
index b1e505bdd..323e6c29c 100644
--- a/examples/smtbmc/demo1.v
+++ b/examples/smtbmc/demo1.v
@@ -6,10 +6,12 @@ module demo1(input clk, input addtwo, output iseven);
 
 	always @(posedge clk)
 		cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
-	
+
+`ifdef FORMAL
 	assert property (cnt != 15);
 	initial assume (!cnt[3] && !cnt[0]);
 	// initial predict ((iseven && addtwo) || cnt == 9);
+`endif
 endmodule
 
 module inc(input addtwo, output iseven, input [3:0] a, output [3:0] y);
diff --git a/examples/smtbmc/demo2.v b/examples/smtbmc/demo2.v
new file mode 100644
index 000000000..34745e898
--- /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