Unexpected SVA assertion behavior for a periodic signal

Question

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

Answer 1

I think that there are 2 issues there.

1. I think that there is a misconception in the implication operator. Assertion should not fail in your case. The implication allows for the right hand side expression to be true eventually. So, if a goes up, it will eventually go down. So, at #50 it goes down after sampled high at #30, and this cause the assertion to pass, and go to the next cycle of evaluation: #70 -> #90.

For each successful match of the antecedent sequence_expr, the consequent property_expr isseparately evaluated. The end point of the match of the antecedent sequence_expr is the start pointof the evaluation of the consequent property_expr.

2. there is a bug in the compiler you use. There should be no assertion message at time #10. I tried it with vcs 2017.03 and it worked correctly.

also you can add this line to you code to get some debugging prints:

always @(posedge clk) $display("%0t a = %b", $time, $sampled(a));

I got these results during the simulation:

10 a = 0
30 a = 1
50 a = 0
Entered assert at 50
PASS at           50
70 a = 1
90 a = 0
Entered assert at 90
PASS at           90