There are 2 signals ‘a’ and ‘b’. I have to write an assertion to check if ‘b’ does not toggle for 50 cycles when the toggle of ‘a’ is encountered.
In reply to taestytart:
ap_b_Stable: assert property(@ (posedge clk) $rose(a) |->
$stable{b) [*50] );
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- 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 - Papers:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - 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
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/
In reply to ben@SystemVerilog.us:
Hi, thank you for the answer. From what I understand, when a goes from 0 to 1, b stays stable for 50 cycles. Is it possible to use rose and fell for ‘a’ in the condition?
($rose(a) || $fell(a) |->$stable(b) [*50]);
In reply to taestytart:
Yes because ($rose(a) || $fell(a) is and expression, and that expression is a sequence of 1 cycle.
The use of the sequential or would be inappropriate here because
($rose(a) or $fell(a) |->$stable(b) [*50]); // DO NOT USE
// Because all terms of the OR in the antecedent need to be verified with its consequent
// Esentially, the following
($rose(a) or $fell(a) |->$stable(b) [*50]); // is equivalent to
( ($rose(a) |->$stable(b) [*50]) and ($fell(a) |->$stable(b) [*50]);
// If you insist on using the "or", then use the first_match() with it.
ap_ab: assert property(@ (posedge clk) first_match($rose(a) or $fell(a))
|-> $stable(b)[*50]);
There is a general recommendation by people on the 1800’2017 committee on assertions that one should avoid using the first_match()
In reply to taestytart:
One more note on *($rose(a) or $fell(a) |->stable(b) [*50])*;
One can correctly argue that in this case the **first_match()** is not needed because
one of the 2 threads is false. These threads are the rose(a) |-> consequent and the othher $fell(a) |-> consequent.
However, that would not be the case if one of the or elements were a sequence. Also, the or slows down the simulator because it has to process the other thread.
I still recommend the use of the boolean || or operator.