Assertion Check

SystemVerilog
, ,
10

In reply to rkg_:
Addressing your second question first
http://systemverilog.us/vf/rpt2.sv

1704×832 161 KB


// After the |-> ##1 the sequence (b} is repeated twice
ap2: assert property(a |-> ##1 (b)[*2]); 

// After the |-> the sequence (##1 b) is repeated twice
ap2_1: assert property(a |-> (##1 b)[*2]);

1704×832 161 KB

what is the use of [*6} ?
for lock de-assertion it can happen at any number of sampled clk unlike lock condition . only thing is four consecutive fll_inc or fll_dec after the lock assertion .

The [*6} came from your original requirements … based on value of a, number of cycle (between 1 to 6 clock cycle of ref_clk)
Also, without a repeat operator how could the local variable inc_count, dec_count ever be ==4? SOmething is missing in your requirements. With poorly expressed requirements, I am doing my best to make assumptions, hoping that you’ll get the idea as to what best todo.
It might be a good idea to express again all the requirements in English.
As to you last comments for lock de-assertion it can happen at any number of sampled clk unlike lock condition . only thing is four consecutive fll_inc or fll_dec after the lock assertion . You could change the property to something like:


// Fix as needed per requirements 
property p_unlock_condition_check_unlock_prog_00; 
        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 
            !o_fll_lock==(inc_count==4 || dec_count==4) 
     ##0 !o_fll_lock[->1]; // if needed

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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: