Difficulty: Medium · Puzzle 3 of 6 · Topic: Implication Puzzles
Property intent: after req, ack must appear after 1 cycle, then done exactly 2 cycles after ack. Timeline: C10 req=1, C11 ack=1, C12 done=1, C13 done=0. Determine the verdict.
property p_chain;
@(posedge clk) req |-> ##1 ack ##2 done;
endpropertyCompute the done check cycle from the acknowledged point.
1) req at C10 triggers consequent.
2) ##1 ack requires ack at C11, which is satisfied.
3) ##2 done then requires done at C13.
4) done is high at C12 only, so the required C13 sample fails.Answer: FAIL - ack timing is correct, but done arrives one cycle too early relative to the chained ##2 requirement.
Candidates often compress chained delays mentally and accidentally check done at C12.
How would verdict change if done were high at both C12 and C13?