Proving three debug cause cases in a RISC-V core never occur

1The issue

Line 1241 of the core's controller is a condition checked in the debug flush state, on the way into debug mode. It works out which cause sent the core there. Three rows of that condition were never covered by the maintainers' tests: a hardware trigger as the only cause, an ebreak instruction that is not set to enter debug as the only cause, and a data load event as the only cause. The core's maintainers had waived all three using their own formal checks.

The points on the issue

2What we did

1. 1Found why. Every trigger or debug request that sends the core into this state also sets a debug request flag in the same cycle, so a trigger is never the only cause.
2. 2Proved rows 5 and 10 with formal verification, which checks every reachable state, not only the ones a test happens to try.
3. 3Row 4 depends on a 32 bit trigger comparator, and the first proof method could not finish it. We proved it with a second method that is also a full unbounded proof.
4. 4Checked the proofs are meaningful. A separate run reached the debug flush branch and the taken branch at step 7.