Proving an operand select case in a RISC-V core never occurs

1The issue

Line 872 of the core's ID stage, where instructions are decoded, chooses a register to read for the APU (auxiliary processing unit) logic. That logic is only built in when the floating point unit is. The line checks five select signals. One combination was never covered by the maintainers' tests: a bit mask taken from a register while operand B is neither an immediate value nor a bit mask, and operand A is not register C. The core's maintainers had waived it.

The points on the issue

2What we did

1. 1Found why. The decoder takes the bit mask from a register in only four places (cv.insertr, cv.bclrr, cv.bsetr and the cv.addNr/subNr family), and each also sets one of the other signals, which rules this combination out.
2. 2Proved the combination can never occur with formal verification, which checks every reachable state, not only the ones a test happens to try.
3. 3Ran the proof twice: without the floating point unit, and with it, where line 872 is actually built into the core.
4. 4Checked the proof is meaningful. A separate run reached the enclosing branch at step 2 and four neighbouring legal combinations at step 6.