Assertion Check

SystemVerilog
, ,
12

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
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. 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
  3. Papers: