// 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
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.
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?
“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
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?
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?
[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
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
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!
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:
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
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.
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 :)
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.
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