// 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 @(negedge 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 /td> index : iCE40/yosys [no description]

about summary refs log tree commit diff stats

path: root/examples/smtbmc/demo4.smtc

blob: 2f91f8164a5b6ed7cfe3c78d0e783263a34445ab (plain)