Local variable in SVA

SystemVerilog
, , , ,
1

Hi,
I am working on one assertions and I came across some specific requirement.
There is one busy signal in the +ve and -ve edge of busy signal, continually I want to count the number of clock cycle.
So for this I have written the below assertion.
assert property (@(posedge clk) $rose(busy) |-> ##[1:max] $fell (busy))

When in place of max(Variable), I am giving any hardcoded value it is working.
But with max variable it is giving error with
Error-[NCE] Non-constant expression
The following expression should be a constant.
Expression: max

How to correct the above Error or what could be the possible solution for the above requirement?

2

In reply to durgesh01:
See my SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy

module m; 
import sva_delay_repeat_range_pkg::*;
bit busy, clk; 
bit[0:8] max; 

assert property (@(posedge clk) $rose(busy) |-> 
        dynamic_delay_lohi_sq(1, max, $fell (busy)));   //##[1:max] $fell (busy))

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:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    Understanding and Using Immediate Assertions
    Understanding and Using Immediate Assertions | Verification Horizons - December 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    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/
3

In reply to ben@SystemVerilog.us:

Thanks Ben.
This way, I have modified my assertion as below and it is working properly.

sequence s1(d1);
int v;
((1, v=d1) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);
endsequence

sequence s2(e1,maxi,sq);

int v1,diff;
((1,v1=e1,diff=maxi-1) ##0 s1(1) ##0(diff>=0, diff=diff-1) [*1:$] ##0sq);
endsequence
assert property (@(posedge clk) $rose(busy) |-> s2(1, max, $fell(busy)))

Thanks a lot.

4

In reply to durgesh01:

This looks too complex. Have you looked at my options in the package?
What are your requirements? provide an example with fixed variables.
Also, compare your desired implementation against a simpler one with constant changes.

5

In reply to ben@SystemVerilog.us:
In the below URL i have added the screen shot of waveform.
Your text to link here…
Basically I am writing assertion for the performance monitor.
In that busy signal is range and within that range no of clock cycle should not be more than a certain number(different for different test cases).

So for required condition, If no of clock cycle more than range in each block it should give error(X and Y coord are block).
So I have taken rising and falling point of busy. for each cycle of busy it should check.
below assertion working properly if max is defined as parameter.
assert property (@(posedge clk) $rose(busy) |-> ##[1:max] $fell (busy))

But I want to pass max value from run command line(with $value$plusargs), but when I am doing this it is throwing error as below.
Error-[NCE] Non-constant expression
The following expression should be a constant.
Expression: max

Then I used sequence and passing the value as local variable, and came across above assertion.(Mentioned in previous post)

Assertion is working properly but it is too complex. So if with all above requirement kindly provide simple assertion.

Thanks

6

In reply to ben@SystemVerilog.us:

Hi ben ,
Can we go with the following way ?


module test; 
bit busy, clk; 
bit[0:8] max; 
assert property (p1); 

property p1;
int count = 0;
@(posedge clk) $rose(busy) |-> first_match((busy , count = count+1)
        [*1:$] ##1 $fell (busy)) ##0 (count <= max); 
endproperty

endmodule
7

In reply to Shubhabrata:

module m;
// from
// import sva_delay_repeat_range_pkg::*;
bit busy, er, ok, clk;
bit[1:0] max=2'b11;
initial forever #10 clk = !clk;
sequence dynamic_delay(count);
int v;
(count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);
endsequence // dynamic_delay
sequence dynamic_delay_lohi_sq(d1, d2, sq);
int v1, vdiff;
( (1, v1=d1, vdiff=d2-d1) ##0 dynamic_delay(v1)   ##0
(vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq);
endsequence
assert property (@(posedge clk) $rose(busy) |->
dynamic_delay_lohi_sq(1, max, $fell (busy)))  ok=1; else er=1;   //##[1:max] $fell (busy))
initial begin
$dumpfile("dump.vcd"); $dumpvars;
@(posedge clk) busy<= 1'b1;
repeat(3) @(posedge clk);
busy<=1'b0;
repeat(3) @(posedge clk);
$finish;
end
endmodule
  • Your code has errors. This is what you meant
property p_2busy;
int count = 0;
@(posedge clk) $rose(busy) |->
first_match((busy, count = count+1, $display("c=%d", count))[*1:$] ##1 $fell(busy)) ##0 (count <= max);
endproperty
// **** The first_match is not need here, SEE MY LASR RESPONSE
ap_2busy:  assert property(p_2busy) ok2=1; else er2=1;

FUll code + waveforms:

module m; 
    // from 
    // import sva_delay_repeat_range_pkg::*;
     bit busy, er, ok, ok2, er2, clk; 
     bit[1:0] max=2'b11; 
     initial forever #10 clk = !clk;
   
     sequence dynamic_delay(count);
       int v;
     (count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0);
     endsequence // dynamic_delay
   
     sequence dynamic_delay_lohi_sq(d1, d2, sq);
       int v1, vdiff;
         ( (1, v1=d1, vdiff=d2-d1) ##0 dynamic_delay(v1)   ##0     
             (vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq); 
     endsequence
   
    ap_tobusy:  assert property (@(posedge clk) $rose(busy) |-> 
           dynamic_delay_lohi_sq(1, max, $fell (busy)))  ok=1; else er=1;   //##[1:max] $fell (busy))

    property p_2busy; 
        int count = 0;
        @(posedge clk) $rose(busy) |-> 
      first_match((busy, count = count+1, $display("c=%d", count))[*1:$] ##1 $fell(busy)) ##0 (count <= max); 
    endproperty
// the first_match() is needed here to test the count. 
    ap_2busy:  assert property(p_2busy) ok2=1; else er2=1;
   
     initial begin
       $dumpfile("dump.vcd"); $dumpvars;
       @(posedge clk) busy<= 1'b1; 
       repeat(4) @(posedge clk);
       busy<=1'b0; 
       repeat(3) @(posedge clk); 
       //
       repeat(1) @(posedge clk);
       busy<=1'b1; 
       repeat(3) @(posedge clk);
       busy<=1'b0; 
       repeat(3) @(posedge clk); 

       $finish;
      end
   endmodule

// sim 

# c=          1
# c=          2
# c=          3
# c=          4
# c=          1
# c=          2
# c=          3

Code

1270×775 46.7 KB

Ben

8

In reply to ben@SystemVerilog.us:

Hi Ben,

First of all, thank you so much for correcting my code. I thought something but wrote down something else. It was the biggest blunder. The updated form is working, right? I ran it and your solution on eda-playground and I didn’t notice any difference.

Actually, your solution seemed a little bit intricate to me. That’s why I tried to write the assertion with the techniques I have learned.

One more thing, the waveform you shared where your solution and my assumption can be observed clearly, over there I noticed one thing. In my case, ok2 is not exactly presented as ok signal. You also can notice that. Is that any kind of fault or something else?

9

In reply to ben@SystemVerilog.us:

I have another question regarding my code which you corrected. Why did you use first_match ?
I don’t think it was necessary. I mean we are dealing with consecutive repetition and also only one repetition case. So I am not getting the importance of this construct over here?

10

In reply to Shubhabrata:

In reply to ben@SystemVerilog.us:
…The updated form is working, right? I ran it and your solution on eda-playground and I didn’t notice any difference.

Correct, yours is the same as mine.

Actually, your solution seemed a little bit intricate to me. That’s why I tried to write the assertion with the techniques I have learned.

As you found out, there are many ways to approach an assertion. Your original question was that a certain event must occur within a range of cycles from n to m. if n and m were static, like 1 to 5, then you can use ##[1:5] var. However, SVA does not support dynamic ranges where n and m are defined in variables. This type of question came in very often. To solve this in a much easier way, I wrote a package, and YES, it is complex.
The count approach is definitely easier to understand and I too prefer it.

One more thing, the waveform you shared where your solution and my assumption can be observed clearly, over there I noticed one thing. In my case, ok2 is not exactly presented as ok signal. You also can notice that. Is that any kind of fault or something else?

It is something related to either the tools or the *$dumpfile(“dump.vcd”); $dumpvars;
*. I originally tested the code in eda and the OKs were delayed by one cycle; I could not explain it. Also, the displays of the count were odly duplicated. So I left my slick Pixelbook and tried my heavier laptop that has a full license of a simulator. The results there were as expected, and those are the ones I included in my last post.

11

In reply to Shubhabrata:

In reply to ben@SystemVerilog.us:
I have another question regarding my code which you corrected. Why did you use first_match ?
I don’t think it was necessary. I mean we are dealing with consecutive repetition and also only one repetition case. So I am not getting the importance of this construct over here?

You are correct for this case. In general, I worry about cases of the form
*a [ 1: ] ##1 b ##0 c** https://www.edaplayground.com/x/Vbud because as long as "a==1 and when b==0, the simulator checks for other threads. Here, you would need the first_match, like first_match(a [* 1: ] ##1 b) ##0 c

Your case is different because the “b” is “!a”, thus you no longer have more threads, and the first_match is not needed. I missed that point and I used the first_match, again because this structure generally needs it. Check the 2 models below.


// The general worrisome case that needs the first_match
module m;
    bit clk, a, b, c, p, e, pass, err;
    initial forever #10 clk = !clk;
    
    ap_1: assert property (@(posedge clk) $rose(a) |-> a [* 1: $] ##1 b ##0 c) pass=1; else err=1; 
  
    ap_2: assert property (@(posedge clk) $rose(a) |->
                           first_match(a [* 1: $] ##1 b) ##0 c) p=1; else e=1;
    initial begin
      $dumpfile("dump.vcd"); $dumpvars;
      repeat (2) begin
        @(posedge clk);
        a <= 1'b1; 
        repeat(2)  @(posedge clk);
        b<= 0; 
        repeat(2)  @(posedge clk);
        b<=1'b1; 
        repeat(2)  @(posedge clk);
        c<= 1'b1;
        repeat(2)  @(posedge clk);
      end
      $finish;
    end
  endmodule

// (1) - EDA Playground


// Your model, no need for the first_case, though it does not hurt. 
  module m;
    bit clk, a, b, c, p, e, pass, err;
    initial forever #10 clk = !clk;
    
    ap_1: assert property (@(posedge clk) $rose(a) |-> a [* 1: $] ##1 !a ##0 c) pass=1; else err=1; 
  
    ap_2: assert property (@(posedge clk) $rose(a) |->
                           first_match(a [* 1: $] ##1 b) ##0 c) p=1; else e=1;
    initial begin
      $dumpfile("dump.vcd"); $dumpvars;
      repeat (2) begin
        @(posedge clk);
        a <= 1'b1; 
        repeat(2)  @(posedge clk);
        a<= 0; 
        repeat(2)  @(posedge clk);
        a<=1'b1; 
        repeat(2)  @(posedge clk);
        c<= 1'b1;
        repeat(2)  @(posedge clk);
      end
      $finish;
    end
  endmodule