In reply to vshankr:
This is a very confusing assertion because
@(data or posedge clk) says that the clocking event that starts the asn is either a change in data or a posedge of clk. There are 2 problems with this:
- the sampling event for the rest of the assertion is either of 2 events.
I never used this because the property takes different meanings depending upon which initial clocking event starts the assertion.
- If data changes from 4'b1001 to 4'b1101 there is no event
I suggest that the assertion be rewritten based on the requirements.
Perhaps the author was trying to say something like
// Guessing here at to the meaning
// there should never be a clk within 3 cycles consisting of a change of data in cycle 2
not ($changed(clk) within (1'b1 ##1 $changed(data) ##1 1'b1));
// This is not the way to write it. Yes a ##1 is a 1 clocking event tick.
// Also, does ##1 does not always refer to clk(not data) in this case, it depends as to what
// the "initial clocking event ", the one that starts the assertion is.
// In this model, it could be the @(data)
// I never saw this type ( @(a) or (b)) of modeling for the clocking event
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
2) Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
- Understanding the SVA Engine,https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertionshttps://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environmenthttps://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment