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

SystemVerilog
,
11

In reply to Have_A_Doubt:

In reply to UVM_LOVE:
Using $stable :


sequence  stable_seq ;
$stable(idle) throughout $rose(reset)[->1] ;
endsequence
property reset_chk0_p;                                         
@(posedge clk) $fell(reset) |-> ##[0:1] idle ##1 stable_seq ; 
endproperty
// We use ##1 stable_seq  instead of  ##0 stable_seq  as idle could have changed at same clock as $fell(reset) is True OR 1 clock after $fell(reset) is True.
// Hence $stable(idle) would be False in these 2 cases had we used  ##0 stable_seq

Can’t implement like this instead of using the sequence?

property CHK03;                                              
@(posedge clk)                                               
  //$fell(reset) |-> ##[1:2] idle[*0:$] ##1 $rose(reset);    
  $fell(reset) |-> ##[1:2] idle ##1 $stable(idle) throughout  $rose(reset);
endproperty                                                  
                                                             
CHK03_P : assert property (CHK03);