Difficulty: Medium · Puzzle 1 of 6 · Topic: Temporal Corner Puzzles
Property intent: when valid is high, data from 2 cycles ago must be 8'hA5. Timeline: reset deasserts at C0, first active check with valid=1 occurs at C1. Determine the verdict.
property p_past_2;
@(posedge clk) valid |-> ($past(data, 2) == 8'hA5);
endpropertyAsk whether two prior sampled cycles exist yet.
1) valid at C1 triggers the check immediately.
2) $past(data,2) requires sampled history reaching back to C-1 relative to C1, which is unavailable in startup.
3) Tools typically evaluate this as unknown/invalid history and the comparison does not prove true.Answer: FAIL - the first trigger occurs before a 2-cycle sampled history exists, so the $past comparison is not satisfied.
Candidates assume $past auto-fills with reset values unless explicitly guarded.
How would you gate this property so it only starts after two valid sample edges?