Using property expression : !a[*0:$] |=> b

Hello Forum ,
I am trying the following concurrent assertion

 bit  clk , a , b ;
 always #5 clk = !clk;
 ap1:assert property( @(posedge clk) !a[*0:$] |=> b ) 
            $display("T:%0t Pass",$time); else  $display("T:%0t Fails",$time);
  initial  begin
    #4 ; b = 1 ;
    #20; a = 1 ;
    #2 ; $finish();

My expected output is 3 pass reports at time:25 whereas currently the closest matching output ( as it varies across tools ) I observe is 2 pass reports at time:25

Both the 1st attempt at time:5 and 2nd attempt at time:15 result in pass at time:25 as ‘a’ is true (1) .

For the 3rd attempt at time:25 as ( 1 |-> b ) matches.
Remaining antecedent sequence ( !a[*1:$] ## 1 1 ) ends ( i.e vacuous pass ) at time:25 ( due to ‘a’ == 1 ), hence I expected a 3rd pass report at time:25

Any thoughts / suggestions are welcome

By default, some tools may not display vacuous passes. There are some switches to do so.

Hi Ben,

By default, some tools may not display vacuous passes. There are some switches to do so.

I believe by default a vacuous pass doesn’t trigger the pass action block. ( 3 tools on edaplayground agree )

For the 3rd attempt at T:25 there is a non-vacuous pass via ( 1 |->b ),
so shouldn’t the pass action block execute ?
The other threads in the 3rd attempt have a vacuous pass due to ‘a’ being sampled high.
Thus the 3rd attempt starts and ends at time:25 itself

As per LRM, it should trigger - not the best use of that feature, hence tools tend to shut that down by default. Verilator and one other simulator agrees with that. I guess the 3 simulators you mentioned have some way to turn it on (for sure one has).

As per LRM, it should trigger

Could you please suggest the LRM section for the above quote.

I was referring to thread where Dave’s comments were inline with my observation on tool’s output for ::

ap2:assert property( @(posedge clk) 0 |-> 1 )  $display("PASS");

When tested on eda as well the licensed tools at work , 3 tools don’t execute the pass action block

Similarly in the case of ‘ap1’ I believe the pass action block executes only due to non-vacuous pass.
For each of the 3 attempts none of the threads fail and there is at least 1 non-vacuous pass.
The confusion is whether the pass action block should execute thrice or twice at time:25