Decoding
Decoding of instructions.
Instructions are encoded as specified in [ISA] and [ISAP],
and as formalized in encoding.
We define an executable decoder that maps the encodings of instructions
to the corresponding instruction fixtypes
defined in instructions.
Currently we only cover the decoding of
the instructions defined in instructions.
We only handle the normal encodings,
i.e. not the compressed ones in the C extension [ISA:26];
thus, our decoder operates on 32-bit encodings.
Subtopics
- Decode
- Decode an instruction.
- Decoding-of-encoding
- Theorems about decoding applied to encoding.
- Get-fields-rtype
- Retrieve the non-opcode fields of an R-type instruction
[ISA:2.2] [ISA:2.3].
- Get-fields-stype
- Retrieve the non-opcode fields of an S-type instruction
[ISA:2.2] [ISA:2.3].
- Get-fields-itype
- Retrieve the non-opcode fields of an I-type instruction
[ISA:2.2] [ISA:2.3].
- Get-fields-btype
- Retrieve the non-opcode fields of a B-type instruction
[ISA:2.3].
- Encoding-of-decoding
- Encoding applied to decoding.
- Get-imm-jtype
- Retrieve the immediate field of a J-type instruction.
- Get-imm-btype
- Retrieve the immediate field of a B-type instruction.
- Get-imm-utype
- Retrieve the immediate field of a U-type instruction.
- Get-fields-utype
- Retrieve the non-opcode fields of a U-type instruction
[ISA:2.2] [ISA:2.3].
- Get-imm-stype
- Retrieve the immediate field of an S-type instruction.
- Get-imm-itype
- Retrieve the immediate field of an I-type instruction.
- Get-fields-jtype
- Retrieve the non-opcode fields of a J-type instruction
[ISA:2.3].
- Decoding-as-inverse
- Declarative definition of decoding as inverse of encoding.
- Get-rs2
- Retrieve the rs2 field of an instruction.
- Get-rs1
- Retrieve the rs1 field of an instruction.
- Get-rd
- Retrieve the rd field of an instruction.
- Get-opcode
- Retrieve the opcode field of an instruction.
- Get-funct7
- Retrieve the funct7 field of an instruction.
- Get-funct3
- Retrieve the funct3 field of an instruction.
