Proving the fix for an instruction count bug in debug mode

1The issue

The minstret register counts the instructions a RISC-V core retires, meaning finishes. Issue 558 reported that an mret run in debug mode raised that count. An mret is the instruction that returns from a trap. The issue author also suggested where to fix it, in the decoder. The maintainers later changed the decoder to treat mret in debug mode as illegal, and the issue was closed.

The points on the issue

2What we did

1. 1Wrote a rule: while the core is in debug mode, a retiring mret must not raise the instruction count.
2. 2Ran it on the design from 27 May 2022, before the issue was filed. Formal checking found a 10 cycle trace: a debug request, then an mret fetched from the debug halt address that retires with the count raised.
3. 3Proved the same rule on the current design for all time, and checked that an mret can no longer retire in debug mode at all.
4. 4Only then read the maintainers' fix. It blocks the exact path the trace isolates, at the place the issue author proposed.