		Search-engine friendly clone of the ACL2 documentation.

Encoding

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:35].

Signature
(encode-op-imm-funct funct) → funct3
Arguments: funct — Guard (op-imm-funct-p funct).
Returns: funct3 — Type (ubyte3p funct3).

Definitions and Theorems

Function: encode-op-imm-funct

(defun encode-op-imm-funct (funct)
  (declare (xargs :guard (op-imm-funct-p funct)))
  (op-imm-funct-case funct
                     :addi 0
                     :slti 2
                     :sltiu 3
                     :andi 7
                     :ori 6
                     :xori 4))

Theorem: ubyte3p-of-encode-op-imm-funct

(defthm ubyte3p-of-encode-op-imm-funct
  (b* ((funct3 (encode-op-imm-funct funct)))
    (ubyte3p funct3))
  :rule-classes :rewrite)

Theorem: encode-op-imm-funct-of-op-imm-funct-fix-funct

(defthm encode-op-imm-funct-of-op-imm-funct-fix-funct
  (equal (encode-op-imm-funct (op-imm-funct-fix funct))
         (encode-op-imm-funct funct)))

Theorem: encode-op-imm-funct-op-imm-funct-equiv-congruence-on-funct

(defthm encode-op-imm-funct-op-imm-funct-equiv-congruence-on-funct
  (implies (op-imm-funct-equiv funct funct-equiv)
           (equal (encode-op-imm-funct funct)
                  (encode-op-imm-funct funct-equiv)))
  :rule-classes :congruence)