		Search-engine friendly clone of the ACL2 documentation.

Gate-elim

Vl-module-gate-elim

Convert gates throughout a module.

Signature
(vl-module-gate-elim x primalist) → (mv new-x addmods)
Arguments: x — Guard (vl-module-p x).; primalist — Mapping from gate types to primitive modules.
Guard (vl-primalist-p primalist).
Returns: new-x — Type (vl-module-p new-x), given the guard.; addmods — Type (vl-modulelist-p addmods), given the guard.

Definitions and Theorems

Function: vl-module-gate-elim

(defun vl-module-gate-elim (x primalist)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-primalist-p primalist))))
 (let ((__function__ 'vl-module-gate-elim))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    ((when (vl-module->hands-offp x))
     (mv x nil))
    ((unless x.gateinsts) (mv x nil))
    ((mv warnings
         new-gateinsts new-modinsts addmods)
     (vl-gateinstlist-gate-elim x.gateinsts primalist x.warnings))
    (new-x
     (change-vl-module x
                       :warnings warnings
                       :gateinsts new-gateinsts
                       :modinsts (append new-modinsts x.modinsts))))
   (mv new-x addmods))))

Theorem: vl-module-p-of-vl-module-gate-elim.new-x

(defthm vl-module-p-of-vl-module-gate-elim.new-x
  (implies (and (force (vl-module-p x))
                (force (vl-primalist-p primalist)))
           (b* (((mv ?new-x ?addmods)
                 (vl-module-gate-elim x primalist)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-module-gate-elim.addmods

(defthm vl-modulelist-p-of-vl-module-gate-elim.addmods
  (implies (and (force (vl-module-p x))
                (force (vl-primalist-p primalist)))
           (b* (((mv ?new-x ?addmods)
                 (vl-module-gate-elim x primalist)))
             (vl-modulelist-p addmods)))
  :rule-classes :rewrite)

Theorem: vl-module-gate-elim-mvtypes-1

(defthm vl-module-gate-elim-mvtypes-1
  (true-listp (mv-nth 1 (vl-module-gate-elim x primalist)))
  :rule-classes :type-prescription)