Reaching an interrupt and debug clash as a core wakes up

1The issue

Line 399 of the core's controller decides what to do when an interrupt arrives in the first instruction fetch after the core starts or wakes from sleep. Two conditions on that line were never covered: an interrupt while the core is in debug mode, and an interrupt while a debug request is waiting. Both had been waived in earlier versions, with no proof or test behind the waiver.

The points on the issue

2What we did

1. 1Found why the debug mode case is impossible. The core only enters this fetch state after reset or after sleep, and it never sleeps while in debug mode.
2. 2Proved this with an unbounded formal proof, which checks every reachable state, not only the ones a test happens to try.
3. 3Used a formal search to find a path to the other condition: the core sleeps, an interrupt wakes it, and a debug request arrives in that first fetch cycle.
4. 4Wrote a test that wakes the core with a timer interrupt and sends a debug request at a different delay each time, over 32 iterations. It hits the condition once, at cycle 13562, and never hits the debug mode case.