		Search-engine friendly clone of the ACL2 documentation.

Decoding-executable

Get-imm-btype

Retrieve the immediate field of a B-type instruction.

Signature
(get-imm-btype enc) → imm
Arguments: enc — Guard (ubyte32p enc).
Returns: imm — Type (ubyte12p imm).

This consists of four chunks, in bits 8-11, 25-30, 7, and 31 [ISA:2.2], which, when joined, form the bits imm[12:1] of the immediate. We return those 12 bits, not imm[12:0] with imm[0] implicitly 0.

Definitions and Theorems

Function: get-imm-btype

(defun get-imm-btype (enc)
  (declare (xargs :guard (ubyte32p enc)))
  (b* ((imm[4.1] (part-select enc :low 8 :high 11))
       (imm[10.5] (part-select enc :low 25 :high 30))
       (imm[11] (part-select enc :low 7 :high 7))
       (imm[12] (part-select enc :low 31 :high 31)))
    (logappn 4 imm[4.1]
             6 imm[10.5] 1 imm[11] 1 imm[12])))

Theorem: ubyte12p-of-get-imm-btype

(defthm ubyte12p-of-get-imm-btype
  (b* ((imm (get-imm-btype enc)))
    (ubyte12p imm))
  :rule-classes :rewrite)