Produce the vl-emodwire-ps for a vl-constint-p.
(vl-msb-constint-bitlist x warnings) → (mv successp warnings bits)
In E modules, the symbols
We are given an atomic, constant integer expression. This expression has
some width and value. We return a width-long list of symbols
Function:
(defun vl-msb-constint-bitlist (x warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (vl-atom-p x) (vl-constint-p (vl-atom->guts x))))) (let ((__function__ 'vl-msb-constint-bitlist)) (declare (ignorable __function__)) (b* ((width (vl-atom->finalwidth x)) (guts (vl-atom->guts x)) (value (vl-constint->value guts)) ((unless width) (mv nil (fatal :type :vl-programming-error :msg "Cannot generate wires for ~a0 because it does not ~ have a finalwidth." :args (list x)) nil)) (bits (vl-msb-constint-bitlist-aux value nil)) (blen (length bits)) ((when (equal blen width)) (mv t (ok) bits)) ((when (< blen width)) (mv t (ok) (make-list-ac (- width blen) 'acl2::f bits)))) (mv nil (fatal :type :vl-programming-error :msg "Produced too many wires for ~a0. Finalwidth: ~x1. ~x2 ~ Bits: ~x3." :args (list x (vl-atom->finalwidth x) blen bits)) nil))))
Theorem:
(defthm booleanp-of-vl-msb-constint-bitlist.successp (b* (((mv ?successp ?warnings ?bits) (vl-msb-constint-bitlist x warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-constint-bitlist.warnings (b* (((mv ?successp ?warnings ?bits) (vl-msb-constint-bitlist x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-msb-constint-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-constint-bitlist x warnings))) (vl-emodwirelist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-constint-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-constint-bitlist x warnings))) (true-listp bits)) :rule-classes :type-prescription)