(vl-design-check-selfassigns x) → new-design
Function:
(defun vl-design-check-selfassigns (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-check-selfassigns)) (declare (ignorable __function__)) (b* ((x (vl-design-fix x)) ((vl-design x) x)) (change-vl-design x :mods (vl-modulelist-check-selfassigns x.mods)))))
Theorem:
(defthm vl-design-p-of-vl-design-check-selfassigns (b* ((new-design (vl-design-check-selfassigns x))) (vl-design-p new-design)) :rule-classes :rewrite)