• 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

• Decoding

Decode

Decode an instruction.

Signature

(decode enc feat) → instr?

Arguments

enc — Guard (ubyte32p enc).

feat — Guard (featp feat).

Returns

instr? — Type (instr-optionp instr?).

The first input is a 32-bit encoding of the instruction; the second input consists of the features, which affect decoding. If decoding is successful, we return the instruction. If decoding is unsuccessful, we return nil.

The values of the encoded fields, which we write in binary notation, are taken from the instruction listings in [ISA:34].

We retrieve the opcode, and we dispatch based on it. Each dispatch first retrieves the fields, based on the format, and then checks them to see whether they are valid, and to determine which instruction is encoded, if any.

With the OP-IMM opcode, shift instructions are encoded in a specialization of the I-type format, where the low 5 or 6 bits of the immediate are the shift amount, while the high 7 or 6 bits need to have specific values. Whether the immediate is split into 5 low bits and 7 high bits, or into 6 low bits and 6 high bits, depends on whether we are in RV32I or RV64I mode, so we use the features passed as input to this function. We generate slightly different shift instructions, in the two cases.

With the OP-IMM-32 opcode, shift instructions are encoded in a specialization of the I-type format, where the low 5 bits of the immediate are the shift amount, while the high 7 bits need to have specific values.

Definitions and Theorems

Function: decode

(defun decode (enc feat)
  (declare (xargs :guard (and (ubyte32p enc) (featp feat))))
  (let ((__function__ 'decode))
    (declare (ignorable __function__))
    (case (get-opcode enc)
      (3 (b* (((mv funct3 rd rs1 imm)
               (decode-itype enc))
              (funct (case funct3
                       (0 (load-funct-lb))
                       (1 (load-funct-lh))
                       (2 (load-funct-lw))
                       (3 (if (feat-64p feat)
                              (load-funct-ld)
                            nil))
                       (4 (load-funct-lbu))
                       (5 (load-funct-lhu))
                       (6 (if (feat-64p feat)
                              (load-funct-lwu)
                            nil))
                       (7 nil)))
              ((unless funct) nil))
           (instr-load funct rd rs1 imm)))
      (19 (b* (((mv funct3 rd rs1 imm)
                (decode-itype enc))
               (funct (case funct3
                        (0 (op-imm-funct-addi))
                        (1 nil)
                        (2 (op-imm-funct-slti))
                        (3 (op-imm-funct-sltiu))
                        (4 (op-imm-funct-xori))
                        (5 nil)
                        (6 (op-imm-funct-ori))
                        (7 (op-imm-funct-andi))))
               ((when funct)
                (instr-op-imm funct rd rs1 imm)))
            (if (feat-64p feat)
                (b* ((loimm (part-select imm :low 0 :high 5))
                     (hiimm (part-select imm :low 6 :high 11))
                     ((when (= funct3 1))
                      (if (= hiimm 0)
                          (if (feat-64p feat)
                              (instr-op-imms64 (op-imms-funct-slli)
                                               rd rs1 loimm)
                            nil)
                        nil)))
                  (case hiimm
                    (0 (if (feat-64p feat)
                           (instr-op-imms64 (op-imms-funct-srli)
                                            rd rs1 loimm)
                         nil))
                    (16 (if (feat-64p feat)
                            (instr-op-imms64 (op-imms-funct-srai)
                                             rd rs1 loimm)
                          nil))
                    (t nil)))
              (b* ((loimm (part-select imm :low 0 :high 4))
                   (hiimm (part-select imm :low 5 :high 11))
                   ((when (= funct3 1))
                    (if (= hiimm 0)
                        (if (feat-32p feat)
                            (instr-op-imms32 (op-imms-funct-slli)
                                             rd rs1 loimm)
                          nil)
                      nil)))
                (case hiimm
                  (0 (if (feat-32p feat)
                         (instr-op-imms32 (op-imms-funct-srli)
                                          rd rs1 loimm)
                       nil))
                  (16 (if (feat-32p feat)
                          (instr-op-imms32 (op-imms-funct-srai)
                                           rd rs1 loimm)
                        nil))
                  (t nil))))))
      (23 (b* (((mv rd imm) (decode-utype enc)))
            (instr-auipc rd imm)))
      (27 (b* (((unless (feat-64p feat)) nil)
               ((mv funct3 rd rs1 imm)
                (decode-itype enc))
               ((when (= funct3 0))
                (instr-op-imm-32 (op-imm-32-funct-addiw)
                                 rd rs1 imm))
               (loimm (part-select imm :low 0 :high 4))
               (hiimm (part-select imm :low 5 :high 11))
               ((when (= funct3 1))
                (if (= hiimm 0)
                    (instr-op-imms-32 (op-imms-32-funct-slliw)
                                      rd rs1 loimm)
                  nil))
               ((when (= funct3 5))
                (case hiimm
                  (0 (instr-op-imms-32 (op-imms-32-funct-srliw)
                                       rd rs1 loimm))
                  (32 (instr-op-imms-32 (op-imms-32-funct-sraiw)
                                        rd rs1 loimm))
                  (t nil))))
            nil))
      (35 (b* (((mv funct3 rs1 rs2 imm)
                (decode-stype enc))
               (funct (case funct3
                        (0 (store-funct-sb))
                        (1 (store-funct-sh))
                        (2 (store-funct-sw))
                        (3 (if (feat-64p feat)
                               (store-funct-sd)
                             nil))
                        (t nil)))
               ((unless funct) nil))
            (instr-store funct rs1 rs2 imm)))
      (51 (b* (((mv funct3 funct7 rd rs1 rs2)
                (decode-rtype enc))
               (funct (case funct3
                        (0 (case funct7
                             (0 (op-funct-add))
                             (1 (op-funct-mul))
                             (32 (op-funct-sub))
                             (t nil)))
                        (1 (case funct7
                             (0 (op-funct-sll))
                             (1 (op-funct-mulh))
                             (t nil)))
                        (2 (case funct7
                             (0 (op-funct-slt))
                             (1 (op-funct-mulhsu))
                             (t nil)))
                        (3 (case funct7
                             (0 (op-funct-sltu))
                             (1 (op-funct-mulhu))
                             (t nil)))
                        (4 (case funct7
                             (0 (op-funct-xor))
                             (1 (op-funct-div))
                             (t nil)))
                        (5 (case funct7
                             (0 (op-funct-srl))
                             (1 (op-funct-divu))
                             (32 (op-funct-sra))
                             (t nil)))
                        (6 (case funct7
                             (0 (op-funct-or))
                             (1 (op-funct-rem))
                             (t nil)))
                        (7 (case funct7
                             (0 (op-funct-and))
                             (1 (op-funct-remu))
                             (t nil)))))
               ((unless funct) nil))
            (instr-op funct rd rs1 rs2)))
      (55 (b* (((mv rd imm) (decode-utype enc)))
            (instr-lui rd imm)))
      (59 (b* (((unless (feat-64p feat)) nil)
               ((mv funct3 funct7 rd rs1 rs2)
                (decode-rtype enc))
               (funct (case funct3
                        (0 (case funct7
                             (0 (op-32-funct-addw))
                             (1 (op-32-funct-mulw))
                             (32 (op-32-funct-subw))
                             (t nil)))
                        (1 (case funct7
                             (0 (op-32-funct-sllw))
                             (t nil)))
                        (2 nil)
                        (3 nil)
                        (4 (case funct7
                             (1 (op-32-funct-divw))
                             (t nil)))
                        (5 (case funct7
                             (0 (op-32-funct-srlw))
                             (1 (op-32-funct-divuw))
                             (32 (op-32-funct-sraw))
                             (t nil)))
                        (6 (case funct7
                             (1 (op-32-funct-remw))
                             (t nil)))
                        (7 (case funct7
                             (1 (op-32-funct-remuw))
                             (t nil)))))
               ((unless funct) nil))
            (instr-op-32 funct rd rs1 rs2)))
      (99 (b* (((mv funct3 rs1 rs2 imm)
                (decode-btype enc))
               (funct (case funct3
                        (0 (branch-funct-beq))
                        (1 (branch-funct-bne))
                        (2 nil)
                        (3 nil)
                        (4 (branch-funct-blt))
                        (5 (branch-funct-bge))
                        (6 (branch-funct-bltu))
                        (7 (branch-funct-bgeu))))
               ((unless funct) nil))
            (instr-branch funct rs1 rs2 imm)))
      (103 (b* (((mv funct3 rd rs1 imm)
                 (decode-itype enc))
                ((unless (= funct3 0)) nil))
             (instr-jalr rd rs1 imm)))
      (111 (b* (((mv rd imm) (decode-jtype enc)))
             (instr-jal rd imm)))
      (t nil))))

Theorem: instr-optionp-of-decode

(defthm instr-optionp-of-decode
  (b* ((instr? (decode enc feat)))
    (instr-optionp instr?))
  :rule-classes :rewrite)