Variable delay in assertion

Is there any method to apply variable delay in assertion

like signal_a |-> #Delay signal_a where delay will be coming from some parameter value.So each time parameter is changed the changed delay is applied.

I have used the following code for this :

property p(o_clk_en,reset_b) ;
    int v_cnt;                                         // local variable which store value of delay      
    bit prev_a;                                        // local variable which store input value
    @(posedge clk) disable iff (~reset_b)
        //   $rose(i_rst_b) |-> ##2 o_clk_en 
       //    ($rose(o_clk_en[0]) ,v_cnt=0) |=> first_match((1'b1,v_cnt=v_cnt+1)[*1:$] ##0 (v_cnt==div_value));*/
        o_clk_en[3] |-> ##5 o_clk_en[3] ;
                                                                                   

  //    ((o_clk_en[3] == 0 || o_clk_en[3] == 1), prev_a = o_clk_en[3], v_cnt=delay+1'b1 ) |-> ((v_cnt != 0 && v_cnt > 0) , v_cnt=v_cnt-1'b1)[*1:$] ##1 (v_cnt == 0) ##0 (o_clk_en[3] == prev_a);

endproperty

BUT IT IS NOT WORKING.

In reply to prashantk:

The codes :-

(rose(o_clk_en[0]) ,v_cnt=0) |=> first_match((1'b1,v_cnt=v_cnt+1)[*1:] ##0 (v_cnt==div_value));

and

((o_clk_en[3] == 0 || o_clk_en[3] == 1), prev_a = o_clk_en[3], v_cnt=delay+1’b1 ) |-> ((v_cnt != 0 && v_cnt > 0) , v_cnt=v_cnt-1’b1)[*1:$] ##1 (v_cnt == 0) ##0 (o_clk_en[3] == prev_a)

are not working

In reply to prashantk:
There are two issues to discuss with your proposed solutions. Rather than discussing your exact code, let me provide an explanation, as defined in my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
For Simple delay (e.g., ##v b), I propose two solutions, one for the general case, and one where the variable “v” is limitied in range, like up to 16.


// General case
bit[2:0] v=3;
default clocking @(posedge clk); endclocking
ap_delay_desired: assert property( $rose(a) |-> ##v b); // ILLEGAL in 1800'2012 
property p_delay_equivalent; // Equivalent implementation
  int local_v; //  
  $rose(a) |-> 
   (1, local_v = v) ##0 first_match((1, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
   ##0 b;
endproperty
ap_delay_equivalent: assert property(p_delay_equivalent);

/* If the variable used to define the delay has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item. Example: */
generate for (genvar g_i=0; g_i<8; g_i++) begin
  ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate
 

In your example, I fal to understand uour use of the “and” of 2 properties.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us


In reply to ben@SystemVerilog.us:

Thanks for the reply ben,

actully I was trying to implement signal_a |-> #Delay signal_a .Now as SVA does not allow variable delay , so I tried to use either of the two codes (which will be equivalent to signal_a |-> #Delay signal_a ) I posted earlier. And in my case the delay part is fixed that will be coming from parameter , so it doesn’t have any range.

One more question can we apply for loop in assertions as you have used ,because we need static variables in assertions and for loop creates dynamic variables.

WAITING FOR YOUR REPLY.THANKS

In reply to prashantk:

In reply to ben@SystemVerilog.us:
actually I was trying to implement signal_a |-> #Delay signal_a .Now as SVA does not allow variable delay , so I tried to use either of the two codes (which will be equivalent to signal_a |-> #Delay signal_a ) I posted earlier. And in my case the delay part is fixed that will be coming from parameter , so it doesn’t have any range.

[Ben] If your delay size is from a parameter, then you can use that parameter directly. Thus, with parameters,

parameer delay=3; 
signal_a |-> ##delay signal_a  // LEGAL  

SVA requires that the value of the delay size (or repeat size) be static after elaboration.
However, if the delay is dynamic, in that it can change during simulation, then you can us the methods I outlined above.

One more question can we apply for loop in assertions as you have used ,because we need static variables in assertions and for loop creates dynamic variables.

[Ben] What I used is a generate loop that is expanded at elaboration time, and thus create static values for the g_i.
You can use regular for loops, but the loop variable is not used for delays or repeat sizes. For example,


always @(posedge clk) begin : alw_foo
  automatic logic k=1'b0; // automatic, evaluated in the Active region
  static logic m=1'b1; // static, evaluated in the Preponed region
  // k <= !k; //  non-blocking assignment may not be on an automatic variable
  k = !k; // OK
  //  int i variable declared in the loop is automatic
  for (int i=0; i<10; i++)
    a4: assert property (foo[i] && bar[i]);
  ap_k: assert property(k);
end : alw_foo 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us