Convert gates throughout a list of modules and add any new primitives into the module list.
(vl-modulelist-gate-elim x &key (primalist '*vl-gateinst-primitives-alist*)) → new-x
Function:
(defun vl-modulelist-gate-elim-fn (x primalist) (declare (xargs :guard (and (vl-modulelist-p x) (vl-primalist-p primalist)))) (let ((__function__ 'vl-modulelist-gate-elim)) (declare (ignorable __function__)) (b* (((mv new-x addmods) (vl-modulelist-gate-elim-aux x primalist)) (addmods (mergesort addmods)) (allmods (mergesort (append addmods new-x))) ((unless (uniquep (vl-modulelist->names allmods))) (raise 'vl-modulelist-gate-elim "Name collision for ~&0." (duplicated-members (vl-modulelist->names allmods))))) allmods)))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-gate-elim (implies (and (force (vl-modulelist-p x)) (force (vl-primalist-p primalist))) (b* ((new-x (vl-modulelist-gate-elim-fn x primalist))) (vl-modulelist-p new-x))) :rule-classes :rewrite)