Why the FPU arbiter in a RISC-V core never arbitrates
A coverage hole in a RISC-V core's FPU arbiter. We proved two FPU operation groups never present a result in the same cycle, so its selection logic never runs.
1The issue
The issue reports unreachable code in the lzc blocks of the core's FPU build. These blocks sit in a round robin arbiter whose job is to choose between several requests that arrive at once. The maintainers' record waived the holes and explained them as a one core setup that under uses the arbitration. It gave no proof, no test, and no module instance or line number.
The points on the issue
2What we did
- 1Traced the lzc blocks to the round robin arbiter in rr_arb_tree. In this build the only instance with more than one input is the operation group arbiter at the top of the FPU.
- 2Proved with an unbounded formal proof that no more than one operation group ever requests that arbiter at once. The core issues one APU operation at a time and waits for it.
- 3Checked the proof is meaningful. A cover run reaches each of the four operation groups, so every arbiter input can be active.
- 4Wrote waiver text that states the cause and says which part is still open.
3Result
The arbiter never has to choose in this build, so its round robin selection logic, including the lzc, never runs. This adds a proof to the maintainers' explanation.
This identifies the cause, but mapping it onto the specific uncovered lines inside lzc.sv still needs the original coverage database.
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