In reply to ben@SystemVerilog.us:
Hi Ben ,
I have enabled the debug mode and i have few observation.
NO,$rose (sar_eoc) modified is in the antecedent. As mentioned above, the intersect starts after the ##1 at
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) → one thread start just after 1 clock cycle on detection of posedge of sar_eoc and it will run based on intersect 1’b1**[1:8]* here for 8 clock cycle , (if i change to 20 thread will finish at 20 clock cycle ).
case: 2 And one place even, there is no toggle in inc and dec, it has triggered .
*it seems, what i asked question looking right here "intersect 1’b1[1:8] , will it start matching just after sar_eoc==1" (in my case )
I guess it is not taking care $rose of (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2])
thus it is triggering case 2 (my assumption )
And from above comment : (a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a ) we have used [=] operator so if anytime inc or dec goes high 2 times continuously it will start intersect which is happening in my case 2 (i guess).
I have attached the waveform :
if you can suggest changes , for after detection of posedge of sar_eoc , if ($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2] (gap between two posedge of non- consecutive of inc or dec should be 8 sampled_monclk ) lock should asserted.
And in the same way
property p_lock_condition_check_unlock_prog_00;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( $rose (o_fll_sar_eoc ) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |->
**##1 ((inc_count==1 ||dec_count==1 ), inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec),$display("\t **time=%t inc_count**= %d, dec_count ",$time,inc_count,dec_count))**[*1:6] ##0
o_fll_lock===(inc_count==2 || dec_count==2);
endproperty
** inc_count and dec_count is always zero in my log even i can see the posedge of fll_inc and dec in my simulation (Seems $rose it is not taking)