In reply to Rahul Patel:
From my SVA Handbook
always [3:4] a ##[1:4] b |-> c
* For every attempt, property must be true at 3rd and 4th cycle of that attempt
* Must be nonvacuously true at either 3rd or 4th cycle of that attempt
Now, with your example:
module m;
... variable declarations..
initial forever #10 clk=!clk;
assert property ( always [4:5] a ##[1:4] b |=> c );
In your testbench the antecedent is a no-match in cycles 4 and 5, thus the assertion is vacuously true.
On a separate note, I believe that you are misusing the "always"
// You are stating that at every clocking event (i.e., every 20ns) you have an attempt, and for that attempt, you want that in the 4th and 5th cycle thereafter the property is true.
Thus, at every attempt (every cycle) you have a new thread that behaves separately from the other threads.
Attempt 1 ^ . . . . P
Attempt 2 ^ . . . . P
Attempt 2 ^ . . . . . P
....
Attempt n ^ . . . . P
You can see the confusion!!! Actually, after the 4th cycle, you are checking the property at every cycle. If this is what you want, then write
assert property ( ##4 a ##[1:4] b |=> c );
Personally, if you must or want to use the always in an assertion, use it in an initial statement. Thus,
initial assert property ( always [4:5] a ##[1:4] b |=> c );
Thus, you want the property "a ##[1:4] b |=> c " to be true only in cycles 4 and 5.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- 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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy