Difficulty: Medium · Puzzle 2 of 6 · Topic: Temporal Corner Puzzles
Property intent: after start rises, done must be high one cycle later. Timeline: start is 0 at every clock edge except C60, where it is sampled 1 and then 0 again at C61. Between the C40 and C41 edges start also glitches high for about 2 ns and is back to 0 before C41. done is low at every edge except C61. Evaluate the glitch near C40 and the rise at C60.
property p_rose_delay;
@(posedge clk) $rose(start) |-> ##1 done;
endproperty$rose compares the sampled value at this edge with the sampled value at the previous edge. What did each edge actually see?
1) The glitch between C40 and C41 is not present at any sampled edge: start is 0 at C40 and 0 at C41, so $rose is false at both and no attempt is started.
2) At C60 start is sampled 1 and was sampled 0 at C59, so $rose is true and an attempt starts.
3) ##1 done requires done at C61, and done is high at C61.
4) So there is exactly one attempt and it passes; the glitch is invisible to the assertion.Answer: PASS - the C40-C41 glitch is never sampled, so it starts no attempt (a waveform viewer would show a rise that the assertion does not see); the real rise at C60 is followed by done at C61.
Checked by running the code in Verilator 5; the printed output supports the answer above. A 2 ns glitch between edges is never sampled, so the only attempt is the real rise at C60.
Reading the waveform viewer, the glitch looks like a rise at about C40.5 and you would expect done at C41 and report a failure. Assertions only see values sampled at the clock edge; the glitch is a real design hazard, but this assertion cannot catch it.
If done never went high at C61 (stayed low), would this still pass? Model answer: No, the C60 attempt FAILS at C61 because done is low; the glitch near C40 still creates no attempt, so it is neither the cause nor flagged.
I would only look at values sampled at the clock edge. The glitch between C40 and C41 is gone at both edges, so there is no rise and no attempt. The real rise at C60 starts one attempt, and done is high at C61, so the property passes. The trap is trusting the waveform viewer, which shows a rise that the assertion never sees. I would note the glitch is a real hazard that needs a different check.