You are writing a property to verify bus protocol
property p_handshake;
@(posedge clk) req |=> ##2 ack;
endpropertyDuring simulation, the req signal transitions to high at clock cycle 10. For the assertion to successfully pass, at exactly which clock cycle MUST the ack signal be high?
The |=> operator is the non-overlapping implication operator. It means that if the antecedent (req) is true at cycle T, the evaluation of the consequent begins at cycle T+1 (cycle 11). The consequent is ##2 ack. This specifies a delay of 2 clock cycles from the start of the consequent evaluation. Therefore, 11 + 2 = 13. ack must be high at cycle 13.