Instruction for next program counter after mret executed first before instruction at mret target

Nobody has claimed this yet.

Hello,

we are making formal verification experiments with IBEX and we for example have also found the problem from bug #1462 two days ago, with overwriting the branch mispredict address by a second predicted branch and also sending the second predicted branch as valid instruction to ID-stage even that the preceeding branch is mispredicted. Please let me know, when you also need more details for this behavior.

In a second formal verification run we see a mret instruction going into ID-stage. In the following two cycles signal id_in_ready_i of ibex_if_stage is low. The reason is that the control-FSM of ibex_id_stage is in states DECODE and FLUSH and sets the signals retain_id and halt_if, this happens due to the mret instruction in the ID-stage. Nevertheless, the immediately succeeding instruction after the mret (PC+4) moves into the skid-buffer of ibex_if_stage, because it is a predicted branch and id_in_ready_i is low. In the third cycle after mret went into ID-stage the instruction immediately after the mret (PC+4) is sent as valid instruction to the ID-stage, because it is in the skid-buffer and skid buffer has priority over the instruction at the mret target address.

I am no compiler expert and do not know which instructions can be at PC+4 after mret. But my question is, if it is correct and allowed to happen that the instruction at PC+4 after mret program counter is executed in this case first after an mret instruction and not immediately the instruction at the mret target?

Thank you for your help.

Best Regards,
Christian

## My Environment
IBEX parameters:
#(.PMPEnable(1'b1),
.PMPNumRegions(16),
.MHPMCounterNum(3),
.RV32B(RV32BFull),
.RegFile(RegFileFF), //default-value
.BranchTargetALU(1'b1),
.WritebackStage(1'b1),
.ICache(1'b1),
.ICacheECC(1'b1),
.BranchPredictor(1'b1),
.DbgTriggerEn(1'b1),
.SecureIbex(1'b1),
.RndCnstLfsrSeed(32'hac533bf4),
.RndCnstLfsrPerm(160'h1e35ecba467fd1b12e958152c04fa43878a8daed)
)

**EDA tool and version:**
JasperGold v2021.06

**Operating system:**
CentOS 7.9.2009

**Version of the Ibex source code:**
31c5b5eefdf5607ce67427b3316f9111f801c465

Start by tracing the mret path through ibex_id_stage and ibex_if_stage, focusing on the DECODE and FLUSH states, id_in_ready_i, retain_id, halt_if, and the skid-buffer priority. Determine whether PC+4 may reach ID before the mret target, then document the expected ordering and verification evidence needed to establish whether this is a bug.

Written by the indexing model from the issue text.