		Search-engine friendly clone of the ACL2 documentation.

Decoding

Get-funct3

Retrieve the funct3 field of an instruction.

Signature
(get-funct3 enc) → funct3
Arguments: enc — Guard (ubyte32p enc).
Returns: funct3 — Type (ubyte3p funct3).

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

Definitions and Theorems

Function: get-funct3

(defun get-funct3 (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (let ((__function__ 'get-funct3))
    (declare (ignorable __function__))
    (part-select enc :low 12 :high 14)))

Theorem: ubyte3p-of-get-funct3

(defthm ubyte3p-of-get-funct3
  (b* ((funct3 (get-funct3 enc)))
    (ubyte3p funct3))
  :rule-classes :rewrite)