RORI is decoded as legal when it should not be

[itsomaia]

Observed Behavior

The RISC-V ISA for bit manipulation states that for the 32-bit implementations of the ISA, for the RORI instruction the bit 25 needs to be 1'b0. However, in the implementation we have downloaded from the Github on 17 July 2024, an instruction could be considered to be a valid RORI despite the bit 25 being 1'b1. It means there are two ways to decode the same instruction which means it is prone to security vulnerabilities and it does not comply with the ISA.

Expected Behavior

To not classify an instruction as RORI when bit 25 is non-zero. Perhaps mark it as illegal.

Steps to reproduce the issue

Running formalISA v 3.0 app with Cadence JasperGold 2023.09, a cover that should have failed ends up passing.

My Environment

Running formalISA v 3.0 app with Cadence JasperGold 2023.09

EDA tool and version: Running formalISA v 3.0 app with Cadence JasperGold 2023.09

Operating system:

Ubuntu 22.04.01

Version of the Ibex source code:

[kliuMsft]

Thanks for investigating. @marnovandermaas, is this something fixed in the upstream ibex?

[itsomaia]

Thank you very much for your quick reply. There is the same issue with other bit manipulation instructions that use the OP-IMM opcode, such as instructions BINVI, BEXTI,BCLRI, REV8 and BSETI.

[kliuMsft]

@itsomaia, looks like the issue also exists in the upstream ibex (https://github.com/lowRISC/ibex). Come to think about it, in the RORI case, bit 25 is bit 5 of SHAMT and marked as "reserved" in the ISA extension spec. I think in RiSC-V it's actually not a requirement to generate illegal insn exception in such cases (considered implementation-dependent). Maybe that's part of the reason why it's not fixed..

[marnovandermaas]

Yes, I think there are more examples in Ibex where the decode takes a shortcut expecting that the compiler does the sensible thing and not generate reserved instructions. Doing a full decode that covers all of these cases would require more area and I don't see the benefit at the moment.

[itsomaia]

The problem with your argument is that just saving area is not enough. Area is part of PPA analysis. Power is equally important especially if the processor is going to be used for IOT. By decoding illegal instructions as legal we are sending them for execution to the pipe burning power. We can't simply expect a compiler to generate the correct (expected encodings for the opcode) unless the compiler is verifiably correct. Given an enormous amount of work has gone in in creating a secure processor such as cheriot-ibex it'd would be good to address these issues, we will be happy to help formally verify the fixes are correct.

[marnovandermaas]

I'm not sure I understand the power argument because coming across reserved instructions should be very rare in normal operation. I will also mention that the RISC-V instruction set architecture specifies that decoding a reserved instruction is unspecified, so what Ibex does conforms to the specification:

[rmn30]

I agree we don't really care what this case does providing it is not something really weird like returning a valid capability. Assuming it is something sensible like ignoring bit 5 I think it is OK. However, arguments in favour of raising a reserved instruction exception are:

1. It helps with debugging / error detection.
2. It allows the software to catch and emulate the reserved instruction, which might be relevant in case some future version of the specification makes it defined.
3. We need some defined behaviour in order to complete formal verification.

[itsomaia]

Thank you for your response. We also discovered that bit 26, which isn't defined as reserved and must be set to 0, may vary and still be identified as a valid BINVI, BCLRI, or BSETI instruction. These cases have been filed separately as issues #48, #49, and #50.

[kliuMsft]

@itsomaia, commit 94aeb07 should fix the issue along with issues https://github.com/microsoft/cheriot-ibex/issues/48, https://github.com/microsoft/cheriot-ibex/issues/49, and https://github.com/microsoft/cheriot-ibex/issues/50. Please verify. Thanks,