Catching an interrupt that broke debug single stepping

1The issue

In debug single step mode, the core runs one instruction and then stops for the debugger. The report said that an interrupt during a step could make the core run the wrong number of instructions. The RISC-V debug spec says that once an interrupt is taken during a step, the core must stop for debug before any instruction of the interrupt handler finishes. The core let one handler instruction finish first.

The points on the issue

2What we did

1. 1Wrote a rule from the debug spec: once an interrupt is taken during a step, no handler instruction may finish until the core enters debug mode.
2. 2Ran it with formal verification, which checks every reachable state, on the design from before the fix. The tool found a case where a handler instruction finished one step before the core entered debug.
3. 3Ran the same rule on the current design. It holds for every reachable state, and a bounded check 30 steps deep also passes.
4. 4Read the fix by the core's maintainers only after the proof. It makes the core stop for debug on the interrupt itself, the same event our rule watches.