		Search-engine friendly clone of the ACL2 documentation.

Gate-elim

Vl-modulelist-gate-elim

Convert gates throughout a list of modules and add any new primitives into the module list.

Signature
(vl-modulelist-gate-elim x &key (primalist '*vl-gateinst-primitives-alist*)) → new-x
Arguments: x — Guard (vl-modulelist-p x).; primalist — Mapping from gate types to primitive modules.
Guard (vl-primalist-p primalist).
Returns: new-x — Type (vl-modulelist-p new-x), given the guard.

Definitions and Theorems

Function: vl-modulelist-gate-elim-fn

(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: vl-modulelist-p-of-vl-modulelist-gate-elim

(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)