In reply to foxtrot:
Quote:
..but it's a vacuous pass even when ack rises after say 4 or 6 clk2 cycles.
Vacuity occurs only if the antecedent
$rose(req)==0.
Keep in mind that at every clocking event (i.e., the
@(negedge clk1)) you have an attempt at the property, and if in the cycles af$ter the successful
$rose(req) you have no more rose, then those attempts are vacuous. Maybe what you see are those vacuous threads.
However, the attempt with a successful
$rose(req) can finish in one of the possible ways:
PASS, FAIL, INCOMPLETE (if at end of simulation
ack never occurred).
Try the following
ap_reqack: assert property(@(negedge clk1) $rose(req) |->
@(posedge clk2) !ack[*4:$] ##1 ack) $display("%t PASS", $realtime);
else $display("%t FAIL", $realtime);
Ben Cohen
http://www.systemverilog.us/
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
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- 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