SystemVerilog assertion scheduling

Question

A SystemVerilog assertion is latching the previous values even though the transition is detected.

I have the below property as part of the file. a and b are inputs whose width is 1-bit.

property p_sig_detect();
    @(a,b)
    (a == 1) -> (b == 1);
endproperty

a_sig_detect : assert property(p_sig_detect());

In the above code, the assertion is behaving like below:

  1. At 0 ,    a = 0,       b = 0 (initial state)  --> No effect
  2. At t1,    a = 0->1,    b = 0                  --> Passing
  3. At t2,    a = 1,       b = 0->1               --> Throwing Error saying that "b" is 0
  4. At t3,    a = 1,       b = 1->0               --> Passing
  5. At t4&t5, a = 1->0->1, b = 0                  --> Throwing Error once a becomes 1 at t5

Can someone please explain why it's latching the previous value even though the transition is detected?

Answer 1

The sampled values used in a synchronous assertion are the values in the preponed region before the clocking event.

You should be using immediate or deferred assertions that do not use clocks or sample values instead of concurrent assertions and properties that do.

module top;
  bit a,b;
  
  initial begin
    #1 a = 1;
    #1 b-= 1;
    #1 a = 0;
    #1 b = 0;
    #1 $finish;
  end
  
  let p_sig_detect = (a == 1) -> (b == 1);

  always_comb
    a_sig_detect : assert (p_sig_detect()) $info("pass"); else $error("fail");
endmodule