Concurrent assertions sample on a clock. |-> is overlapping implication; |=> is next-cycle. Immediate assert fires when the statement runs — see Assertions.
sequenceDiagram participant REQ participant ACK REQ->>ACK: valid Note over ACK: |=> next cycle ACK-->>REQ: ack
property p_req_ack;
@(posedge clk) disable iff (!rst_n)
req |=> ack;
endproperty
assert property (p_req_ack);
Keep properties in a checker or bind file if synthesis does not want them in the DUT.
Wrong vs right
Wrong — req |-> ack when ack is specified one cycle later.
Right — match the protocol: same-cycle |->, next-cycle |=>, and disable iff on reset.