		Search-engine friendly clone of the ACL2 documentation.

Decoding-executable

Get-rs1

Retrieve the rs1 field of an instruction.

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

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

Definitions and Theorems

Function: get-rs1

(defun get-rs1 (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (let ((__function__ 'get-rs1))
    (declare (ignorable __function__))
    (part-select enc :low 15 :high 19)))

Theorem: ubyte5p-of-get-rs1

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