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
30
31
32
33
34
35
36
37
|
logger -expect-no-warnings
read_verilog -formal <<EOT
module top(input clk);
reg signed [3:0] value = -1;
reg ready = 0;
always @(posedge clk) begin
if (ready)
assert ($past(value) == -1);
ready <= 1;
end
endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk
design -reset
read_verilog -formal <<EOT
module top(input clk);
reg signed [3:0] value = -1;
reg ready = 0;
always @(posedge clk) begin
if (ready)
assert ($past(value + 4'b0000) == 15);
ready <= 1;
end
endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk
|
