Difficulty: Easy · Puzzle 3 of 6 · Topic: Temporal Corner Puzzles
Property intent: when valid falls, idle must be high in that same cycle. Timeline: the test starts at C60 with valid=1; valid=1 through C69, then valid=0 from C70 on. idle=1 at C70 only and idle=0 at every other sampled edge. Evaluate p_fell and p_level.
property p_fell;
@(posedge clk) $fell(valid) |-> idle;
endproperty
property p_level;
@(posedge clk) !valid |-> idle;
endpropertyCount how many sampled edges make each antecedent true.
1) $fell(valid) compares valid at this edge with valid at the previous edge. It is true only at C70 (1 at C69, 0 at C70). At C71 and later both samples are 0, so it is false.
2) p_fell therefore starts exactly one attempt, at C70, where idle is 1. It PASSES.
3) !valid is a level: it is true at C70, C71, C72 and every later edge. p_level starts an attempt each cycle.
4) idle is 0 at C71, so p_level FAILS at C71 (and at every later edge).
5) Same waveform, opposite verdicts: $fell is a one-cycle event, !valid is a state.Answer: p_fell PASSES (one attempt at C70, idle=1); p_level FAILS from C71 (valid stays low, idle drops).
Checked by running the code in Verilator 5; the printed output supports the answer above. $fell is a one-cycle event that passes at C70; !valid is a level and fails as soon as idle drops at C71.
Candidates read $fell(valid) as 'valid is low' and expect checks in every idle cycle. It fires once, on the edge where the sampled value changes from 1 to 0, so a single idle pulse satisfies it. Use the level form when the requirement is a state, and $fell when it is a transition.
If valid went 1,0,1,0 at C69, C70, C71, C72, how many attempts would p_fell start and where? Model answer: two, at C70 and C72 (each 1 to 0 transition is a fall; the rise at C71 is not). idle must be high at both C70 and C72 or the property fails at the one where it is low.
I would separate event from level. The fell of valid is true only at C70, where idle is high, so that property passes with one attempt. The not valid form is a level, true at C70 and at every later edge, and idle is low at C71, so it fails at C71 and onward. The trap is reading fell as valid is low. I would use fell for a transition requirement and the level form for a state requirement.