examples/smtbmc/demo3.v

   1 // Whatever the initial content of this memory is at reset, it will never change
   2 // see demo3.smtc for assumptions and assertions
   3
   4 module demo3(input clk, rst, input [15:0] addr, output reg [31:0] data);
   5         reg [31:0] mem [0:2**16-1];
   6         reg [15:0] addr_q;
   7
   8         always @(posedge clk) begin
   9                 if (rst) begin
  10                         data <= mem[0] ^ 123456789;
  11                         addr_q <= 0;
  12                 end else begin
  13                         mem[addr_q] <= data ^ 123456789;
  14                         data <= mem[addr] ^ 123456789;
  15                         addr_q <= addr;
  16                 end
  17         end
  18 endmodule