• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
        • Instructions
        • States
        • Decoding
          • Decode
          • Decode-rtype
          • Decode-stype
          • Decode-itype
          • Decode-btype
          • Get-imm-jtype
          • Get-imm-btype
          • Get-imm-utype
          • Get-imm-stype
          • Get-imm-itype
          • Decode-utype
          • Decode-jtype
          • Get-rs2
          • Get-rs1
          • Get-rd
          • Get-opcode
          • Get-funct7
          • Get-funct3
        • Encoding
        • Features
        • Semantics
        • Execution
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Riscv

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.
Decode-rtype
Retrieve the non-opcode fields of an R-type instruction [ISA:2.2] [ISA:2.3].
Decode-stype
Retrieve the non-opcode fields of an S-type instruction [ISA:2.2] [ISA:2.3].
Decode-itype
Retrieve the non-opcode fields of an I-type instruction [ISA:2.2] [ISA:2.3].
Decode-btype
Retrieve the non-opcode fields of a B-type instruction [ISA:2.3].
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-imm-stype
Retrieve the immediate field of an S-type instruction.
Get-imm-itype
Retrieve the immediate field of an I-type instruction.
Decode-utype
Retrieve the non-opcode fields of a U-type instruction [ISA:2.2] [ISA:2.3].
Decode-jtype
Retrieve the non-opcode fields of a J-type instruction [ISA:2.3].
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.