blob: 0cf529a4298b5f0e8928e675c4b8ba92efd7f967 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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 @(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
|
