Move modules and other design elements that have fatal warnings
from the
(vl-design-filter-zombies good bad) → (mv good-- bad++)
Function:
(defun vl-design-filter-zombies (good bad) (declare (xargs :guard (and (vl-design-p good) (vl-design-p bad)))) (let ((__function__ 'vl-design-filter-zombies)) (declare (ignorable __function__)) (b* (((vl-design good)) ((vl-design bad)) ((mv bad-mods good-mods) (vl-filter-modules (vl-modulelist-zombies good.mods) good.mods)) ((mv bad-interfaces good-interfaces) (vl-filter-interfaces (vl-interfacelist-zombies good.interfaces) good.interfaces)) ((mv bad-udps good-udps) (vl-filter-udps (vl-udplist-zombies good.udps) good.udps)) ((mv bad-programs good-programs) (vl-filter-programs (vl-programlist-zombies good.programs) good.programs)) ((mv bad-packages good-packages) (vl-filter-packages (vl-packagelist-zombies good.packages) good.packages)) ((mv bad-configs good-configs) (vl-filter-configs (vl-configlist-zombies good.configs) good.configs)) ((mv bad-typedefs good-typedefs) (vl-filter-typedefs (vl-typedeflist-zombies good.typedefs) good.typedefs)) (good (change-vl-design good :mods good-mods :interfaces good-interfaces :udps good-udps :programs good-programs :packages good-packages :configs good-configs :typedefs good-typedefs)) (bad (change-vl-design bad :mods (append bad-mods bad.mods) :interfaces (append bad-interfaces bad.interfaces) :udps (append bad-udps bad.udps) :programs (append bad-programs bad.programs) :packages (append bad-packages bad.packages) :configs (append bad-configs bad.configs) :typedefs (append bad-typedefs bad.typedefs)))) (mv good bad))))
Theorem:
(defthm vl-design-p-of-vl-design-filter-zombies.good-- (b* (((mv ?good-- ?bad++) (vl-design-filter-zombies good bad))) (vl-design-p good--)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-p-of-vl-design-filter-zombies.bad++ (b* (((mv ?good-- ?bad++) (vl-design-filter-zombies good bad))) (vl-design-p bad++)) :rule-classes :rewrite)
Theorem:
(defthm vl-design-filter-zombies-of-vl-design-fix-good (equal (vl-design-filter-zombies (vl-design-fix good) bad) (vl-design-filter-zombies good bad)))
Theorem:
(defthm vl-design-filter-zombies-vl-design-equiv-congruence-on-good (implies (vl-design-equiv good good-equiv) (equal (vl-design-filter-zombies good bad) (vl-design-filter-zombies good-equiv bad))) :rule-classes :congruence)
Theorem:
(defthm vl-design-filter-zombies-of-vl-design-fix-bad (equal (vl-design-filter-zombies good (vl-design-fix bad)) (vl-design-filter-zombies good bad)))
Theorem:
(defthm vl-design-filter-zombies-vl-design-equiv-congruence-on-bad (implies (vl-design-equiv bad bad-equiv) (equal (vl-design-filter-zombies good bad) (vl-design-filter-zombies good bad-equiv))) :rule-classes :congruence)