Added examples/smtbmc/demo2.v

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index 4a154c2f9c10c204a630135acb3c88f6fbb27971..649c3f69b8b77f4b8042e8df3b4248b881dd44a9 100644 (file)
--- 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 b1e505bdd6b17967b5ebdc7fa278ff88ff414335..323e6c29cf29f9f551cbf3de48f1fe878d693796 100644 (file)
--- 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 (file)
index 0000000..34745e8
--- /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