Difficulty: Medium · Puzzle 1 of 6 · Topic: Temporal Corner Puzzles
Property intent: when valid is high, the data from 2 cycles ago must have been 8'hA5. Setup: simulation starts at C0, the first clock edge; reset is already released at C0; data is a logic [7:0] with no initial value and is 8'hA5 at every edge from C0 on; valid is 0 until it goes high for the first time at C1. Determine the verdict at C1.
property p_past_2;
@(posedge clk) valid |-> ($past(data, 2) == 8'hA5);
endpropertyAsk whether two prior sampled cycles exist yet, and what $past returns when they do not.
1) valid at C1 triggers the check immediately.
2) $past(data,2) at C1 needs the sample at C-1, which does not exist. There is no 'unavailable' result: the LRM returns the default value of the expression type, X for a 4-state logic, 0 for a 2-state type.
3) X == 8'hA5 is X, which is not true, so the consequent is not satisfied and the property FAILS at C1 even though data was A5 all along.
4) If valid first rose at C2, $past(data,2) would read C0 (8'hA5) and the property would pass.Answer: FAIL - the first trigger at C1 reads a $past sample from before simulation start, which returns the type default (X here, 0 for a 2-state type), not A5.
Checked by running the code in Verilator 5; the printed output supports the answer above. At C1 the $past(data,2) sample predates the simulation; Verilator's 2-state default of 0 (X in a 4-state simulator) is not A5, so it fails.
Candidates either think $past is skipped or invalid at startup, or assume it auto-fills with the current or reset value. Neither: it returns X or 0, so the comparison fails and the failure is a false alarm caused by missing history (Verilator reports FAIL at C1 for this setup).
How would you gate this property so it only starts after two real sample edges? Model answer: add a warm-up flag, for example a 2-bit counter that resets to 0 and saturates at 2 after two clocks, and write (valid && warm_ok) |-> ... or put !warm_ok in the disable iff. Holding reset for at least two clock edges with a defined data value also gives $past real history, but the explicit flag does not depend on that.
I would look at what the past function returns at C1: it needs the sample from two cycles back, which is before simulation start. There is no skip; it returns the default of the type, X for four state data, so the comparison with A5 is not true and the property fails at C1, even though the data was A5 all along. The trap is assuming it is skipped or filled with the current value. I would fix it by gating the check on enough history having passed.