Showing a RISC-V core ran before halting for debug at reset

1The issue

When a debugger asks a core to halt from the moment reset ends, the core should stop before it runs any code. Issue 410 reported that the core's controller could not go straight from its reset debug state to the halted state. Instead it passed through a boot step and started running first. The maintainers later changed the controller so it checks the debug request during reset, and the issue was closed.

The points on the issue

2What we did

1. 1Wrote a rule for the debug state machine: with a debug request held from reset, the core must halt before it runs. It may run only after a debug return.
2. 2Ran the rule on the design from January 2022, before the fix. Formal checking, which tries every input sequence, found a 4 cycle trace where the core runs before it halts.
3. 3Ran the same rule on the current design. It is proven for all time, and also passes a bounded check to 25 cycles.
4. 4Only after proving, read the maintainers' fix and compared it with the trace.