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

[cappold]

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

[GregAC]

Thanks for the report @cappold this does sound like a bug, the instruction after an mret shouldn't get executed. We should be flushing out the prefetch buffer following an mret and likely other things that set the PC (e.g. on exceptions).

I'll leave this open for now as I won't immediately create a fix. We'll wait to resolve #1462 first.

[cappold]

Hello,

Thank you for the answer. We have now found a similar behavior for the instruction sequence CSR-instruction->Store->Branch->JAL. The branch is predicted as not taken, but later it is computed that the branch should be taken. Nevertheless, the CPU executes the instruction at PC+2 after the branch first, before the instruction at the branch target. The reason is that the instruction at PC+2 moves into the skid-buffer, because stall_id_i is high for two cycles (reasons are outstanding store first cycle and stall_branch high due to branch target buffer and data independent timing for first two cycles). In formal verification runs with environments which allow situations where e.g. the debug_req_i signal can be high for only a few cycles (to few that debug mode is started), we found some other situations where the instruction from the skid-buffer is executed first, before the instruction which should be executed next. We just wanted to know you about these additional findings.

Thank you.

Best Regards, Christian