Produce the vl-emodwire-ps for a vl-id-p.
(vl-msb-wire-bitlist x walist warnings) → (mv successp warnings bits)
We are given an atomic, identifier expression. This expression has some width and refers to a particular wire. We return a wires associated with this name in MSB order.
Function:
(defun vl-msb-wire-bitlist (x walist warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-wirealist-p walist) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (vl-atom-p x) (vl-id-p (vl-atom->guts x))))) (let ((__function__ 'vl-msb-wire-bitlist)) (declare (ignorable __function__)) (b* ((width (vl-atom->finalwidth x)) (guts (vl-atom->guts x)) (name (vl-id->name guts)) ((unless (posp width)) (mv nil (fatal :type :vl-programming-error :msg "Expected only sized expressions, but ~a0 does not ~ have a finalwidth." :args (list x)) nil)) (wires (llist-fix (cdr (hons-get name walist)))) ((unless (and (consp wires) (mbt (vl-emodwirelist-p wires)))) (mv nil (fatal :type :vl-bad-id :msg "No wires for ~a0." :args (list name)) nil)) (nwires (length wires)) ((when (< width nwires)) (mv nil (fatal :type :vl-programming-error :msg "Produced too many wires for ~a0. Finalwidth is ~x1, ~ but produced ~x2 bits: ~x3." :args (list x (vl-atom->finalwidth x) nwires wires)) nil)) ((when (eql nwires width)) (mv t (ok) wires)) (type (vl-atom->finaltype x)) (extension-bit (if (eq type :vl-signed) (car wires) 'acl2::f)) (wires (append (replicate (- width nwires) extension-bit) wires))) (mv t (ok) wires))))
Theorem:
(defthm booleanp-of-vl-msb-wire-bitlist.successp (b* (((mv ?successp ?warnings ?bits) (vl-msb-wire-bitlist x walist warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-wire-bitlist.warnings (b* (((mv ?successp ?warnings ?bits) (vl-msb-wire-bitlist x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-msb-wire-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-wire-bitlist x walist warnings))) (vl-emodwirelist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-wire-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-wire-bitlist x walist warnings))) (true-listp bits)) :rule-classes :type-prescription)