		Search-engine friendly clone of the ACL2 documentation.

Get-opcode

Retrieve the opcode field of an instruction.

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

Function: get-opcode

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