		Search-engine friendly clone of the ACL2 documentation.

Encoding

Encode-branch-funct

Encode the name of an instruction with the BRANCH opcode into the funct3 field [ISA:2.5.2] [ISA:34].

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

Definitions and Theorems

Function: encode-branch-funct

(defun encode-branch-funct (funct)
  (declare (xargs :guard (branch-funct-p funct)))
  (let ((__function__ 'encode-branch-funct))
    (declare (ignorable __function__))
    (branch-funct-case funct
                       :beq 0
                       :bne 1
                       :blt 4
                       :bge 5
                       :bltu 6
                       :bgeu 7)))

Theorem: ubyte3p-of-encode-branch-funct

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

Theorem: encode-branch-funct-of-branch-funct-fix-funct

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

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

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