For RV32I, SLLI, SRLI, and SRAI generate an illegal instruction exception if imm[5] != 0

[darbaria]

Bug Title

USer ISA page 30 states that for RV32I, SLLI, SRLI, and SRAI generate an illegal instruction exception if imm[5] != 0

APP: formalISA

parameter PULP_XPULP = 0
parameter PULP_CLUSTER = 0

Assertion vacuity failure. An assertion stating that on a valid decode of a SRRLI/SRAI/SRLI when imm[5] !=0 raises an exception fails the vacuity check. On further analysis, we are able to prove that by construction the imm[5] bit can never be 1 on a decode of SRRLI/SRAI/SRLI. The imm[5] bit can be 1 at other times but never in this case. So by construction, the design can never decode and detect this illegal condition.This seems inconsistent with the RISC-V specification.

There is no waveform to show here.

[davideschiavone]

Hello @darbaria ,

I think there is a mistake somewhere in the setup.

I tried to execute

srli x0,x0,0x1F

that would be:

01f05013

0000000 11111 00000 101 00000 0010011

and it works. Then I executed

03f05013

0000001 11111 00000 101 00000 0010011

As you see, the bit25 is now 1, which would be your immediate[5].

The core traps in the illegal instruction. Attached the screenshot of the waves

[darbaria]

@davideschiavone just to be clear, when we decode a legal SLLI/SRLI/SRAI by construction the opcode will ensure that imm[5] i.e., instr[25] cannot be 1. This is the reason my assert fails vacuity as both conditions cannot be met.

I read the line in the RISC-V ISA spec " For RV32I, SLLI, SRLI, and SRAI generate an illegal instruction exception if imm[5] != 0" to mean that when we are decoding one of these shift instructions and imm[5] is 1 the design must generate an exception. It looks like this sentece is inconsistent with the OP decode definition of these instructions in the ISA spec.

Note: I can also see illegal_insn_o pin going high when bit [25] is 1 for other cases but not in this case. Also, my ISA checks for SRLI/SRAI/SLLI prove that they work correctly for this processor.

[davideschiavone]

Hello @darbaria ,

indeed I am injcting in the assembly an hexadecimal value (by passing the compiler), not the instruction per se, otherwise I could not exercise the illegal instruction.

In the example before I executed:

0x03F05013

which is

0000001 11111 00000 101 00000 0010011

the bit 25 is 1

and the OPCODE is the OP-IMM, the funct3 101 is the SRLI

page 130: https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf

[darbaria]

As per the 1:1 chat with @davideschiavone it is agreed that this issue is an ISA bug in the RISC-V v 2.2. We cannot build a RISC-V machine that can decode these shift instructions as well as raise exception for imm[5]. Interestingly, in the ratified ISA specification this requirement has been dropped off.