(vl-mark-wires-for-assignment x alist) → new-alist
Function:
(defun vl-mark-wires-for-assignment (x alist) (declare (xargs :guard (and (vl-assign-p x) (vl-wireinfo-alistp alist)))) (let ((__function__ 'vl-mark-wires-for-assignment)) (declare (ignorable __function__)) (b* ((lvalue (vl-assign->lvalue x)) (rhs (vl-assign->expr x)) (alist (vl-mark-wires-set (vl-expr-names lvalue) t alist))) (vl-mark-wires-used (vl-expr-names rhs) t alist))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-assignment (implies (and (force (vl-assign-p x)) (force (vl-wireinfo-alistp alist))) (b* ((new-alist (vl-mark-wires-for-assignment x alist))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)