Sva repetition using variable

SystemVerilog
, , ,
1

can i use a variable in repeat operator ?
for example

seq s1;

property check;
@ (posedge clk)
$rose(enable) |-> s1[*no_of_repeatition] |=> $rose(done);
endproperty

2

In reply to bassem yasser:

No. The repeat must be a constant. However… See

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
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf

3

Bringing this thread back to life…I often see the following solution, but I’m not sure how it impacts performance, and I’m pretty sure it won’t scale beyond variables that are a few bit long.

logic clk;
logic req;
logic ack;
logic [3:0] gap;

genvar gap_count;

generate 
   for (gap_count = 0; gap_count<$bits(gap); gap_count++)
       assert property (@(posedge clk) ((gap == gap_count) && req) |-> ##gap_count ack);
endgenerate
4

In reply to avidan.efody:

You can also use my sva package in item 1 in my signature below.
Ben

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

In reply to bassem yasser:


logic s1;
bit[5:0]no_of_repetition;
property check;
int count=0;
@ (posedge clk)
$rose(enable) |-> (s1,count=count+1)[*1:$] ##1 $rose(done) ##0 (count == no_of_repetition);
endproperty

This is what you meant, I reckon.

6

In reply to Shubhabrata:
// Bad assertion
(s1,count=count+1)[*1:$] ##1 $rose(done) ##0 (count == no_of_repetition);
required a first_match because if for example, no_of_repetition==4 and s1==1 for 15 cycles, and done occurs at the 7th cycle, the assertion will fail only when s1==0.

//Corrected assertion 
property check;
int count=0;
@ (posedge clk)
$rose(enable) |-> 
   first_match((s1,count=count+1)[*1:$] ##1 $rose(done)) ##0 (count == no_of_repetition);
endproperty
7

In reply to ben@SystemVerilog.us:

Yup, got it. This assertion will fail because I am highlighting infinite consecutive repetition of signal-s1. For this, we need to use first_match, right? But I have read somewhere probably in some thread here or on any website that we use this construct if this problem occurs on the antecedent side. Could you tell me about this?

Another thing, I just observed. The example you mentioned, according to that assertion will fail at the 7th cycle when done will be asserted. But our requirement is something else, I guess. It’s been said that after 4th cycle assertion should pass.


property check;
int count=0;
@ (posedge clk)
$rose(enable) |-> 
   (s1,count=count+1)[*1:$] ##1(count == no_of_repetition) ##0 $rose(done);
endproperty

I think this one is doable and we don’t need to use first_match.

8

In reply to Shubhabrata:

  • (s1,count=count+1)[*1:$] ##1(count == no_of_repetition) ##0 $rose(done);
    As long as s1==1 and count!= no_of_repetitions and ($rose(done)==1 || rose(done)==0)
    count will increment at every cycle and the assertion will not fail
    You are correct in that there is only one path for a pass.
    With

first_match(s1,count=count+1)[*1:$] ##1(count == no_of_repetition) ##0 $rose(done);

at the very first match of (s1,count=count+1)[*1:$] ##1(count == no_of_repetition) then
if $rose(done) is true assertion PASSes else assertion fails.
No other threads is considered.

  • In my paper Understanding the SVA Engine Using the Fork-Join Model I demonstrated several concepts in how SVA is processed. One important concept was:
    Demonstrated concepts - Multi-threading and need for unique match in antecedents
    The sequence ##[1:n]sequence creates multiple threads. This model demonstrates that for assertions with range delays in antecedents there is a need for a unique match (refer to the_1to5 for Loop). This is because SVA requires that each of the threads of a multithreaded antecedent be tested with its appropriate consequent, and for success, each of those threads must succeed.
    Note that this multithreaded concept is not exclusive to delay ranges, but also apply to repeat ranges.
    For example:
    ap_repeat_1to5b_then_3c : assert property(@(posedge clk) ($rose(a) ##1 b[*1:5] ) |-> ##3 c); // A first_match() is needed in the antecedent
    In many cases, the first_match() function can be avoided with the use of the goto operator ( [->1].
    Understanding the SVA Engine Using the Fork-Join Model

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. Free books:
  1. Papers and publications
    SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II
    Understanding and Using Immediate Assertions
    Understanding and Using Immediate Assertions
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
    SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    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/