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 (all other samples are 0): 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 (two cycles after ack, not after req).
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 (reported at C13).
Checked by running the code in Verilator 5; the printed output supports the answer above. ack is on time but done is needed at C13 (two cycles after ack), so the check fails at C13.
Candidates often compress chained delays mentally and accidentally check done at C12. Each ## is relative to the previous term, so the done check is req + 1 + 2 = C13.
How would the verdict change if done were high at both C12 and C13? Model answer: it would PASS. Only the C13 sample is checked; done at C12 is simply ignored by this property.
I would chain the delays from the previous term: req at C10, ack one cycle later at C11, then done two cycles after the ack, so at C13. Ack is correct at C11, but done is high at C12 and low at C13, so the property fails at C13. The trap is measuring the done delay from req instead of from ack. I would next check whether the spec meant two cycles after ack or after req.