Difficulty: Medium · Puzzle 5 of 6 · Topic: Temporal Corner Puzzles
Property intent: when valid is high, data must equal the data sampled in the previous cycle (a held bus). The clock runs during reset. Timeline (all other samples are 0): rst_n=0 at C0..C3 and 1 from C4; data=8'h00 during reset (C0..C3) and 8'h5A from C4 on; valid=1 at C4 and C5. Evaluate p_hold and p_hold_gated.
property p_hold;
@(posedge clk) valid |-> (data == $past(data));
endproperty
property p_hold_gated;
@(posedge clk) (valid && $past(rst_n)) |-> (data == $past(data));
endpropertyBecause the clock ran during reset, $past has real history. Compare what it returns at C4 with what the first beat legitimately carries.
1) At C4 valid is high, data is 8'h5A and $past(data) is the C3 sample, the reset value 8'h00. The history is real here (the clock ran), not a startup default.
2) p_hold compares 5A with 00 and FAILS at C4. This is a false alarm: the first beat after reset is allowed to differ from the reset-time bus.
3) p_hold_gated: $past(rst_n) at C4 is the C3 sample, 0, so the antecedent is false and nothing is checked at C4. At C5 $past(rst_n) is 1 and 5A equals 5A, so it passes.
4) Putting disable iff (!rst_n) on p_hold would not help: rst_n is already 1 at C4, so the attempt is not disabled.Answer: p_hold FAILS at C4 (false alarm on the first beat after reset); p_hold_gated passes because $past(rst_n) in the antecedent skips the first post-reset cycle.
Checked by running the code in Verilator 5; the printed output supports the answer above. The first beat after reset differs from the reset-time bus: p_hold raises a false alarm at C4, the $past(rst_n) gate does not.
The history exists but belongs to reset, so the compare is meaningless on the first cycle after release. disable iff only masks cycles where reset is currently active, so it cannot fix a check that straddles reset release; guard the antecedent on the previous reset value or a history-valid flag.
Would $past(data, 1, rst_n), the gating argument of $past, be the same fix? Model answer: No. The gating argument gates the clocking event that $past samples on; it changes which earlier sample is returned, not whether the check runs, so the comparison still happens at C4. It is not a window or a history-valid test, and some tools reject the 3-argument form (Verilator 5.048 reports it unsupported). Guard the antecedent with $past(rst_n) or a flag instead.
I would note that the clock ran during reset, so the past data at C4 is the real reset value, zero. The first beat after release has data 5A, so the plain property fails at C4, which is a false alarm. The gated version looks at the previous reset value, which is low at C4, so nothing is checked then and at C5 the data matches and it passes. The trap is thinking disable iff fixes it; it only masks while reset is active, so I would gate the antecedent on the past reset.