Assert a_nmi_handler_max_retire fails in formal with PMA config

Created by: silabs-mateilga

Component:RTL git hash: 9c1d3db4

Controller retires two instructions (1 is max) before taking the bus error NMI, when an ST instruction is retired to the write buffer. See waveform0. for details.

Early debugging with @silabs-oysteink indicates id stage should be halted in the case where nmi_allowed is high but the fsm decides not to take it anyway. A quick modification where nmi_allowed is made to depend on nmi_pending_q ( assign nmi_allowed = interrupt_allowed && nmi_pending_q; ) solved the immediate CEX, but formal found another CEX seen in waveform1.

reproduce: Run formal verification with PMA enabled, any of the PMA configurations found in core-v-verif/cv32e40x/tb/uvmt/uvmt_cv32e40x_constants.sv should show the problem, example waveform from pma_test_cfg_4.

waveform0

waveform1