		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-make-implicit-wires-aux

Main function for adding implicit wires.

Signature
(vl-make-implicit-wires-aux x st implicit newitems warnings) → (mv new-warnings st implicit newitems)
Arguments: x — Module elements to process, should be in the same order in which they were parsed.
Guard (vl-genelementlist-p x).; st — Guard (vl-implicitst-p st).; implicit — Accumulator for new variable declarations to add.
Guard (vl-vardecllist-p implicit).; newitems — Accumulator for rewriting X and inserting implicit variable declarations right where they occur.
Guard (vl-genelementlist-p newitems).; warnings — An ordinary warnings accumulator, which we may extend with fatal warnings (e.g., for undeclared identifiers) or non-fatal warnings (e.g., for compatibility warnings like Verilog-XL doesn't infer an implicit wire here.).
Guard (vl-warninglist-p warnings).
Returns: new-warnings — Type (vl-warninglist-p new-warnings).; st — Type (vl-implicitst-p st).; implicit — Type (vl-vardecllist-p implicit).; newitems — Type (vl-genelementlist-p 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.

Definitions and Theorems

Function: vl-make-implicit-wires-aux

(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: vl-warninglist-p-of-vl-make-implicit-wires-aux.new-warnings

(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: vl-implicitst-p-of-vl-make-implicit-wires-aux.st

(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: vl-vardecllist-p-of-vl-make-implicit-wires-aux.implicit

(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: vl-genelementlist-p-of-vl-make-implicit-wires-aux.newitems

(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: vl-make-implicit-wires-aux-of-vl-genelementlist-fix-x

(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: vl-make-implicit-wires-aux-vl-genelementlist-equiv-congruence-on-x

(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: vl-make-implicit-wires-aux-of-vl-implicitst-fix-st

(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: vl-make-implicit-wires-aux-vl-implicitst-equiv-congruence-on-st

(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: vl-make-implicit-wires-aux-of-vl-vardecllist-fix-implicit

(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: vl-make-implicit-wires-aux-vl-vardecllist-equiv-congruence-on-implicit

(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: vl-make-implicit-wires-aux-of-vl-genelementlist-fix-newitems

(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: vl-make-implicit-wires-aux-vl-genelementlist-equiv-congruence-on-newitems

(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: vl-make-implicit-wires-aux-of-vl-warninglist-fix-warnings

(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: vl-make-implicit-wires-aux-vl-warninglist-equiv-congruence-on-warnings

(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)