A simple assertion; req implies ack; does not fail

In reply to a72:
I never liked to use the until construct when the left hand side is is not a simple expression. I find it confusing to use the until when property_expr1 is a sequence rather than a simple expression.
property_expr1 until property_expr2
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.

Try this for your assertion.


// $rose(req) |=> !req[*1:10] until ack ##1 !ack;
$rose(req) |=> !req[*1:10] intersect 
                 ack[->1] ##1 !ack;

More discussion on this coming soon.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. 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
  1. Papers:

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/