examples/smtbmc/demo2.v

   1 // Nothing to prove in this demo.
   2 // Just an example for memories, vcd dumps and vlog testbench dumps.
   3
   4 `ifdef FORMAL
   5 `define assume(_expr_) assume(_expr_)
   6 `else
   7 `define assume(_expr_)
   8 `endif
   9
  10 module demo2(input clk, input [4:0] addr, output reg [31:0] data);
  11         reg [31:0] mem [0:31];
  12         always @(negedge clk)
  13                 data <= mem[addr];
  14
  15         reg [31:0] used_addr = 0;
  16         reg [31:0] used_dbits = 0;
  17         reg initstate = 1;
  18
  19         always @(posedge clk) begin
  20                 initstate <= 0;
  21                 `assume(!used_addr[addr]);
  22                 used_addr[addr] <= 1;
  23                 if (!initstate) begin
  24                         `assume(data != 0);
  25                         `assume((used_dbits & data) == 0);
  26                         used_dbits <= used_dbits | data;
  27                 end
  28         end
  29 endmodule