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

SystemVerilog
, ,
1

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();
  end

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

2

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

3

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

4

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).

5

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