IbexSetExceptionPCOnSpecialReqIfExpected firing when it shouldn't

[matteovit]

Observed Behavior

IbexSetExceptionPCOnSpecialReqIfExpected is fired when (I think) it shouldn't.

The firmware does a CSR write to mstatus to (re)enable the interrupts. This triggers a pipeline flush in the core.
An interrupt is asserted at exactly the same time and IbexSetExceptionPCOnSpecialReqIfExpected fails.

the firing assertion is:

`ASSERT(IbexSetExceptionPCOnSpecialReqIfExpected,
      exception_req_pending && expect_exception_pc_set && exception_req_done |->
      seen_exception_pc_set || exception_pc_set)

The antecedent sequence expression is exception_req_pending && expect_exception_pc_set && exception_req_done.

Looking one at a time:

exception_req_pending <= (exception_req_pending | exception_req) & ~exception_req_done;

where

assign exception_req = (special_req | enter_debug_mode | handle_irq);
assign handle_irq = ~debug_mode_q & ~debug_single_step_i & ~nmi_mode_q &
      (irq_nm | (irq_pending_i & irq_enabled));

So in this context, exception_req_pending is latching if there is an interrupt pending (and enabled) until exception_req_done is asserted.

// Set `expect_exception_pc_set` if exception req needs one and keep it asserted until
// exception req is done
expect_exception_pc_set <= (expect_exception_pc_set | exception_req_needs_pc_set) & ~exception_req_done;

Which is latching exception_req_needs_pc_set:

exception_req_needs_pc_set = enter_debug_mode | handle_irq | special_req_pc_change;

handle_irq is asserted.

The problem is with exception_req_done.

assign exception_req_done =
      exception_req_pending & (ctrl_fsm_cs != DECODE) & (ctrl_fsm_ns == DECODE);

This is asserted if exception_req has been latched and the control units move from a state different from DECODE to the DECODE state. This is true for both FLUSH and i.e. IRQ_TAKEN.

So the antecedent sequence expression is true if an interrupt exception was executed or if there is an interrupt pending (at the correct point in time) and the pipeline is flushed.

The consequent sequence expression is:

seen_exception_pc_set || exception_pc_set

where

assign exception_pc_set =
      exception_req_pending & (pc_set_o & (pc_mux_o inside {PC_EXC, PC_ERET, PC_DRET}));

but this is not true because the exception (interrupt) is not handled since the pipeline is currently being flushed.

Expected Behavior

I don't think IbexSetExceptionPCOnSpecialReqIfExpected should fire in this scenario.

My Environment

Version of the Ibex source code:

1313104

No changes to the code