In reply to a72:
Probably, you expect the assertion fails because ack keeps 1 for 2 or more cycles.
But the property sees only negedge of ack, not how long ack keeps 1 or 0.
In short, B of “A until B” is like a event of end of A.
In reply to a72:
Probably, you expect the assertion fails because ack keeps 1 for 2 or more cycles.
But the property sees only negedge of ack, not how long ack keeps 1 or 0.
In short, B of “A until B” is like a event of end of A.