Assertion with variable declaration in SVA

SystemVerilog
1

How to implement variable delay in SV?
condition : ##[a:b] when a and b are variables?

eg: first_match((a && $fell(sig2)), delay1=TMAX, delay2=TMIN) |=>

(need to implement delay between TMIN and TMAX,both are variables)

2

In reply to christin kripa John:
The easiest solution is explained in my paper

Dynamic delays and repeats
ISSUE: Using dynamic values for delays or repeats is illegal in SVA; how can this be easily resolved?
int dly1=2, dly2=7; // module variables
ap_abc_delay: assert property($rose(a) ##dly1 b |-> ##dly2 c); // ILLEGAL SVA
ap_abc_repeat: assert property($rose(a) |-> b[*dly1] ##1 c); // ILLEGAL SVA
SOLUTION: The concept is very simple, the repeat or delay sequence is saved in a package with two defined sequence declarations that include arguments.
http://SystemVerilog.us/vf/sva_delay_repeat_pkg.sv


package sva_delay_repeat_pkg;
 sequence dynamic_repeat(q_s, count);
 int v=count;
 (1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
 endsequence

 sequence dynamic_delay(count);
 int v;
 (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
 endsequence
endpackage
// The package can be applied as follows:
// SystemVerilog.us/vf/sva_delay_repeat.sv
import sva_delay_repeat_pkg::*;
module top;
 timeunit 1ns; timeprecision 100ps;
 bit clk, a, b, c=1;
 int r=2;
 default clocking @(posedge clk); endclocking
 sequence q1; a ##1 b; endsequence
 ap_abr: assert property(a |-> dynamic_repeat(q1, r) ##1 c);
 ap_delay:assert property(a |-> dynamic_delay(r) ##0 b);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    FREE BOOK: Component Design by Example
    … A Step-by-Step Process Using VHDL with UART as Vehicle
    http://systemverilog.us/cmpts_free.pdf
3

In reply to ben@SystemVerilog.us:

Here,both the delay values are variables.(variables get value only after a function call)
How can we write a simple assertion on this?

4

In reply to christin kripa John:
In my SVA book I provide th following solutions:

 
11.4.2 Range delay (e.g., ##[2:v] b
The first element of the range must be a constant, and cannot be a variable. The second element is a variable. Below is an equivalent assertion for : // /11.4/m5067_gen_options.sv
ap_range_fix: assert property($rose(a) |-> ##[N:v] b);
property p_range_equivalent; // Equivalent implementation
int local_v; // this is an internal local variable defined by the tool
  $rose(a) |-> (1, local_v = v-N)
  ##N 1'b1 ##0 first_match((1, local_v=local_v - 1)[*0:$] ##1 (b || local_v<=0))
  ##0 b;
endproperty
ap_range_equivalent: assert property(p_range_equivalent);
// generate option
generate for (genvar g_i=0; (g_i<8); g_i++) begin
  if (g_i >= N)
  ap_range_gen: assert property (v==g_i && $rose(a) |-> ##[N:g_i] b);
end endgenerate

Also, read my article in
verificationacademy.com/news/verification-horizons-march-2018-issue

For your problem, the following works and is tested with the below code using static values for the range.


    property p1; 
        int v_r1, v_r2, v_diff;
        ($rose(a), v_r1=r1, v_r2=r2, v_diff = v_r2 - v_r1) |-> 
        dynamic_delay(v_r1)  ##0  
        first_match((1, v_diff=v_diff - 1)[*0:$] ##1 (b || v_diff<=0))
        ##0 b;
    endproperty  
    a_p1: assert property(@ (posedge clk) p1);

testbench


package sva_delay_repeat_pkg;
    sequence dynamic_repeat(q_s, count);
    int v=count;
    (1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
    endsequence
    
    sequence dynamic_delay(count);
    int v;
    (1, v=count) ##0 first_match((1, v=v-1'b1) [*0:$] ##1 v<=0);
    endsequence
   endpackage
   // The package can be applied as follows:
   // SystemVerilog.us/vf/sva_delay_repeat.sv
   


import uvm_pkg::*; `include "uvm_macros.svh" 
import sva_delay_repeat_pkg::*;
module top; 
  timeunit 1ns;     timeprecision 100ps;    
    bit clk, a, b, c, d; 
    int r1=2, r2=5; 
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk; 
    /* 
    11.4.2 Range delay (e.g., ##[2:v] b
The first element of the range must be a constant, and cannot be a variable. The second element is a variable. Below is an equivalent assertion for : // /11.4/m5067_gen_options.sv
ap_range_fix: assert property($rose(a) |-> ##[N:v] b);
property p_range_equivalent; // Equivalent implementation
int local_v; // this is an internal local variable defined by the tool
$rose(a) |-> (1, local_v = v-N)
##N 1'b1 ##0 first_match((1, local_v=local_v - 1)[*0:$] ##1 (b || local_v<=0))
##0 b;
endproperty
ap_range_equivalent: assert property(p_range_equivalent);
generate option
generate for (genvar g_i=0; (g_i<8); g_i++) begin
if (g_i >= N)
ap_range_gen: assert property (v==g_i && $rose(a) |-> ##[N:g_i] b);
end endgenerate  */
    property p1; 
        int v_r1, v_r2, v_diff;
        ($rose(a), v_r1=r1, v_r2=r2, v_diff = v_r2 - v_r1) |-> 
        dynamic_delay(v_r1)  ##0  
        first_match((1, v_diff=v_diff - 1)[*0:$] ##1 (b || v_diff<=0))
        ##0 b;
    endproperty  
    a_p1: assert property(@ (posedge clk) p1);  
    a_p2: assert property(@ (posedge clk) $rose(a) |-> ##[2:5] b );  
    
    initial begin 
       bit va, vb; 
      repeat(200) begin 
        @(posedge clk);   
        if (!randomize(va, vb)  with 
        { va dist {1'b1:=1, 1'b0:=3};
          vb dist {1'b1:=1, 1'b0:=2};      
      }) `uvm_error("MYERR", "This is a randomize error")
       a <= va; 
       b <= vb;
    end 
    $stop; 
  end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    FREE BOOK: Component Design by Example
    … A Step-by-Step Process Using VHDL with UART as Vehicle
    http://systemverilog.us/cmpts_free.pdf
5

My requirment is this. But i am getting error
int width=10;
property abc;
@posedge clk
$rose(a)|=> $stable(a)[*width];
endproperty

6

In reply to kolliparapavankumar:

You should have looked further into my package sva_delay_repeat_range_pkg
https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats


package sva_delay_repeat_range_pkg;
...
     // int d1, d2; 
    // bit a, b, c=1'b1; 
    // sequence q_s; a ##1 c; endsequence  
    // sequence my_sequence; e ##1 d[->1]; endsequence 
//----------------------------------------------------------------
    // ******       DYNAMIC REPEAT q_s[*d1] **********
    // Application:  $rose(a)  |-> q_dynamic_repeat(q_s, d1) ##1 my_sequence;
    sequence q_dynamic_repeat(q_s, count);
        int v=count;
        (1, v=count) ##0 first_match((q_s, v=v-1'b1) [*1:$] ##0 v<=0);
    endsequence
...
endpackage
import uvm_pkg::*; `include "uvm_macros.svh"  
module top; 
    timeunit 1ns;     timeprecision 100ps;  
    bit clk, a, b, c=1, w;   
    int width=10;
 ap_repeat: assert property(@ (posedge clk)    
            $rose(a)|=> q_dynamic_repeat($stable(a), width) );

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
7

Here q_s means is it $stable

8

In reply to kolliparapavankumar:

Yes, an expression is a sequence of 1 cycle.
If the sequence is more than 1 cycle, you will need to define it in a sequence declaration.

9

In reply to kolliparapavankumar:

 
sequence var_width;
    int cnt;
    (req,cnt = 0) //local variables needs to be initialized
    ##1 (req, cnt++)[*1:$]
    ##1 (!req && (cnt == width-1) );
     endsequence: var_width
  
  property chkr;
    @(posedge clk)
    $rose(req) |-> var_width;
  endproperty

This is from an LRM example.
have setup a tb here, use it for testing.