Until_with evaluation

I wrote below assertion for this question: “once req is high, req must stay high until ack is not asserted”.

property check_req_ack;
     @(posedge clk)
     req |=> req s_until_with ack;
endproperty

assert property (check_req_ack);

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.

In reply to kuki2002:

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.

Use $rose(req) |=> req s_until_with ack
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:

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks. Actually for this case, I cannot use $rose as req can be high at cycle 6th and I would want the assertion to check for ack from then on.

clk 1 2 3 4 5 6 7 8
req 0 1 1 1 1 1 1 1
ack 0 0 0 0 1 0 0 1

In reply to kuki2002:

See my reply on exclusivity at
https://verificationacademy.com/forums/systemverilog/assertion-req-and-gnt-signals

In reply to ben@SystemVerilog.us:

Hi Ben thanks.
I think below would also work right, changing |=> to |->. I tried and it seems ok.

property check_req_ack;
     @(posedge clk)
     req |-> req s_until_with ack;
endproperty
 
assert property (check_req_ack);

In reply to kuki2002:

Ir would work. It also address the condition when req and ack are both true in teh same cycle.

In reply to ben@SystemVerilog.us:

Thanks Ben.