Systemverilog assertion - How do I check the stable signal after implication operator?

In reply to kddholak:

In reply to UVM_LOVE:


$rose(reset)[->1] is equivalent to  !reset[*0:$] ##1 $rose(reset)

What is the difference between
fell(reset) |-> ##[0:1] idle ##0 idle[*0:] intersect !reset[*0:$] ##1 $rose(reset);
and
fell(reset) |-> ##[0:1] idle idle ##[0:] intersect !reset[*0:$] ##1 $rose(reset); ?

I’m confused between “idle[*0:]" and "idle ##[0:]”.

idle[*0:$] can be interpreted as (idle ##1) (idle ##1 idle ##1) (idle ##1 idle ##1 idle ##1)…

idle ##[0:$] can be interpreted as (idle ##0) (idle ##1 idle ##1) (idle ##1 idle ##1 idle ##1)…