		Search-engine friendly clone of the ACL2 documentation.

Decoding

Get-rs2

Retrieve the rs2 field of an instruction.

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

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

Definitions and Theorems

Function: get-rs2

(defun get-rs2 (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (let ((__function__ 'get-rs2))
    (declare (ignorable __function__))
    (part-select enc :low 20 :high 24)))

Theorem: ubyte5p-of-get-rs2

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