Proving a debug path in a RISC-V core can never run

1The issue

Line 850 of the core's controller, and the 36 lines after it, never ran in any of the maintainers' simulations. The code handles debug single stepping while the core runs a hardware loop. The same code in another controller state is fully covered. The core's maintainers suspected it could never run, but could not set up a formal proof, so the hole stayed open.

The points on the issue

2What we did

1. 1Found why rows 2 and 3 can never happen. Single step can only be turned on by a debug return or a register write, and both send the controller back to its normal state. There it stops for the single step before it can enter the hardware loop state.
2. 2Proved this with formal verification, which checks every reachable state, not only the ones a test happens to try.
3. 3Checked the proof is meaningful. When we broke the design on purpose, the check failed, so it can catch a real bug.
4. 4Wrote a test for row 4: in debug mode, turn on single step and run a hardware loop. It reaches the row on 28 clock cycles, and on none when single step is left off.