[Assertion] Dynamic Repetition

SystemVerilog
1

As in a below screenshot, the signal B is driven by DUT based on the config values where we have dynamic delays as well as repetitions (total iterations). The random delays are taken care in the assertion below, but need help to code dynamic repetition.

I want to replace “CFG2_s ##0 CFG3_s ##0 CFG2_s ##0 CFG3_s” in property with something like, “(CFG2_s ##0 CFG3_s)[*CFG4]”.

Screenshot:

1020×280 36.8 KB

Code without dynamic repetition:

// Get Delay (num of clocks)
function int delay(logic[15:0] t);
  real res;
  case(CFG5) // unit: us
    0: res=0.01;
    1: res=0.1;
    2: res=1;
    3: res=10;
  endcase
  delay=(t*res*100); // convert to 10ns unit (1 CLK)
endfunction // delay

// CFG1: initial delay between A and B
sequence CFG1_s;
  int count;
  ($rose(A),count=0) ##0 (count<delay(CFG1),count+=1)[*] ##1 (count==delay(CFG1)) && $rose(B);
endsequence // CFG1_s

// CFG2: negative level of B
sequence CFG2_s(bit last=0);
  int count;
  ($fell(B),count=0) ##0 (count<delay(CFG2),count+=1)[*] ##1 (count==delay(CFG2)) && (!last)? $rose(B) : $rose(C);
endsequence // CFG2_s

// CFG3: positive level of B
sequence CFG3_s;
  int count;
  ($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##1 (count==delay(CFG3)) && $fell(B);
endsequence // CFG3_s

// Property to check A -> B -> C transition
property P1;
  @(posedge CLK) CFG1_s |-> ##1 CFG2_s ##0 CFG3_s ##0 CFG2_s ##0 CFG3_s ##0 CFG2_s(1);
endproperty // P1

check_B: assert property(P1);
2

In reply to bdreku:

Take a look at my package on this subject
https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
** 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) https://rb.gy/cwy7nb
  3. Papers:
3

In reply to ben@SystemVerilog.us:
Thanks Ben.

The repetition operator checks whether a signal or a sequence repeats for given number of clock cycles.

so the (seq1 ##0 seq2)[*3] is expanded as,

(seq1 ##0 seq2) ##1 (seq1 ##0 seq2) ##1 (seq1 ##0 seq2).

But as my both the sequences advances with clock, is it ever possible to have repetition after ##0 delay instead of ##1 ?

for exa, can we use repetition operator for the following series of sequences?

(seq1 ##0 seq2) ##0 (seq1 ##0 seq2) ##0 (seq1 ##0 seq2)

PS: Theoretically this requirement doesn’t make any sense, so planning to modify the sequences to adopt the ##1 repetition delay, but being a lazy coder, just want to check if it’s possible in any case.

4

In reply to bdreku:
It is possible to do what you want in SystemVerilog, but not in SVA.
Specifically, you want something like


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    bit clk, r, a=1, b=1, c=1, d=1;   
    int rpt=3, thread;
    event e_pass, e_fail, e_abcd, e_done, e_clk;  // for debug  
    let tID="My model"; 
    
    initial forever #10 clk=!clk;  
    sequence seq1; @(posedge clk) a ##1 b; endsequence 
    sequence seq2; @(posedge clk) c ##2 d; endsequence      
    
    ap_r : assert property(@(posedge clk) $rose(r) |->  
       (seq1 ##0 seq2) ##0 (seq1 ##0 seq2) ##0 (seq1 ##0 seq2));
    // Action block is not used here 

    // (seq1 ##0 seq2) ##0 (seq1 ##0 seq2) ##0 (seq1 ##0 seq2)
    task automatic t_abcd(int count); // 
       bit match=1'b1; 
       int my_thread;
       my_thread=thread; thread+=1; 
        -> e_abcd;
       repeat(count) begin : rpt1  // seq1; va ##1 b;
         //seq1:  a ##1 b
         if(match && a) match=1'b1; 
         else begin match=1'b0; disable rpt1; end 
         @(posedge clk) if(match && b) match=1'b1; 
         else begin match=1'b0; disable rpt1; end 
         // ##0 seq2: c ##2 d;
         if(match && c) match=1'b1; 
         else begin match=1'b0; disable rpt1; end 
         @(posedge clk); -> e_clk; 
         @(posedge clk);
         if(match && d) match=1'b1; 
         else begin match=1'b0; disable rpt1; end 
       end : rpt1  
       ai_3sq: assert(match) else
        `uvm_error(tID,$sformatf("%m : t_abcd FAIL, my_thread=%d", my_thread))
        if(match) -> e_pass; else -> e_fail;   
        -> e_done; 
   endtask

   always @(posedge clk) 
     fork 
       if($rose(r)) t_abcd(rpt); 
     join_none


   //ap_r_task : assert property(@(posedge clk) 
   //     $rose(r) |-> (1, t_abcd(rpt)));

 initial begin  
    bit vr, va, vb, vc, vd;
    repeat(40) begin 
    @(posedge clk) if (!randomize(vr)) `uvm_error("MYERR", "This is a randomize error") 
    r <= vr; //
    end 
    repeat(30) begin 
        repeat(2) @(posedge clk);   
        if (!randomize(vr, va, vb, vc, vd)  with 
        { va dist {1'b1:=1, 1'b0:=1};
          vb dist {1'b1:=1, 1'b0:=2};
          vc dist {1'b1:=1, 1'b0:=3};    
          vd dist {1'b1:=1, 1'b0:=1};    
        }) `uvm_error("MYERR", "This is a randomize error") 
        r <= vr; a<=va; b<=vb; c<=vc; d<=vd; 
    end 
    $finish; 
  end 
endmodule

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) https://rb.gy/cwy7nb
  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/

5

In reply to ben@SystemVerilog.us:
Thanks Ben.

This is the long way for a small fix and I doubt the reusability.

However, the assertion works fine after reusing the dynamic repetition sequence from your package example and modifying a sequence and a property as below.


  // Reused Your sequence for dynamic repetition
  sequence q1_rpt_simple_range_q2(sequence q1, int range, sequence q2); 
      int v, diff;
      (1,  diff=range)  ##0  
      first_match((diff>0 ##0 q1, diff=diff-1'b1) [*1:$] ##1 q2 );
  endsequence

  // Modified the sequence and property
  // CFG3: positive level of B
  sequence CFG3_s;
    int count;
    // Older code
    //($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##1 (count==delay(CFG3)) && $fell(B);
    // Modified as
    ($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
  endsequence // CFG3_s
 
  // Property to check A -> B -> C transition
  property P1;
    // Older code
    //@(posedge CLK) CFG1_s |-> ##1 CFG2_s ##0 CFG3_s ##0 CFG2_s ##0 CFG3_s ##0 CFG2_s(1);
    // Modified as
    @(posedge CLK) CFG1_s |-> ##1 q1_rpt_simple_range_q2((CFG2_s ##0 CFG3_s),(CFG5-1),CFG2_s(1));
  endproperty // P1
6

In reply to bdreku:


// I have a comment on your use of
expr[*] ##0 seq //  in 
  ($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
// Specifically, [*] is equivalent to [*0:$].  Consider the following
a ##0 1[*] ##0 b  // same as 
a ##0 1[*0:$] ##0 b  // same as 
a ##0 1[*0] ##0 b or 
a ##0 1[*1] ##0 b or  
...
a ##0 1[*n] ##0 b // n==infinity 
// BUT !!!!!!! 
0 1[*0] ##0 b // is an empty match, by definition
// THUS, 
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*] ##0 (count==delay(CFG3)) && B;
// IS SAME AS 
($rose(B),count=0) ##0 (count<delay(CFG3),count+=1)[*1:$] ##0 (count==delay(CFG3)) && B;

My point:*Avoid structures that include (or infer) seq1[0] ##0 seq2
(where seq is a sequence of one or more terms
It’s a style issue because SVA reflects requirements.
Why do we want to add meaningless requirements?

7

In reply to ben@SystemVerilog.us:
That’s so true, and as I don’t require [0], replaced [] by [*1:$].

Thank you Ben for this valuable feedback. :-)