		Search-engine friendly clone of the ACL2 documentation.

Bitops/part-select

Part-select

Select a portion of bits from an integer that represents a bit vector

part-select is a macro that lets you write code to extract parts of vectors. For instance:

(part-select foo :low 10 :high 17)   ;; Like foo[17:10] in Verilog

You can also using an index/size, e.g.:

(part-select foo :low 10 :width 7)   ;; Like foo[16:10] in Verilog

Macro: part-select

(defmacro part-select (x &key low high width)
 (cond
  ((and high width)
   (er hard? 'part-select
       "Can't use :high and :width together"))
  ((and low high)
   (cons 'part-select-low-high
         (cons x (cons low (cons high 'nil)))))
  ((and low width)
   (cons 'part-select-width-low
         (cons x (cons width (cons low 'nil)))))
  (t (er hard? 'part-select
         "Need at least :low and :width, or else :low and :high"))))

Definitions and Theorems

Function: part-select-width-low$inline

(defun part-select-width-low$inline (x width low)
  (declare (xargs :guard (and (integerp x)
                              (natp width)
                              (natp low))))
  (mbe :logic (loghead width (logtail low x))
       :exec (logand (1- (ash 1 width))
                     (ash x (- low)))))

Function: part-select-low-high$inline

(defun part-select-low-high$inline (x low high)
  (declare (xargs :guard (and (integerp x)
                              (natp low)
                              (natp high)
                              (<= low high))))
  (part-select-width-low x (+ 1 (- high low))
                         low))