Assertion Check

In reply to rkg_:


( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock;
// Rearranging the ()s
      antecedent |-> 
         ##1 ( (a_sequence or b_sequence) intersect 1'b1[*1:8]
             )
         ##0 o_fll_lock;
 
// Thus, in 
               ($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8]
// the following two threads start at the same cycle 
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) // One thread 
1'b1[*1:8]                                   // a parallel thread

intersect 1’b1[*1:8] , will it start matching just after sar_eoc==1. is it correct understanding ?

NO, sar_eoc==1 is in the antecedent. As mentioned above, the intersect starts after the ##1 at
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2])

Ben