		Search-engine friendly clone of the ACL2 documentation.

Decoding

Get-funct7

Retrieve the funct7 field of an instruction.

Signature
(get-funct7 enc) → funct7
Arguments: enc — Guard (ubyte32p enc).
Returns: funct7 — Type (ubyte7p funct7).

This is always in the bits 25-31 of the 32-bit encoding, for the formats with an funct7 field [ISA:2.2] [ISA:2.3].

Definitions and Theorems

Function: get-funct7

(defun get-funct7 (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (let ((__function__ 'get-funct7))
    (declare (ignorable __function__))
    (part-select enc :low 25 :high 31)))

Theorem: ubyte7p-of-get-funct7

(defthm ubyte7p-of-get-funct7
  (b* ((funct7 (get-funct7 enc)))
    (ubyte7p funct7))
  :rule-classes :rewrite)