		Search-engine friendly clone of the ACL2 documentation.

Encoding

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

Signature
(encode-op-imms-32-funct funct) → (mv funct3 hi6imm)
Arguments: funct — Guard (op-imms-32-funct-p funct).
Returns: funct3 — Type (ubyte3p funct3).; hi6imm — Type (ubyte6p hi6imm).

Definitions and Theorems

Function: encode-op-imms-32-funct

(defun encode-op-imms-32-funct (funct)
  (declare (xargs :guard (op-imms-32-funct-p funct)))
  (op-imms-32-funct-case funct
                         :slliw (mv 1 0)
                         :srliw (mv 5 0)
                         :sraiw (mv 5 16)))

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

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

Theorem: ubyte6p-of-encode-op-imms-32-funct.hi6imm

(defthm ubyte6p-of-encode-op-imms-32-funct.hi6imm
  (b* (((mv ?funct3 ?hi6imm)
        (encode-op-imms-32-funct funct)))
    (ubyte6p hi6imm))
  :rule-classes :rewrite)

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

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

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

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