Proving a single step stall in a RISC-V core never happens

1The issue

Line 675 of the core's controller checks whether the decode stage is ready while the core runs one instruction in debug single step. The branch for a stalled decode stage was never covered. The core's maintainers waived it after an equivalence check showed that removing the lines leaves the outputs unchanged, but there was no direct proof that the stall cannot happen.

The points on the issue

2What we did

1. 1Found why. Single step can only be turned on in debug mode, and the core leaves debug mode by flushing its pipeline. The stepped instruction is the first one after the flush, so nothing older is left to stall it.
2. 2Proved this with an unbounded formal proof, which checks every reachable state, not only the ones a test happens to try.
3. 3Checked the proof is meaningful. The single step block is reached in 16 cycles, and a stalled decode stage is reached in 7 cycles outside single step, so the stall path exists, just not under single step.