Drop arguments to blank ports from a module instance.
(vl-modinst-drop-blankports x ss warnings) → (mv warnings new-x)
Function:
(defun vl-modinst-drop-blankports (x ss warnings) (declare (xargs :guard (and (vl-modinst-p x) (vl-scopestack-p ss) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-modinst-drop-blankports)) (declare (ignorable __function__)) (b* ((x (vl-modinst-fix x)) ((vl-modinst x) x) (target-mod (vl-scopestack-find-definition x.modname ss)) ((unless (and target-mod (eq (tag target-mod) :vl-module))) (mv (fatal :type :vl-bad-instance :msg "~a0 refers to undefined module ~m1." :args (list x x.modname)) x)) ((unless (eq (vl-arguments-kind x.portargs) :vl-arguments-plain)) (mv (fatal :type :vl-programming-error :msg "~a0: expected all modules to be using plain ~ arguments, but found named arguments. Did you ~ forget to run the argresolve transform first?" :args (list x)) x)) (ports (vl-module->ports target-mod)) (plainargs (vl-arguments-plain->args x.portargs)) ((unless (same-lengthp plainargs ports)) (mv (fatal :type :vl-bad-instance :msg "~a0: bad arity. Expected ~x1 arguments but found ~ ~x2 arguments." :args (list x (len ports) (len plainargs))) x)) (new-plainargs (vl-plainarglist-drop-blankports plainargs ports)) (new-arguments (make-vl-arguments-plain :args new-plainargs)) (new-x (change-vl-modinst x :portargs new-arguments))) (mv (ok) new-x))))
Theorem:
(defthm vl-warninglist-p-of-vl-modinst-drop-blankports.warnings (b* (((mv ?warnings ?new-x) (vl-modinst-drop-blankports x ss warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinst-p-of-vl-modinst-drop-blankports.new-x (b* (((mv ?warnings ?new-x) (vl-modinst-drop-blankports x ss warnings))) (vl-modinst-p new-x)) :rule-classes :rewrite)