SVA- Assertion property modification

SystemVerilog
, ,
1

Hi,

I have written the assertion below.

property p_decr_check_prpty ;
 @(posedge monclk_output_rld) disable iff (!i_en_rld)
  ((i_en_rld == 1'b1) && (dec == 1'b1) &&  (lock == 1|=> (o_prog_out== $past(o_prog_out) - 1'b1)  ;
endproperty

But I want this property to modify and take care the below requirement as well.
** o_prog_out will get decrement by 1 until it reach to (prog_trim - freq_dec).(means once the prog_out will reach to (prog_trim - freq_dec). it should stop the decrement)

Any help will be appreciated

2

In reply to rkg_:


* But I want this property to modify and take care the below requirement as well.
** o_prog_out will get decrement by 1 until it reach to (prog_trim - freq_dec).
(means once the prog_out will reach to (prog_trim - freq_dec). it should stop the decrement) */ 

//[Ben] Additional requirements: After the stop of the decrement, 0_prog_out is stable until cond_finish
// My assumption here on that finish
let cond_finish= ((i_en_rld == 1'b1) && (dec == 1'b1) &&  (lock == 1)); // needs to meet the requirements

property p_decr_check_prpty ;
    @(posedge monclk_output_rld) disable iff (!i_en_rld)
     ((i_en_rld == 1'b1) && (dec == 1'b1) &&  (lock == 1)) |-> 
         ##1 first_match(  (o_prog_out== $past(o_prog_out)-1'b1) [*1:$] 
                           ##0 0_prog_out== (prog_trim - freq_dec)
                         ) 
                    ##1 $stable(0_prog_out)[*1:$] ##0 cond_finish;
endproperty
// Note: The first_match() is needed here because without it, the assertion will never finish. 
//       I am also assuming that there are enough decrements to have (0_prog_out== (prog_trim - freq_dec)) 
//
// Onother option: split this into 2 assertions 
property p_decr_check_prpty ;
    @(posedge monclk_output_rld) disable iff (!i_en_rld)
     ((i_en_rld == 1'b1) && (dec == 1'b1) &&  (lock == 1)) |-> 
                 ##1  (o_prog_out== $past(o_prog_out)-1'b1) [*1:$] 
                  ##0 0_prog_out== (prog_trim - freq_dec );
endproperty

property p_decr_check_prpty_stable ;
    @(posedge monclk_output_rld) disable iff (!i_en_rld)
             0_prog_out== (prog_trim - freq_dec) |-> 
                    ##1 $stable(0_prog_out)[*1:$] ##0 cond_finish;
endproperty

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) Amazon.com
  3. Papers: