		Search-engine friendly clone of the ACL2 documentation.

Decoding

Decode

Decode an instruction.

Signature
(decode enc |64P|) → instr?
Arguments: enc — Guard (ubyte32p enc).; |64P| — Guard (booleanp |64P|).
Returns: instr? — Type (instr-optionp instr?).

The first input is a 32-bit encoding of the instruction; the second input is a flag distinguishing between RV64I (if t) and RV32I (if nil). 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 flag 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 |64P|)
 (declare (xargs :guard (and (ubyte32p enc) (booleanp |64P|))))
 (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 (load-funct-ld))
                      (4 (load-funct-lbu))
                      (5 (load-funct-lhu))
                      (6 (load-funct-lwu))
                      (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 |64P| (b* ((loimm (part-select imm :low 0 :high 5))
                          (hiimm (part-select imm :low 6 :high 11))
                          ((when (= funct3 1))
                           (if (= hiimm 0)
                               (instr-op-imms64 (op-imms-funct-slli)
                                                rd rs1 loimm)
                             nil)))
                       (case hiimm
                         (0 (instr-op-imms64 (op-imms-funct-srli)
                                             rd rs1 loimm))
                         (16 (instr-op-imms64 (op-imms-funct-srai)
                                              rd rs1 loimm))
                         (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)
                       (instr-op-imms32 (op-imms-funct-slli)
                                        rd rs1 loimm)
                     nil)))
               (case hiimm
                 (0 (instr-op-imms32 (op-imms-funct-srli)
                                     rd rs1 loimm))
                 (16 (instr-op-imms32 (op-imms-funct-srai)
                                      rd rs1 loimm))
                 (t nil))))))
     (23 (b* (((mv rd imm) (decode-utype enc)))
           (instr-auipc rd imm)))
     (27 (b* (((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 (store-funct-sd))
                       (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* (((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 |64P|)))
    (instr-optionp instr?))
  :rule-classes :rewrite)