Difference in output using ##[0:$] $rose( b ) V/S $rose( b )[->1]

SystemVerilog
,
3

In reply to ben@SystemVerilog.us:

Thanks Ben,
So essentially the consequent is expanded to :


##0 $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or
##1 $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or
##2 $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or
..............................................  or 
##N $rose(b) ##0 ( ($realtime - a_rose) > 2ns ) or

At time:5 since expression:( ($realtime - a_rose) > 2ns ) isn’t true , it keeps on checking the other remaining sequences.As a result no failure at time:5

I then changed property to:


property a_to_b_rise;
    realtime a_rose;
  @(posedge clk) disable iff (!rst_n)
    ($rose(a), a_rose = $realtime) |-> first_match( ##[0:$] $rose(b) ) ##0 ( ($realtime - a_rose) > 2ns ); 
 endproperty

This works as per intention