Difficulty: Hard · Puzzle 6 of 6 · Topic: Temporal Corner Puzzles
Property intent: on $rose(state[3:0]), enter must assert. Timeline (all other samples are 0): state is 4'b0010 at C100 and 4'b0100 at C101, enter=0 at C101. Determine the verdict.
property p_vector_rose;
@(posedge clk) $rose(state[3:0]) |-> enter;
endpropertyIn SVA, $rose on a vector expression is based on the least significant bit transition.
1) LSB of state is 0 at C100 and 0 at C101.
2) $rose(state[3:0]) is therefore false at C101, despite upper-bit toggles.
3) Antecedent does not trigger; consequent is not checked.Answer: VACUOUS-PASS - no antecedent trigger occurs because the vector LSB did not rise, so implication passes vacuously.
Checked by running the code in Verilator 5; the printed output supports the answer above. state changes at C100 and C101, but only its LSB counts for $rose, so the antecedent never hits.
Interviewers use this to catch assumptions that $rose(vector) means any-bit rise. With state going 4'b0010 to 4'b0101 (LSB 0 to 1) the same property would fire and FAIL at C101.
How would you rewrite the trigger to detect a rise on any bit of state? Model answer: compare against the previous sample bit by bit, for example |(state & ~$past(state)) as the antecedent (true here at C101: 0100 & ~0010 = 0100), or OR together $rose(state[i]) for each bit. Note $past needs a valid history (see the reset-release puzzle).
I would look at the least significant bit, since rose on a vector looks only at bit zero. It is zero at C100 and zero at C101, so there is no rise and no attempt, and the property passes vacuously even though the upper bits toggled. The trap is assuming it means any bit rose. With state going from 0010 to 0101 the least significant bit would rise and the property would fail at C101 if enter is low. I would write per-bit or changed checks if the intent is any change.