In reply to ben@SystemVerilog.us:
Thanks for detailed description.
Just last doubt regarding this assertion.
How to modify this assertion so that intersect event(isct0) should only active after the first posedge of inc or dec.
Specification says : lock should only asserted only when (eoc ==1) and two non consecutive posedge of inc or dec anytime after when (eoc =1) and length or gap between two non cosecutive posedge of inc or dec should be 1 to 8 clock cycle of sampled monclk. if length is more then 8 and if lock get asserted it should fail.
property p_lock_condition_check_unlock_prog_01;
@(posedge sampled_monclk) disable iff (!i_en_fll)
(($rose(o_fll_sar_eoc) && i_fll_unlock_prog == 2'b01 ),gen_e(0)) |->
##1(1, gen_e(1)) ##0 ((($rose(o_fll_inc)[=2],gen_e(2)) or ($rose(fll_dec)[=2],gen_e(2))) intersect (1, gen_e(3)) ##0 1[*1:8]) ##0 (o_fll_lock,gen_e(4));
endproperty
waveform :
