		Search-engine friendly clone of the ACL2 documentation.

Decoding-executable

Get-rd

Retrieve the rd field of an instruction.

Signature
(get-rd enc) → rd
Arguments: enc — Guard (ubyte32p enc).
Returns: rd — Type (ubyte5p rd).

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

Definitions and Theorems

Function: get-rd

(defun get-rd (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (let ((__function__ 'get-rd))
    (declare (ignorable __function__))
    (part-select enc :low 7 :high 11)))

Theorem: ubyte5p-of-get-rd

(defthm ubyte5p-of-get-rd
  (b* ((rd (get-rd enc))) (ubyte5p rd))
  :rule-classes :rewrite)