Produce the vl-emodwire-ps for a part-select.
(vl-msb-partselect-bitlist x walist warnings) → (mv successp warnings bits)
We attempt to return the list of wires that correspond to this part select, in MSB order. We are careful to ensure that the range is resolved, the indices are in bounds, and so on.
Function:
(defun vl-msb-partselect-bitlist (x walist warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-wirealist-p walist) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (not (vl-atom-p x)) (equal (vl-nonatom->op x) :vl-partselect-colon)))) (let ((__function__ 'vl-msb-partselect-bitlist)) (declare (ignorable __function__)) (b* ((args (vl-nonatom->args x)) (from (first args)) (left (second args)) (right (third args)) ((unless (and (vl-idexpr-p from) (vl-expr-resolved-p left) (vl-expr-resolved-p right))) (mv nil (fatal :type :vl-bad-expr :msg "Expected a simple name and resolved indices, but ~ found ~a0." :args (list x)) nil)) (name (vl-idexpr->name from)) (left (vl-resolved->val left)) (right (vl-resolved->val right)) (entry (hons-get name walist)) ((unless entry) (mv nil (fatal :type :vl-bad-expr :msg "No wire-alist entry for ~w0." :args (list name)) nil)) (wires (llist-fix (cdr entry))) (plain-name (vl-plain-wire-name name)) ((when (equal wires (list plain-name))) (if (and (eql left 0) (eql right 0)) (mv t (warn :type :vl-select-from-scalar :msg "~a0: permitting selecting bit 0 from a scalar ~ wire, but this is probably wrong." :args (list x)) wires) (mv nil (fatal :type :vl-bad-expr :msg "~w0 is a lone wire, but found ~a1." :args (list name x)) nil))) (name[left] (make-vl-emodwire :basename name :index left)) (name[right] (make-vl-emodwire :basename name :index right)) ((unless (and (member name[left] wires) (member name[right] wires))) (mv nil (fatal :type :vl-bad-expr :msg "Select ~a0 is out of range; valid range is from ~x1 ~ to ~x2." :args (list x (car wires) (car (last wires)))) nil))) (mv t (ok) (vl-emodwires-from-msb-to-lsb name left right)))))
Theorem:
(defthm booleanp-of-vl-msb-partselect-bitlist.successp (b* (((mv ?successp ?warnings ?bits) (vl-msb-partselect-bitlist x walist warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-partselect-bitlist.warnings (b* (((mv ?successp ?warnings ?bits) (vl-msb-partselect-bitlist x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-msb-partselect-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-partselect-bitlist x walist warnings))) (vl-emodwirelist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-partselect-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-partselect-bitlist x walist warnings))) (true-listp bits)) :rule-classes :type-prescription)