Quoting from a book "Systemverilog Assertions and Functional Coverage", Ashok Mehta on page 42,
@ (posedge clk) a |=> !a; In the above sequence, let us say that variable ‘a’ changes to ‘1’ the same time that the sampling edge clock goes posedge clk (and assume ‘a’ was ‘0’ before it went to a ‘1’). Will there be a match of the antecedent ‘a’? No! Since a’ went from ‘0’ to ‘1’ the same time that clock went posedge clk, the value of ‘a’ sampled by clock will be ‘0’ (preponed region) and not ‘1’. This will not cause the property to trigger because the antecedent is not evaluated to be true. This will confuse you during debug. You would expect ‘1’ to be sampled and the property triggered thereof. However, you will get just the opposite result. This is a very important point to understand because in a simulation waveform (or for that matter with Verilog $monitor or $strobe) you will see a ‘1’ on ‘a’ with posedge clk and would not understand why the property did not fire or why it failed (or passed for that matter). Always remember that at the sampling edge, the ‘previous’ value (i.e. a delta before the sampling edge in the preponed region) of the sampled variable is used.
I tried to test this scenario by this Testbench. However I expected assertion to FAIL at simulation times #10, #50, #90
module assert_immediate();
reg a,b,clk;
initial
begin
clk = 0;
forever #10 clk = !clk;
end
initial
begin
a = 0;
b = 0;
repeat (10) @(posedge clk) a = ~a;
end
// always@(posedge clk) $display("a = %d at time %t \n", a, $time);
property p1;
@(posedge clk) a |=> !a;
endproperty
initial #100 $finish;
assert property (p1) $display("Entered assert at %t \n", $time); else $display("FAIL at %t \n", $time);
cover property (p1) $display("PASS at %t \n", $time);
endmodule
But when I ran on EDAPlayground using VCS, I got a different behavior
# KERNEL: Entered assert at 10
# KERNEL:
# KERNEL: PASS at 10
# KERNEL:
# KERNEL: Entered assert at 50
# KERNEL:
# KERNEL: Entered assert at 50
# KERNEL:
# KERNEL: PASS at 50
# KERNEL:
# KERNEL: PASS at 50
# KERNEL:
# KERNEL: Entered assert at 90
# KERNEL:
# KERNEL: Entered assert at 90
# KERNEL:
# KERNEL: PASS at 90
# KERNEL:
# KERNEL: PASS at 90
Entered assert at 10
andPASS at 10
should not be printed. – Shankhadeep Mukerjipreponed
region and hence@10
, the sampled value of a should be0
. – Karan Shah