Illegal CHERI LOAD causing RTYPE instructions to not work correctly

[itsomaia]

Observed Behavior

We see a case that an illegal CHERI LOAD instruction is issued in the pipe, it does not get squashed and is sent for execution to the memory from where it picks up a data value that ends up blocking the execution of the RTYPE instruction for example an AND instruction shown in the waveform. We believe there are multiple issues here. (a) the illegal instruction should raise an exception and must be thrown out of the pipe and not sent to memory (b) Even if we waste pipeline cycles compromising performance and burning power executing an illegal instruction it must not interfere with the regular functionality of the processor's other instructions which it does. The problem is not just that it is impacting the RTYPE instructions but it gets compounded as STORE instructions would also not work correctly corrupting the memory picking up values from register file that they must not.

Let us know if you need the VCD.

Expected Behavior

Expected behaviour is to squash the illegal LOAD, raise an exception and not send it for execution to memory and also not let the end effect be to affect the other instructions such as RTYPE.

Steps to reproduce the issue

We use the formalISA app from Axiomise to run an ISA check to verify that the AND instruction in JasperGold. The property fails in 20 cycles.

My Environment

Integrated CHERIOT IBEX in formalISA

EDA tool and version: formalISA version 3.0, Cadence JasperGold 2023.09

Operating system: Ubuntu 22.04.01

Version of the Ibex source code: Don't have the branch number, but the RTL was downloaded on 17 July 2024

[kliuMsft]

Thanks much for working on cheriot-ibex! I am a little puzzle by the waveform though, for example it seems that JG thinks illegal_reg_cheri and data_req_o are both updated on the falling edge of clk_i, however in cheriot-ibex we use rising edge flops in all cases. Unfortunately I don't have access to formalISA, but if you can share VCD with more signals, I can try looking into this further.

[kliuMsft]

P.S., we did have an RTL fix related with illegal_reg_cheri on July 17 (see issue #40).

[itsomaia]

Thank you very much for your reply. We will pull the new fixed version and re-run the properties.

[itsomaia]

After re-running our assertions, we identified a new issue with bit manipulation instructions related to illegal_reg_cheri and have reported it(see issue #51 ).