(vl-mark-wires-for-gateinst x alist warnings) → (mv new-alist new-warnings warning-wires)
Function:
(defun vl-mark-wires-for-gateinst (x alist warnings) (declare (xargs :guard (and (vl-gateinst-p x) (vl-wireinfo-alistp alist) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-mark-wires-for-gateinst)) (declare (ignorable __function__)) (b* ((args (vl-gateinst->args x)) (range (vl-gateinst->range x)) ((mv alist warning-wires) (vl-mark-wires-for-plainarglist args alist nil)) (warnings (if (not warning-wires) (ok) (warn :type :vl-gateinst-args-unresolved :msg "In ~a0, arguments are not resolved." :args (list x)))) (range-wires (vl-exprlist-names (vl-maybe-range-allexprs range))) (alist (vl-mark-wires-used range-wires t alist))) (mv alist warnings warning-wires))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-gateinst.new-alist (implies (and (force (vl-gateinst-p x)) (force (vl-wireinfo-alistp alist))) (b* (((mv ?new-alist ?new-warnings ?warning-wires) (vl-mark-wires-for-gateinst x alist warnings))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-mark-wires-for-gateinst.new-warnings (b* (((mv ?new-alist ?new-warnings ?warning-wires) (vl-mark-wires-for-gateinst x alist warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-mark-wires-for-gateinst.warning-wires (implies (and (force (vl-gateinst-p x)) (force (vl-wireinfo-alistp alist))) (b* (((mv ?new-alist ?new-warnings ?warning-wires) (vl-mark-wires-for-gateinst x alist warnings))) (string-listp warning-wires))) :rule-classes :rewrite)