Difficulty: Hard · Puzzle 5 of 6 · Topic: Temporal Corner Puzzles
Property intent: when done is high, req must have been high 2 cycles earlier and ack 1 cycle earlier. Timeline: C90 req=1, C91 ack=1, C92 done=1. Determine the verdict.
property p_history_pair;
@(posedge clk) done |-> ($past(req, 2) && $past(ack, 1));
endpropertyEvaluate both $past expressions at the done sample edge.
1) done at C92 triggers check.
2) $past(req,2) reads C90 and is 1.
3) $past(ack,1) reads C91 and is 1.
4) Conjunction is true.Answer: PASS - both history requirements line up exactly with req at C90 and ack at C91 before done at C92.
Candidates sometimes off-by-one the depth argument and read C91 for both terms.
Would this become VACUOUS-PASS or FAIL if done never asserted?