		Search-engine friendly clone of the ACL2 documentation.

Encoding

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

Signature
(encode-op-funct funct) → (mv funct3 funct7)
Arguments: funct — Guard (op-funct-p funct).
Returns: funct3 — Type (ubyte3p funct3).; funct7 — Type (ubyte7p funct7).

Definitions and Theorems

Function: encode-op-funct

(defun encode-op-funct (funct)
  (declare (xargs :guard (op-funct-p funct)))
  (let ((__function__ 'encode-op-funct))
    (declare (ignorable __function__))
    (op-funct-case funct
                   :add (mv 0 0)
                   :sub (mv 0 32)
                   :slt (mv 2 0)
                   :sltu (mv 3 0)
                   :and (mv 7 0)
                   :or (mv 6 0)
                   :xor (mv 4 0)
                   :sll (mv 1 0)
                   :srl (mv 5 0)
                   :sra (mv 5 32)
                   :mul (mv 0 1)
                   :mulh (mv 1 1)
                   :mulhu (mv 3 1)
                   :mulhsu (mv 2 1)
                   :div (mv 4 1)
                   :divu (mv 5 1)
                   :rem (mv 6 1)
                   :remu (mv 7 1))))

Theorem: ubyte3p-of-encode-op-funct.funct3

(defthm ubyte3p-of-encode-op-funct.funct3
  (b* (((mv ?funct3 ?funct7)
        (encode-op-funct funct)))
    (ubyte3p funct3))
  :rule-classes :rewrite)

Theorem: ubyte7p-of-encode-op-funct.funct7

(defthm ubyte7p-of-encode-op-funct.funct7
  (b* (((mv ?funct3 ?funct7)
        (encode-op-funct funct)))
    (ubyte7p funct7))
  :rule-classes :rewrite)

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

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

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

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