In reply to ben@SystemVerilog.us:
Hi Ben,
As you asked,
What is the issue?
// DO you want this? ---> **i want this**
( (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;
// OR this "intersect 1'b1[*1:8] , will it start matching just after sar_eoc==1"
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 ) |->
(($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
##0 o_fll_lock;
http://systemverilog.us/vf/your_screen.png → In this snippet,(at your green arrow marker ) why is assertion is getting triggered since I do not see two non-consecutive inc or dec.
I am writing assertion to check lock is happening only if two posedge of inc or dec (means only two non consecutive ) and gap between two posedge inc or dec is 1 to 8 cycle of sample_monclk.