In reply to emin:
Hi Ben,
Property :-
// 1st requirement (fll_lock_assertion):- FLL LOCK is asserted on detecting two positive edges
// of FLL INC or FLL DEC only when (fll_sar_eoc == 1). and fll_inc or fll_dec anytime after (sar_eoc==1) but once any thing (posedge of dec or inc) comes second comes between 1 to 8 (since prog_unlock is 1 here) then only lock should asserted.
// and two positive edge of fll_inc or fll_dec (consecutive is not necessary )
//between 1 to 6 clock cycle of sampled_clk
Type - 1
property p_lock_condition_check_unlock_prog_01;
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( o_fll_sar_eoc == 1 && i_fll_unlock_prog == 2'b01, inc_count=0, dec_count=0 ) |=>
(1, inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec))[*1:8] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
Problem 1 :-lock is asserted after 22 clk cycle of sample_monclk. and above assertion is not able to caught. (marked in purple)
Problem 2 :- assertion failing after de-assertion of lock. (marked in red )
problem 3:- Unexpected triggered (marked in blue colour)
waveform attached.
Type -2 :
property p_lock_condition_check_unlock_prog_01;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (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;
endproperty
Problem -1 :- Assertion triggered but it start checking fll_inc or fll_dec right after the sar_eoc assertion till the 1 to 8 clock cycle of sample clk (instead it should wait and check fll_inc or fll_dec anytime after (sar_eoc==1) but once any thing (two posedge of dec or inc whoever come early ) between 1 to 8 of sample_monclk (since prog_unlock is 1 here) then only lock should asserted.[/b])
Waveform :-
do you see any issue ?