		Search-engine friendly clone of the ACL2 documentation.

Drop-blankports

Vl-module-drop-blankports

Drop any blank ports from a module, and simultaneously remove all arguments to blank ports from all module instances within the module.

Signature
(vl-module-drop-blankports x ss) → new-x
Arguments: x — module to rewrite.
Guard (vl-module-p x).; ss — Guard (vl-scopestack-p ss).
Returns: new-x — Type (vl-module-p new-x).

Definitions and Theorems

Function: vl-module-drop-blankports

(defun vl-module-drop-blankports (x ss)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-module-drop-blankports))
   (declare (ignorable __function__))
   (b* (((vl-module x) x)
        (ss (vl-scopestack-push (vl-module-fix x)
                                ss))
        (ports (vl-portlist-drop-blankports x.ports))
        ((mv warnings modinsts)
         (vl-modinstlist-drop-blankports x.modinsts ss x.warnings)))
     (change-vl-module x
                       :ports ports
                       :modinsts modinsts
                       :warnings warnings))))

Theorem: vl-module-p-of-vl-module-drop-blankports

(defthm vl-module-p-of-vl-module-drop-blankports
  (b* ((new-x (vl-module-drop-blankports x ss)))
    (vl-module-p new-x))
  :rule-classes :rewrite)