Questions about dummy instruction insertion (instructions from if-stage skid buffer can get lost)

Hello,

we are using IBEX with dummy instruction insertion and are doing formal verification experiments. We have observed that when a predicted branch is in the skid-buffer of the if-module (instr_skid_valid_q signal is high) and the stall_dummy_instr signal is high, then the skid-buffer valid signal is always cleared, also if the instruction of the skid buffer has not been transferred to the id-stage. With this the instruction from the skid-buffer can be completely lost. Is this behavior intended, because I think the branch needs to be evaluated to decide which succeeding instruction has to be executed, also if dummy instructions are inserted?

As second observation we have seen that the dummy instruction insertion is not considered when setting the valid signal of instructions for the id-stage (instr_valid_id_d). Is it intended that the dummy instruction insertion module can indicate the insertion of a dummy instruction and see the instruction as being transferred to the id-stage, but the instruction has not been sent as valid instruction to the id-stage because instr_valid_id_d is low and the dummy instruction insertion process is started new?

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:

31c5b5e