SVA: Package for dynamic and range delays and repeats

SystemVerilog
,
7

In reply to ben@SystemVerilog.us:

Here is a workaround for dynamic delays to be used for formal verification:



module top; 
    import uvm_pkg::*; `include "uvm_macros.svh" 
    import sva_delay_repeat_range_pkg::*;
    timeunit 1ns;     timeprecision 100ps;  
    bit clk, a, b, c=1, w;  
    bit[1:0] v=2;  
       
    initial forever #10 clk=!clk;  
    
    // ******       DYNAMIC DELAY ##v **********
    // Application:  $rose(a)  |-> q_dynamic_delay(v) ##0 my_sequence;
    ap_dyn_delay: assert property(@ (posedge clk) 
       $rose(a) |-> q_dynamic_delay(v) ##0 b);  
    
    ap_fix_delay2: assert property(@ (posedge clk)   
       $rose(a) |-> ##2 b); 

    // For formal verification
    generate for (genvar i=0; i<=3; i++)
        begin 
            ap_fvi: assert property(@ (posedge clk) 
               v==i && $rose(a) |-> ##i b);  
        end
    endgenerate

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/