Proving a write back clash in a RISC-V core can never occur
An open coverage hole in a RISC-V core's execute stage, with the floating point unit built in. We proved the uncovered case can never happen.
1The issue
Line 211 of the core's execute stage sits inside the branch that handles a result from the APU (auxiliary processing unit). It raises a contention flag when the ALU wants to write a register and the APU is not enabled. One case was never reached by the maintainers' regression: the APU and an ALU register write both enabled at once inside that branch. 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 decoder never enables the APU and an ALU register write for the same instruction in the same cycle.
- 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 enclosing branch at step 12.
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