Top-level clean-selects transform.
(vl-design-clean-selects x) → *
Function:
(defun vl-design-clean-selects (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-clean-selects)) (declare (ignorable __function__)) (b* (((vl-design x) x) (ss (vl-scopestack-init x)) (mods (vl-modulelist-clean-selects x.mods ss))) (vl-scopestacks-free) (change-vl-design x :mods mods))))
Theorem:
(defthm vl-design-clean-selects-of-vl-design-fix-x (equal (vl-design-clean-selects (vl-design-fix x)) (vl-design-clean-selects x)))
Theorem:
(defthm vl-design-clean-selects-vl-design-equiv-congruence-on-x (implies (vl-design-equiv x x-equiv) (equal (vl-design-clean-selects x) (vl-design-clean-selects x-equiv))) :rule-classes :congruence)