[SVA] signal rises and stays stable check -> how to write an assertion?

SystemVerilog
1

Hi All,

How can I write an assertion for a signal, which should rise within between 10 to 20 cycles and stay stable (HIGH) until the assertion will be disabled?

Thank you!

2

In reply to dmitryl:

 
 // How can I write an assertion for signal "a", 
    // which should rise within between 10 to 20 cycles 
    // FROM 1) initialization,  
    // and stay stable (HIGH) until the assertion will be disabled?

    // FROM 1) initialization, 
    initial begin
        ap_a_init: assert property(##[10:20] $rose(a) |=> always(a));  
    end

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

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy

3

In reply to ben@SystemVerilog.us:

Thank you a lot, Ben!

But how could I disable this assertion?

Let’s consider some TestBench, which has two events - event1 and event2.
When event1 happens, I’d expect the signal “a” should rise and stay stable (high) until event2.
When event2 happens, I’d like to release (disable/disassert) the assertion (after event2, the signal “a”) can receive any value.
Number of cycles between event1 and event2 is unknown.

4

In reply to dmitryl:

I think you mean you want the assertion to pass, not disable, if the conditions are satisfied.

You asked a similar question on another forum. It is important to be very specific about your requirements and leave little room for assumptions when writing an assertion. Based on these two posts, here is what I think your requirements are

When (event1) rises, (a) needs to rise within 10 to 20 cycles and needs to stay high until after (event2) rises.

Before anyone spends more time on this, does this match your requirements?

5

“I think you mean you want the assertion to pass, not disable, if the conditions are satisfied” - no, after rising of (event2), I want to stop checking either the signal (a) is still stable or not (after (event2) rose, signal (a) may get any value)

“when (event1) rises, (a) needs to rise within 10 to 20 cycles and needs to stay high until (event2) rises” - that is exactly what I need

6

In reply to dmitryl:

 
  // FROM 1) initialization, 
    initial begin
        ap_a_init: assert property(##[10:20] $rose(a) |=> 
   a[*0:$] ##1 $rose(b) );  
    end

Ben Ben@systemverilog.us

7

Great! Thank you, Ben!

One more question… You wrote your assertion without referring to clock edge (neither posedge or nor negedge).

Let’s consider there are several clocks in the TestBench. How does the simulator know which of the clocks is the reference clock? I mean how does the simulator know which clock to refer for ##[10:20] and ##1?

8

In the Ben’s last example, what will happen if the signal b never rise? In this case the assertion will never be ended and never will issue error… Correct?

initial begin
ap_a_init: assert property(##[10:20] rose(a) |=> a[*0:] ##1 $rose(b) );
end

Actually I need the signal a be checked for the stability after its rise until the signal b rises. If the signal b doesn’t rise then the stability check should be performed till end of the simulation. So, how to change the assertion in order to meet this requirement?

9

In reply to dmitryl:

[quote] You wrote your assertion without referring to clock edge (neither posedge or nor negedge)./quote]
You need to better understand te syntax and the working of SVA.
I used the default clocking and default disable


default clocking cb_clk @ (posedge clk);
endclocking
default disable iff (rst);

Without the strong qualifier, if “a==1” at all cycles and the rose(b) never occurs, the tool not report it as a failure when the simulation ends ($finish). To get a failure, you need the strong qualifier, as shown below.



   initial begin
        ap_a_init: assert property(##[10:20] $rose(a) |=> 
                 strong(a[*0:$] ##1 $rose(b)) );  
    end

Study the syntax and how SVA works!
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy

10

Dear Ben, I just searched the LRM 3.1a and also your book (SVA Handbook), but have not found the strong qualifier description there…
Where can I learn about this qualifier (and others, which I probably missed)?
Thank you!

11

In reply to dmitryl:
The strong and weak is covered in 1800 and in my books.
1800: 16.12.1 Sequence property
Sequence properties have three forms: sequence_expr, weak(sequence_expr), and
strong(sequence_expr). The strong and weak operators are called sequence operators.
strong(sequence_expr) evaluates to true if, and only if, there is a nonempty match of the sequence_expr.
weak(sequence_expr) evaluates to true if, and only if, there is no finite prefix that witnesses inability to
match the sequence_expr. The sequence_expr of a sequential property shall not admit an empty match.
If the strong or weak operator is omitted, then the evaluation …

**In my book, 4th edition (*previous editions also cover this topic)
2.3.2.1.1 Strong / weak sequence in consequent
 Rule: The concept of strong/weak properties and sequence properties is addressed in Section 3.9. [1] If the strong or weak operator is omitted, then the evaluation of the sequence_expr (interpreted as a property) depends on the assertion statement in which it is used. If the assertion statement is assert property or assume property, then the sequence_expr is evaluated as weak(sequence_expr). Otherwise, the sequence_expr is evaluated as strong(sequence_expr).
 Guideline: Qualify as strong properties that are sequences and have range delays or consecutive repetition operators (e.g., [, [->, [= ) and are consequents in an assertion. This is important when it is necessary to qualify an assertion as a failure if the consequent never terminates at the end of simulation. Example:

ap_ab_recommend: assert property(@ (posedge clk) a |-> strong([1:] b)); //  ap_ab_weak: assert property(@ (posedge clk) a |-> ([1:] b)); // 
ap_abc_recommend: assert property(@ (posedge clk) a |-> strong(b[) ##1 c); // 
ap_abc_weak: assert property(@ (posedge clk) a |-> (b[) ##1 c); // 



Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
* [SVA Handbook 4th Edition, 2016 ISBN 978-1518681448](http://goo.gl/JOfuEB)  
* [Real Chip Design and Verification Using Verilog and VHDL, 2002  isbn 978-1539769712 ](https://goo.gl/d10QHh)
* 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:  https://verificationacademy.com/forums/systemverilog/vf-horizonspaper-sva-alternative-complex-assertions
12

In reply to dmitryl:

Dear Ben, I just searched the LRM 3.1a and also your book (SVA Handbook), but have not found the strong qualifier description there…
Where can I learn about this qualifier (and others, which I probably missed)?
Thank you!

Please delete the 3.1a LRM and get yourself the latest version.

13

In reply to ben@SystemVerilog.us:

Thank you for sharing the link!

BTW, what’s the difference between the ##[1:3]a and a[1:3] syntax?

14

In reply to dmitryl:

  • ##[1:3]a is same as 1’b1 ##[1:3]a, and tha is a clock delay of 1 to 3
  • a[1:3] is a vector bit 1 to 3. Thus, if

bit[0:15] a;
bit[0:2]  c;
c <=  a[1:3]; // "c" get vector slice of "a"

Again, sudy the SystemVerilog syntax!
Ben

15

In reply to ben@SystemVerilog.us:

It’s my mistake, I formulated my question badly… Actually I wanted to ask about the difference between the ##[1:3]a and *a[1:3] in assertions…

As for a[*1:3], does it means that statement ‘a’ should be repeated for 1, 2, or 3 cycles?
Will it the same as writing always(a)[*1:3]?

As for ##[1:3]a, does it mean that statement ‘a’ should be delayed for 1, 2 or 3 cycles?

16

In reply to dmitryl:
SV1800’2017 explains all of this;

 
a[*1:3] ##1 b // is same as 
(a[*1] ##1 b) or (a[*2] ##1 b) or (a[*3] ##1 b)

##[1:3]a ##1 b // is same as 
(##1 a ##1 b) or (##2 a ##1 b) or (##3 a ##1 b) 


Don't even think about always(a)[*1:3], you're not at that stage yet. 
(in case you're wondering what it means, you won't find it in the syntax :)

Ben

17

In reply to ben@SystemVerilog.us:

Hi Ben,

I have something similar requirement. I need to check whether “b” remains always high after 3 clock cycles of “a” going high. Below update doesn’t work.

ap_a_init: assert property(@(posedge clk) $rose(a) |-> ##3 always(b));

or
ap_a_init: assert property(@(posedge clk) rose(a) |-> strong (##3 (!(b)[*0:])) ;

Please suggest.

18

In reply to rohithgm:

update doesn’t work.

It should work; why do you say that it does not?
The only changes I would suggest are:


initial 
 ap_a_init: assert property(@(posedge clk) $rose(a)[->1] |-> ##3 always(b));

//or
initial 
  ap_a_init: assert property(@(posedge clk) $rose(a)[->1] |-> strong (##3 (!(b)[*0:$])) ;

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

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. 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
19

In reply to ben@SystemVerilog.us:

There is compilation errors for below assertion - illegal expression primary [4.2(IEEE)].

initial 
 ap_a_init: assert property(@(posedge clk) $rose(a)[->1] |-> ##3 always(b));

Error for below assertion: Unexpected identifier/operator specified in the “assert” property statement.

initial 
  ap_a_init: assert property(@(posedge clk) $rose(a)[->1] |-> strong (##3 (!(b)[*0:$])) ;
20

In reply to rohithgm:
Oops! My mistake in the use of the always with a sequence Per 1800


property_expr ::= 
  ...
    sequence_expr #-# property_expr   // followed-by operator 
  | sequence_expr #=# property_expr
  ...
  | always property_expr
  | always [ cycle_delay_const_range_expression ] property_expr
  | s_always [ constant_range] property_expr
// Thus, one cannot do the following 
$rose(a)[->1] |-> ##3 always(b)); // because
// "##3" is a sequence that is followed by the "always(b)" property 
// If you want a sequence followed by a property, then you have to the followed-by operator 
  sequence_expr #-# property_expr // concatenation with zero cycle delay
  sequence_expr #=# property_expr // concatenation with one cycle delay

below is code that compiles OK 
module m; 
    bit clk, a, b; 
    initial 
    ap_a_init: assert property(@(posedge clk) $rose(a)[->1] |->
    ##3 1'b1 #-# always(b));

    initial // with the cycle_delay_const_range_expression
    ap_a_init1: assert property(@(posedge clk) $rose(a)[->1] |->
      always[3:$] (b));
    
    initial 
    ap_a_init2: assert property(@(posedge clk) $rose(a)[->1] |-> 
    strong (##3 !(b)[*0:$])) ;
    // Had an opened "("
endmodule
// EDA Playground simulator
https://www.edaplayground.com/x/xij

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