Fill in any blank arguments in a module instance's argument list.
(vl-modinst-plainarglist-blankargs args ports nf warnings inst) → (mv warnings new-args vardecls nf)
Function:
(defun vl-modinst-plainarglist-blankargs (args ports nf warnings inst) (declare (xargs :guard (and (vl-plainarglist-p args) (vl-portlist-p ports) (vl-namefactory-p nf) (vl-warninglist-p warnings) (vl-modinst-p inst)))) (declare (xargs :guard (same-lengthp args ports))) (let ((__function__ 'vl-modinst-plainarglist-blankargs)) (declare (ignorable __function__)) (b* ((nf (vl-namefactory-fix nf)) (inst (vl-modinst-fix inst)) ((when (atom args)) (mv (ok) nil nil nf)) ((mv warnings cdr-prime cdr-vardecls nf) (vl-modinst-plainarglist-blankargs (cdr args) (cdr ports) nf warnings inst)) (arg1 (vl-plainarg-fix (car args))) ((vl-plainarg arg1) arg1) ((when arg1.expr) (mv (ok) (cons arg1 cdr-prime) cdr-vardecls nf)) (port1 (vl-port-fix (car ports))) ((when (eq (tag port1) :vl-interfaceport)) (mv (fatal :type :vl-blankargs-fail :msg "~a0: blank argument is connected to interface port ~s1." :args (list inst (vl-interfaceport->name port1))) (cons arg1 cdr-prime) cdr-vardecls nf)) ((vl-regularport port1)) ((unless (and port1.expr (posp (vl-expr->finalwidth port1.expr)))) (mv (fatal :type :vl-blankargs-fail :msg "~a0: expected all ports to have expressions with ~ their widths, but a blank argument is connected to ~ port ~a1, which has expression ~a2 and width ~x3." :args (list inst port1 port1.expr (and port1.expr (vl-expr->finalwidth port1.expr)))) (cons arg1 cdr-prime) cdr-vardecls nf)) (port-width (vl-expr->finalwidth port1.expr)) ((mv newname nf) (vl-namefactory-indexed-name "blank" nf)) (range (vl-make-n-bit-range port-width)) (new-nettype (make-vl-coretype :name :vl-logic :pdims (list range) :signedp nil)) (new-vardecl (make-vl-vardecl :name newname :type new-nettype :nettype :vl-wire :loc (vl-modinst->loc inst))) (new-expr (vl-idexpr newname port-width :vl-unsigned)) (arg1-prime (change-vl-plainarg arg1 :expr new-expr))) (mv (ok) (cons arg1-prime cdr-prime) (cons new-vardecl cdr-vardecls) nf))))
Theorem:
(defthm vl-warninglist-p-of-vl-modinst-plainarglist-blankargs.warnings (b* (((mv ?warnings ?new-args ?vardecls ?nf) (vl-modinst-plainarglist-blankargs args ports nf warnings inst))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-plainarglist-p-of-vl-modinst-plainarglist-blankargs.new-args (b* (((mv ?warnings ?new-args ?vardecls ?nf) (vl-modinst-plainarglist-blankargs args ports nf warnings inst))) (vl-plainarglist-p new-args)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-modinst-plainarglist-blankargs.vardecls (b* (((mv ?warnings ?new-args ?vardecls ?nf) (vl-modinst-plainarglist-blankargs args ports nf warnings inst))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-modinst-plainarglist-blankargs.nf (b* (((mv ?warnings ?new-args ?vardecls ?nf) (vl-modinst-plainarglist-blankargs args ports nf warnings inst))) (vl-namefactory-p nf)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinst-plainarglist-blankargs-mvtypes-2 (true-listp (mv-nth 2 (vl-modinst-plainarglist-blankargs args ports nf warnings inst))) :rule-classes :type-prescription)
Theorem:
(defthm vl-modinst-plainarglist-blankargs-of-vl-plainarglist-fix-args (equal (vl-modinst-plainarglist-blankargs (vl-plainarglist-fix args) ports nf warnings inst) (vl-modinst-plainarglist-blankargs args ports nf warnings inst)))
Theorem:
(defthm vl-modinst-plainarglist-blankargs-vl-plainarglist-equiv-congruence-on-args (implies (vl-plainarglist-equiv args args-equiv) (equal (vl-modinst-plainarglist-blankargs args ports nf warnings inst) (vl-modinst-plainarglist-blankargs args-equiv ports nf warnings inst))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst-plainarglist-blankargs-of-vl-portlist-fix-ports (equal (vl-modinst-plainarglist-blankargs args (vl-portlist-fix ports) nf warnings inst) (vl-modinst-plainarglist-blankargs args ports nf warnings inst)))
Theorem:
(defthm vl-modinst-plainarglist-blankargs-vl-portlist-equiv-congruence-on-ports (implies (vl-portlist-equiv ports ports-equiv) (equal (vl-modinst-plainarglist-blankargs args ports nf warnings inst) (vl-modinst-plainarglist-blankargs args ports-equiv nf warnings inst))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst-plainarglist-blankargs-of-vl-namefactory-fix-nf (equal (vl-modinst-plainarglist-blankargs args ports (vl-namefactory-fix nf) warnings inst) (vl-modinst-plainarglist-blankargs args ports nf warnings inst)))
Theorem:
(defthm vl-modinst-plainarglist-blankargs-vl-namefactory-equiv-congruence-on-nf (implies (vl-namefactory-equiv nf nf-equiv) (equal (vl-modinst-plainarglist-blankargs args ports nf warnings inst) (vl-modinst-plainarglist-blankargs args ports nf-equiv warnings inst))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst-plainarglist-blankargs-of-vl-warninglist-fix-warnings (equal (vl-modinst-plainarglist-blankargs args ports nf (vl-warninglist-fix warnings) inst) (vl-modinst-plainarglist-blankargs args ports nf warnings inst)))
Theorem:
(defthm vl-modinst-plainarglist-blankargs-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-modinst-plainarglist-blankargs args ports nf warnings inst) (vl-modinst-plainarglist-blankargs args ports nf warnings-equiv inst))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst-plainarglist-blankargs-of-vl-modinst-fix-inst (equal (vl-modinst-plainarglist-blankargs args ports nf warnings (vl-modinst-fix inst)) (vl-modinst-plainarglist-blankargs args ports nf warnings inst)))
Theorem:
(defthm vl-modinst-plainarglist-blankargs-vl-modinst-equiv-congruence-on-inst (implies (vl-modinst-equiv inst inst-equiv) (equal (vl-modinst-plainarglist-blankargs args ports nf warnings inst) (vl-modinst-plainarglist-blankargs args ports nf warnings inst-equiv))) :rule-classes :congruence)