Proving a multiply flag case in a RISC-V core never occurs
An open coverage hole in a RISC-V core's execute stage. We proved that the high multiply flag can never be set without a high multiply operation.
1The issue
Line 387 of the core's execute stage decides when to hold on to an APU (auxiliary processing unit) result that arrives while the register write port is busy. One case was never reached by the maintainers' regression: the multiplier's high multiply flag set while the current operation is not a high multiply, with every other part of the condition false. The core's maintainers had already reported it unreachable with their own formal tool.
The points on the issue
2What we did
- 1Found why. The multiplier raises the high multiply flag only for a high multiply operation.
- 2Proved the case can never happen with formal verification, which checks every reachable state, not only the ones a test happens to try. We used the maintainers' configuration with the floating point unit built in.
- 3Used the assumptions enabled in the maintainers' formal setup, such as legal bus handshakes and no writes to the hardware loop control registers.
- 4Checked the proof is meaningful. A separate run reached the full condition at step 14.
3Result
The case can be excluded from coverage. This matches the maintainers' result, now checked with a different, open source tool chain.
The proof assumes software never writes the hardware loop control registers directly, as the maintainers' formal setup does, and holds only for this configuration and core revision.
Have a coverage hole like this one?
Describe the problem in a few lines. An engineer replies, and we agree the scope together.
Discuss a verification problem