Produce the vl-emodwire-ps for a bit-select.
(vl-msb-bitselect-bitlist x walist warnings) → (mv successp warnings bits)
We attempt to return the list of wires that correspond to this bit select. In practice this will be a singleton wire, or nil on failure. We are careful to ensure that the selected bit is in bounds, etc.
Function:
(defun vl-msb-bitselect-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-bitselect)))) (let ((__function__ 'vl-msb-bitselect-bitlist)) (declare (ignorable __function__)) (b* ((args (vl-nonatom->args x)) (from (first args)) (index (second args)) ((unless (and (vl-idexpr-p from) (vl-expr-resolved-p index) (natp (vl-resolved->val index)))) (mv nil (fatal :type :vl-bad-expr :msg "Expected a simple name and resolved index, but found ~ a0." :args (list x)) nil)) (name (vl-idexpr->name from)) (index (vl-resolved->val index)) (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 (eql index 0) (mv t (ok) wires) (mv nil (fatal :type :vl-bad-expr :msg "~w0 is a lone wire, but found ~a1." :args (list name x)) nil))) (name[i] (make-vl-emodwire :basename name :index index)) ((unless (member name[i] wires)) (mv nil (fatal :type :vl-bad-expr :msg "Select ~a0 is out of range: the valid bits are ~s1 ~ through ~s2." :args (list x (car wires) (car (last wires)))) nil))) (mv t (ok) (list name[i])))))
Theorem:
(defthm booleanp-of-vl-msb-bitselect-bitlist.successp (b* (((mv ?successp ?warnings ?bits) (vl-msb-bitselect-bitlist x walist warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-bitselect-bitlist.warnings (b* (((mv ?successp ?warnings ?bits) (vl-msb-bitselect-bitlist x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelist-p-of-vl-msb-bitselect-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-bitselect-bitlist x walist warnings))) (vl-emodwirelist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-bitselect-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-bitselect-bitlist x walist warnings))) (true-listp bits)) :rule-classes :type-prescription)