NMI handler entry retires during single stepping
Created by: silabs-mateilga
Note: This issue is found during work with expanding the debug assertion set in the 40s/dev branch of core-v-verif, and is discovered on the cv32e40s rtl. The issue is still created here, as the debug features are developed on the 40X and merged to 40S.
Component:RTL: For issues in the RTL (e.g. for files in the rtl directory)
###Description Upon a dret from debug mode with dcsr.STEP and dcsr.STEPIE set, trap handler entry should not retire before reentering debug mode. Formal verification of assert a_step_no_trap gives a CEX that proves this is violated in the event of a Load Bus Fault NMI, other interrupt causes can probably give the same problem.
Steps to Reproduce
Formally verify the debug_assert/a_step_no_trap assertion found in this PR of core-v-verif: #1515