BINVI Decode Not Legal

[itsomaia]

Observed Behavior

According to the RISC-V ISA, for the BINVI instruction, bit 26 must be 0, and bit 25 should also be 0. However, in the case of CHERIOT-IBEX, as shown in the waveform, the instruction is still decoded as BINVI even when both bits are set to 1.

Expected Behavior

This instruction not to be decoded as BINVI. The instruction decoded as BINVI is not a BINVI instruction as the bits 26:25 need to be 2'b00 as per the ISA. The challenge with decoding instructions as legal when they are not implies security vulnerabilities. A trojan with bits 26:25 being 2'b00 would be considered a legal BINVI instruction and will be sent to the pipe for execution and can execute malicious code. I believe this must be investigated along with other issues we have filed such as #47

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: