		Search-engine friendly clone of the ACL2 documentation.

Decoding

Get-opcode

Retrieve the opcode field of an instruction.

Signature
(get-opcode enc) → opcode
Arguments: enc — Guard (ubyte32p enc).
Returns: opcode — Type (ubyte7p opcode).

This is always in the low 7 bits of the 32-bit encoding [ISA:2.2] [ISA:2.3].

Definitions and Theorems

Function: get-opcode

(defun get-opcode (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (let ((__function__ 'get-opcode))
    (declare (ignorable __function__))
    (part-select enc :low 0 :high 6)))

Theorem: ubyte7p-of-get-opcode

(defthm ubyte7p-of-get-opcode
  (b* ((opcode (get-opcode enc)))
    (ubyte7p opcode))
  :rule-classes :rewrite)