Proving an execute stage condition row can never happen
A coverage hole in a RISC-V core's execute stage, in the FPU build. We proved the one uncovered row of the condition can never happen.
1The issue
Line 396 of the core's execute stage is the clear condition of a register that remembers an APU result. One row of that condition was never exercised by the maintainers' regression: mulh_active set while the operation is not MUL_H, with every other term false. The core's maintainers reported it as unreachable using a commercial formal tool and waived it. We checked the same property with a different, open source tool chain.
The points on the issue
2What we did
- 1Found why the row can never happen. The multiplier only raises mulh_active for a MUL_H operation, so it cannot be set while the operation is something else.
- 2Proved this with an unbounded formal proof on the FPU build of the core. Unbounded means it holds for every reachable state, not only a fixed number of cycles.
- 3Checked the proof is meaningful. A cover run reaches the full condition at step 15, so the check does not pass only because the condition never comes up.
- 4Wrote waiver text that excludes that one row only, with its assumptions and evidence.
3Result
The uncovered row 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