I have a question regarding above:
if req, ack sequence is as below
clk 1 2 3 4 5 6
req 0 1 1 1 1 0
ack 0 0 0 0 1 0
in that case assertion will become true at clock cycle 5. I want to know whether the antecedent will get evaluated at clk cycle 3, 4, 5 as well causing the assertion to expect ack to be asserted for the req at clk 3, 4, 5? or the next evaluation for the assertion will happen from cycle 6 if req happens to be high then.
I could not figure this out from the material on until_with.
At every clocking event there is an attempt to evaluate the assertion, and every attempt is separate from previous attempts.
Read my paper on understanding of the SVA engine , link below.