		Search-engine friendly clone of the ACL2 documentation.

Vl-constint-p

Vl-constint->msb-bits

Explode a well-typed vl-constint-p atom into MSB-ordered vl-bitlist-p.

Signature
(vl-constint->msb-bits x) → bits
Arguments: x — Guard (vl-expr-p x).
Returns: bits — Type (vl-bitlist-p bits).

We require that X is a well-typed constant integer expression, i.e., our expression-sizing transform should have already been run. Note that the "propagation step" of expression sizing should have already handled any sign/zero extensions, so we assume here that the atom's finalwidth is already correct and that no extensions are necessary.

Definitions and Theorems

Function: vl-constint->msb-bits

(defun vl-constint->msb-bits (x)
  (declare (xargs :guard (vl-expr-p x)))
  (declare
       (xargs :guard (and (vl-atom-p x)
                          (vl-atom-welltyped-p x)
                          (vl-fast-constint-p (vl-atom->guts x)))))
  (let ((__function__ 'vl-constint->msb-bits))
    (declare (ignorable __function__))
    (vl-constint-msb-bits-aux (vl-atom->finalwidth x)
                              (vl-constint->value (vl-atom->guts x))
                              nil)))

Theorem: vl-bitlist-p-of-vl-constint->msb-bits

(defthm vl-bitlist-p-of-vl-constint->msb-bits
  (b* ((bits (vl-constint->msb-bits x)))
    (vl-bitlist-p bits))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-constint->msb-bits

(defthm true-listp-of-vl-constint->msb-bits
  (true-listp (vl-constint->msb-bits x))
  :rule-classes :type-prescription)

Theorem: len-of-vl-constint->msb-bits

(defthm len-of-vl-constint->msb-bits
  (equal (len (vl-constint->msb-bits x))
         (nfix (vl-atom->finalwidth x))))

Theorem: vl-constint->msb-bits-of-vl-expr-fix-x

(defthm vl-constint->msb-bits-of-vl-expr-fix-x
  (equal (vl-constint->msb-bits (vl-expr-fix x))
         (vl-constint->msb-bits x)))

Theorem: vl-constint->msb-bits-vl-expr-equiv-congruence-on-x

(defthm vl-constint->msb-bits-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-constint->msb-bits x)
                  (vl-constint->msb-bits x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-constint-lsb-bits-aux
Vl-constint-msb-bits-aux: Accumulate lsb's into acc, which produces an MSB-ordered list.