		Search-engine friendly clone of the ACL2 documentation.

Get-rs1

Retrieve the rs1 field of an instruction.

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].

Function: get-rs1

(defun get-rs1 (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (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)