Proving a divide unit branch in a RISC-V FPU can never run
A coverage hole in the divide and square root unit of a RISC-V core's FPU. We proved the uncovered branch can never run inside the real core.
1The issue
Lines 287 and 288 of the divide and square root unit in the core's FPU build were never covered by the maintainers' tests. Line 286 handles a new operation starting while the unit is ready. Line 287 asks whether a write back finishes in the same cycle, and line 288 keeps the unit ready if so. The core's maintainers reported the branch as unreachable using a commercial formal tool and waived it.
The points on the issue
2What we did
- 1Found why line 288 can never run. Starting a new operation and completing a write back are mutually exclusive in this unit.
- 2Proved this with an unbounded formal proof, with the check attached to the unit inside the core's FPU wrapper, not to the unit on its own.
- 3Checked the proof is meaningful. A cover run reaches the line 286 case at step 12, so the check does not pass only because that case never comes up.
- 4Wrote waiver text for lines 287 and 288 with the assumptions and evidence.
3Result
The branch is proven dead code in the FPU build and can be waived. This matches the maintainers' record, reached with a different tool chain.
The proof holds for one configuration and RTL revision, under stated assumptions such as legal OBI handshakes and no CSR writes to the hardware loop registers.
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