Difficulty: Medium · Puzzle 4 of 6 · Topic: Temporal Corner Puzzles
Property intent: after cfg_update, cfg_bus must not change for the next two cycles. Timeline (cfg_update is 0 elsewhere): C80 cfg_update=1 and cfg_bus=16'h1234 (the new value is already on the bus), C81 cfg_bus=16'h1234, C82 cfg_bus=16'h1234. Determine the verdict, then say what changes if cfg_bus was 16'h0000 at C80 instead (so the bus changes at C81).
property p_cfg_stable;
@(posedge clk) cfg_update |=> $stable(cfg_bus)[*2];
endproperty$stable at a cycle compares that cycle with the one before it. Which samples does each of the two repetitions compare?
1) cfg_update at C80 triggers a non-overlapped check starting at C81.
2) $stable(cfg_bus) at C81 compares C81 with C80, and at C82 compares C82 with C81. So three equal samples (C80, C81, C82) are needed for the two repetitions.
3) With C80, C81, C82 all 16'h1234 both repetitions hold and the property passes.
4) With C80 = 16'h0000, $stable at C81 is false (0000 vs 1234), so the first repetition fails and the property FAILS at C81.Answer: PASS for C80 = 16'h1234 (three equal samples C80..C82); FAIL at C81 if cfg_bus was different at C80, because $stable at C81 compares against C80.
Checked by running the code in Verilator 5; the printed output supports the answer above. With 1234 on the bus at C80, C81 and C82 both $stable checks hold and the property passes. If the bus was 0000 at C80, $stable at C81 compares against C80 and the check fails at C81.
The two [*2] repetitions are $stable at C81 and C82, and each looks one sample back, so the bus must already hold the value at C80. Both of the usual slips are wrong: counting only C81 and C82 as 'two samples', or evaluating $stable at C80 (that would compare C80 with C79).
If cfg_bus changed to 16'h4321 at C82 (C80 and C81 still 16'h1234), which repetition fails? Model answer: the second one. $stable at C81 is true, $stable at C82 is false (4321 vs 1234), so the property FAILS at C82.
I would count samples: the non-overlapped arrow starts at C81, and each stable check compares a cycle with the one before it. So the two repetitions compare C81 with C80 and C82 with C81, which means three equal samples, C80 to C82. With 1234 on all three the property passes. If the bus was 0000 at C80, the first check fails at C81. The trap is counting only C81 and C82 as the two samples, so I would check the value one cycle earlier.