• 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
        • Encoding
          • Encode
          • Encode-load-funct
          • Encode-store-funct
          • Encode-op-imms-32-funct
          • Encode-op-funct
          • Encode-op-32-funct
          • Encode-op-imms64-funct
          • Encode-op-imms32-funct
          • Encode-op-imm-funct
          • Encode-op-imm-32-funct
          • Encode-branch-funct
        • 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

Encoding

Encoding of instructions.

Instructions are encoded as specified in [ISA] and [ISAP]. Here we define encoding as a mapping from the instruction fixtypes to their encodings.

Without the C extension [ISA:26], instructions are encoded in 32 bits per instruction. So we define our mapping from instructions to 32-bit unsigned integers. We plan to model the C extension in the future: we will define a second encoding mapping, which maps certain instructions to 16 bits per instruction; the features will be also extended with an indication of whether the C extension is present.

Even without modeling the C extension yet, our encoding mapping depends on the features, because it is only defined on instructions that are valid according to the features.

Subtopics

Encode
Encode an instruction in the normal way (i.e. in 32 bits).
Encode-load-funct
Encode the name of an instruction with the LOAD opcode into the func3 field [ISA:2.6] [ISA:4.3] [ISA:34].
Encode-store-funct
Encode the name of an instruction with the STORE opcode into the funct3 field [ISA:2.6] [ISA:4.3] [ISA:34].
Encode-op-imms-32-funct
Encode the name of a shift instruction with the OP-IMM opcode into the funct3 field and the high 6 immediate bits [ISA:4.2.1] [ISA:34].
Encode-op-funct
Encode the name of an instruction with the OP opcode into the funct3 and funct7 fields [ISA:2.4.2] [ISA:13.1] [ISA:13.2] [ISA:34].
Encode-op-32-funct
Encode the name of an instruction with the OP-32 opcode into the funct3 and funct7 fields [ISA:4.2.2] [ISA:13.1] [ISA:13.2] [ISA:34].
Encode-op-imms64-funct
Encode the name of a 64-bit shift instruction with the OP-IMM opcode into the funct3 field and the high 6 immediate bits [ISA:4.2.1] [ISA:34].
Encode-op-imms32-funct
Encode the name of a 32-bit shift instruction with the OP-IMM opcode into the funct3 field and the high 7 immediate bits [ISA:2.4.1] [ISA:34].
Encode-op-imm-funct
Encode the name of a non-shift instruction with the OP-IMM opcode into the funct3 field [ISA:2.4.1] [ISA:34].
Encode-op-imm-32-funct
Encode the name of a non-shift instruction with the OP-IMM-32 opcode into the funct3 field [ISA:4.2.1] [ISA:34].
Encode-branch-funct
Encode the name of an instruction with the BRANCH opcode into the funct3 field [ISA:2.5.2] [ISA:34].