Difficulty: Hard · Puzzle 6 of 6 · Topic: Temporal Corner Puzzles
Property intent: on $rose(state[3:0]), enter must assert. Timeline: state changes from 4'b0010 at C100 to 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.
Interviewers use this to catch assumptions that $rose(vector) means any-bit rise.
How would you rewrite the trigger to detect a rise on any bit of state?