(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* (((vl-design x) x) (ss (vl-scopestack-init x))) (change-vl-design x :mods (vl-modulelist-check-selfassigns x.mods ss)))))
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)
Theorem:
(defthm vl-design-check-selfassigns-of-vl-design-fix-x (equal (vl-design-check-selfassigns (vl-design-fix x)) (vl-design-check-selfassigns x)))
Theorem:
(defthm vl-design-check-selfassigns-vl-design-equiv-congruence-on-x (implies (vl-design-equiv x x-equiv) (equal (vl-design-check-selfassigns x) (vl-design-check-selfassigns x-equiv))) :rule-classes :congruence)