Main function for adding implicit wires.
(vl-make-implicit-wires-aux x st implicit newitems warnings) → (mv new-warnings st implicit newitems)
Note that to keep this code simple, we don't try to defend against multiply declared names here.
We don't try to add any port declarations here, because we have to sort of get through the whole module to make sure there isn't an explicit declaration later on. We handle that in vl-make-implicit-wires-main.
Function:
(defun vl-make-implicit-wires-aux (x st implicit newitems warnings) (declare (xargs :guard (and (vl-genelementlist-p x) (vl-implicitst-p st) (vl-vardecllist-p implicit) (vl-genelementlist-p newitems) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-make-implicit-wires-aux)) (declare (ignorable __function__)) (b* ((x (vl-genelementlist-fix x)) (st (vl-implicitst-fix st)) (warnings (vl-warninglist-fix warnings)) (implicit (vl-vardecllist-fix implicit)) (newitems (vl-genelementlist-fix newitems)) ((when (atom x)) (mv warnings st implicit newitems)) ((unless (eq (vl-genelement-kind (car x)) :vl-genbase)) (vl-make-implicit-wires-aux (cdr x) st implicit (cons (car x) newitems) warnings)) (elem (vl-genelement-fix (car x))) (item (vl-genbase->item elem)) (tag (tag item)) ((when (or (eq tag :vl-interfaceport) (eq tag :vl-regularport))) (raise "We shouldn't see ports here.") (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings)) ((when (eq tag :vl-portdecl)) (b* ((declname (vl-portdecl->name item)) (st (change-vl-implicitst st :portdecls (hons-acons declname item (vl-implicitst->portdecls st)))) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (or (eq tag :vl-vardecl) (eq tag :vl-paramdecl))) (b* (((mv warnings st) (vl-blockitem-check-undeclared item st warnings)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((mv inst-p loc main-exprs other-exprs maybe-name) (case tag (:vl-modinst (b* ((loc (vl-modinst->loc item)) ((mv main other) (vl-modinst-exprs-for-implicit-wires item))) (mv t loc main other (vl-modinst->instname item)))) (:vl-gateinst (b* ((loc (vl-gateinst->loc item)) ((mv main other) (vl-gateinst-exprs-for-implicit-wires item))) (mv t loc main other (vl-gateinst->name item)))) (otherwise (mv nil nil nil nil nil)))) ((when inst-p) (b* ((other-names (vl-exprlist-varnames other-exprs)) (main-names (vl-exprlist-varnames main-exprs)) (warnings (vl-warn-about-undeclared-wires item other-names st warnings)) (imp-names (mergesort (vl-remove-declared-wires main-names st))) (imp-nets (vl-make-ordinary-implicit-wires loc imp-names)) (decls (vl-implicitst->decls st)) (decls (make-fal (pairlis$ imp-names nil) decls)) (decls (if maybe-name (hons-acons maybe-name t decls) decls)) (st (change-vl-implicitst st :decls decls)) (implicit (append imp-nets implicit)) (newitems (append (vl-modelementlist->genelements imp-nets) newitems)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (eq tag :vl-assign)) (b* (((vl-assign item) item) (lhs-names (vl-expr-varnames item.lvalue)) (imp-lhs (mergesort (vl-remove-declared-wires lhs-names st))) (warnings (if (not imp-lhs) warnings (warn :type :vl-tricky-implicit :msg "~a0: wire~s1 ~&2 ~s3 implicitly declared by the ~ left-hand side of this assignment. This is ~ perfectly valid according to the Verilog-2005 ~ standard, but some Verilog tools tools (like ~ Verilog-XL) do not support it, so for better ~ compatibility you may wish to add ~s4." :args (list item (if (vl-plural-p imp-lhs) "s" "") imp-lhs (if (vl-plural-p imp-lhs) "are" "is") (if (vl-plural-p imp-lhs) "explicit declarations for these wires" "an explicit declaration of this wire"))))) (decls (vl-implicitst->decls st)) (decls (make-fal (pairlis$ imp-lhs nil) decls)) (st (change-vl-implicitst st :decls decls)) (imp-nets (vl-make-ordinary-implicit-wires item.loc imp-lhs)) (implicit (append imp-nets implicit)) (newitems (append (vl-modelementlist->genelements imp-nets) newitems)) (newitems (cons (car x) newitems)) (other-names (vl-exprlist-varnames (cons item.expr (vl-maybe-gatedelay-allexprs item.delay)))) (warnings (vl-warn-about-undeclared-wires item other-names st warnings))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (eq tag :vl-alias)) (b* (((vl-alias item) item) (lhs-names (vl-expr-varnames item.lhs)) (rhs-names (vl-expr-varnames item.rhs)) (imp-names (mergesort (vl-remove-declared-wires (append lhs-names rhs-names) st))) (warnings (if (not imp-names) warnings (warn :type :vl-tricky-implicit :msg "~a0: wire~s1 ~&2 ~s3 implicitly declared by this ~ alias declaration." :args (list item (if (vl-plural-p imp-names) "s" "") imp-names (if (vl-plural-p imp-names) "are" "is"))))) (decls (vl-implicitst->decls st)) (decls (make-fal (pairlis$ imp-names nil) decls)) (st (change-vl-implicitst st :decls decls)) (imp-nets (vl-make-ordinary-implicit-wires item.loc imp-names)) (implicit (append imp-nets implicit)) (newitems (append (vl-modelementlist->genelements imp-nets) newitems)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (or (eq tag :vl-initial) (eq tag :vl-always))) (b* ((stmt (if (eq tag :vl-initial) (vl-initial->stmt item) (vl-always->stmt item))) (warnings (vl-stmt-check-undeclared item stmt st warnings)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (eq tag :vl-fundecl)) (b* ((warnings (vl-fundecl-check-undeclared item st warnings)) (decls (vl-implicitst->decls st)) (decls (hons-acons (vl-fundecl->name item) nil decls)) (st (change-vl-implicitst st :decls decls)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (eq tag :vl-taskdecl)) (b* ((warnings (vl-taskdecl-check-undeclared item st warnings)) (decls (vl-implicitst->decls st)) (decls (hons-acons (vl-taskdecl->name item) nil decls)) (st (change-vl-implicitst st :decls decls)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (eq tag :vl-import)) (b* (((vl-import item)) (package (vl-scopestack-find-package item.pkg (vl-implicitst->ss st))) (warnings (if package (ok) (fatal :type :vl-bad-import :msg "~a0: trying to import from undefined package ~s1." :args (list item item.pkg)))) (imports (vl-implicitst->imports st)) (imports (if (eq item.part :vl-import*) (hons-shrink-alist (and package (vl-package-scope-item-alist-top package)) imports) (hons-acons (the string item.part) t imports))) (st (change-vl-implicitst st :imports imports)) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (member tag '(:vl-modport :vl-typedef :vl-fwdtypedef))) (b* ((warnings (fatal :type :vl-unexpected-modelement :msg "~a0: unexpected kind of module item." :args (list item))) (newitems (cons (car x) newitems))) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) ((when (eq tag :vl-genvar)) (vl-make-implicit-wires-aux (cdr x) st implicit newitems warnings))) (impossible) (mv warnings st implicit newitems))))
Theorem:
(defthm vl-warninglist-p-of-vl-make-implicit-wires-aux.new-warnings (b* (((mv ?new-warnings ?st ?implicit ?newitems) (vl-make-implicit-wires-aux x st implicit newitems warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-implicitst-p-of-vl-make-implicit-wires-aux.st (b* (((mv ?new-warnings ?st ?implicit ?newitems) (vl-make-implicit-wires-aux x st implicit newitems warnings))) (vl-implicitst-p st)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-make-implicit-wires-aux.implicit (b* (((mv ?new-warnings ?st ?implicit ?newitems) (vl-make-implicit-wires-aux x st implicit newitems warnings))) (vl-vardecllist-p implicit)) :rule-classes :rewrite)
Theorem:
(defthm vl-genelementlist-p-of-vl-make-implicit-wires-aux.newitems (b* (((mv ?new-warnings ?st ?implicit ?newitems) (vl-make-implicit-wires-aux x st implicit newitems warnings))) (vl-genelementlist-p newitems)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-implicit-wires-aux-of-vl-genelementlist-fix-x (equal (vl-make-implicit-wires-aux (vl-genelementlist-fix x) st implicit newitems warnings) (vl-make-implicit-wires-aux x st implicit newitems warnings)))
Theorem:
(defthm vl-make-implicit-wires-aux-vl-genelementlist-equiv-congruence-on-x (implies (vl-genelementlist-equiv x x-equiv) (equal (vl-make-implicit-wires-aux x st implicit newitems warnings) (vl-make-implicit-wires-aux x-equiv st implicit newitems warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-implicit-wires-aux-of-vl-implicitst-fix-st (equal (vl-make-implicit-wires-aux x (vl-implicitst-fix st) implicit newitems warnings) (vl-make-implicit-wires-aux x st implicit newitems warnings)))
Theorem:
(defthm vl-make-implicit-wires-aux-vl-implicitst-equiv-congruence-on-st (implies (vl-implicitst-equiv st st-equiv) (equal (vl-make-implicit-wires-aux x st implicit newitems warnings) (vl-make-implicit-wires-aux x st-equiv implicit newitems warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-implicit-wires-aux-of-vl-vardecllist-fix-implicit (equal (vl-make-implicit-wires-aux x st (vl-vardecllist-fix implicit) newitems warnings) (vl-make-implicit-wires-aux x st implicit newitems warnings)))
Theorem:
(defthm vl-make-implicit-wires-aux-vl-vardecllist-equiv-congruence-on-implicit (implies (vl-vardecllist-equiv implicit implicit-equiv) (equal (vl-make-implicit-wires-aux x st implicit newitems warnings) (vl-make-implicit-wires-aux x st implicit-equiv newitems warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-implicit-wires-aux-of-vl-genelementlist-fix-newitems (equal (vl-make-implicit-wires-aux x st implicit (vl-genelementlist-fix newitems) warnings) (vl-make-implicit-wires-aux x st implicit newitems warnings)))
Theorem:
(defthm vl-make-implicit-wires-aux-vl-genelementlist-equiv-congruence-on-newitems (implies (vl-genelementlist-equiv newitems newitems-equiv) (equal (vl-make-implicit-wires-aux x st implicit newitems warnings) (vl-make-implicit-wires-aux x st implicit newitems-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-make-implicit-wires-aux-of-vl-warninglist-fix-warnings (equal (vl-make-implicit-wires-aux x st implicit newitems (vl-warninglist-fix warnings)) (vl-make-implicit-wires-aux x st implicit newitems warnings)))
Theorem:
(defthm vl-make-implicit-wires-aux-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-make-implicit-wires-aux x st implicit newitems warnings) (vl-make-implicit-wires-aux x st implicit newitems warnings-equiv))) :rule-classes :congruence)