In reply to rkg_:
See if the following works. Make sure you use the |-> ##1 (consequent)[*n] and NOT the
|-> (##1 consequent)[*n]
module m;
bit[1:0] o_fll_sar_eoc, i_fll_unlock_prog;
bit o_fll_inc, o_fll_lock, sampled_monclk, i_en_fll, fll_dec;
// 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 two positive edge of fll_inc or fll_dec (**consecutive is not necessary )
//between 1 to 6 clock cycle of sampled_clk**
property p_lock_condition_check_unlock_prog_00; // Using |-> ##1 (consequent)
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |->
##1 (1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |=>
(1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0
o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
//---------------------------------------
//2nd requirement (fll_lock de assertion ) :- FLL lock is de-asserted on detecting of four consecutive
// of o_fll_inc signal or fll_dec signal. here the.
// Note :- 1. for requirement two : positive edge is not needed but consecutive of fll_dec or
// fll_inc is must. 1 to 6 clock cycle is **not required**.
property p_unlock_condition_check_unlock_prog_00_v1; // NOT per requirements
int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |->
##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
// does not satisfy "consecutive of fll_dec or fll_inc is must"
!o_fll_lock==(inc_count==4 || dec_count==4)
##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty
// Upon a rose of 0_fll_lock and i_fll_unlock_prog == 2'b00 then
// at anytime thereafter (the ##[1:$]) any 4 sequential occurrence of
// o_fll_inc or 4 sequential occurrence of fll_dec the o_fll_lock==0 at that 4th occurrence
property p_unlock_condition_check_unlock_prog_00_v2; //One option
// int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00) |->
first_match(##[1:$] (o_fll_inc==1)[*4] or (fll_dec==1)[*4]) ##0 !o_fll_lock;
// ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
// does not satisfy "consecutive of fll_dec or fll_inc is must"
// !o_fll_lock==(inc_count==4 || dec_count==4)
// ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty
// If the "at anytime" is constrained to "n" static cycles,
let n=10;
// Upon a rose of 0_fll_lock and i_fll_unlock_prog == 2'b00 then
// at anytime thereafter (the ##[1:$]) any 4 sequential occurrence of
// o_fll_inc or 4 sequential occurrence of fll_dec the o_fll_lock==0 at that 4th occurrence
property p_unlock_condition_check_unlock_prog_00; //One option
// int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00) |->
first_match(##[1:$] (o_fll_inc==1)[*4] or (fll_dec==1)[*4] intersect 1'b1[*n]) ##0 !o_fll_lock;
// ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0
// does not satisfy "consecutive of fll_dec or fll_inc is must"
// !o_fll_lock==(inc_count==4 || dec_count==4)
// ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb - Papers:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy