Proving a debug entry in a RISC-V core always has a cause

1The issue

Lines 1187 and 1210 of the core's controller were never covered by the maintainers' tests. Each is the last fallback branch of a chain of checks that runs as the core enters debug mode. The chain looks for the cause of the debug entry, so the fallback would mean the core entered debug with no cause at all. The core's maintainers had waived both as unreachable using their own formal checks. We set out to confirm that independently.

The points on the issue

2What we did

1. 1Found why line 1187 can never run. The controller enters that state only when a debug cause is present, and the ID stage is halted, so the cause is still there one cycle later.
2. 2Found why line 1210 can never run. That state is entered only on a forced wake up (boot, sleep or a wait for interrupt) or during single step, and nothing in between turns single step off.
3. 3Proved both with formal verification, which checks every reachable state, not only the ones a test happens to try. Both proofs are unbounded and use open source tools.
4. 4Checked the proofs are meaningful. A separate run reached both debug states, so the proofs do not pass just because the states are never entered.