Showing debug registers could be accessed outside debug mode

1The issue

The core has four registers kept for the debugger, such as dcsr and dpc. Outside debug mode, an instruction that accesses them must be rejected as illegal, which causes a trap. The report said that in machine mode the access did not trap. The core flagged the instruction as illegal, but the flag never reached the end of the pipeline, so the instruction finished as if it were allowed.

The points on the issue

2What we did

1. 1Wrote a rule: outside debug mode, an instruction that accesses a debug register must raise an illegal instruction exception.
2. 2It took five versions of the rule. Each was corrected from a trace, for example to rule out bus errors and to allow a debug trigger on the same instruction.
3. 3Ran the final rule with formal verification, which checks every reachable state. It fails on the design before the fix and holds on the current design.
4. 4Read the fix by the core's maintainers only after the proof. A condition that is always false when the extension interface is off had blocked the illegal flag; the fix inverts it.