		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-make-implicit-wires-main

Augment a list of module elements with declarations for any implicit nets, and make sure that every identifier being used has a declaration.

Signature
(vl-make-implicit-wires-main loaditems ifports ss warnings) → (mv implicit newitems warnings)
Arguments: loaditems — All of the module elements from a single module, in the order they were parsed.
Guard (vl-genelementlist-p loaditems).; ifports — Interface ports for the module (we implicitly declare them first).
Guard (vl-interfaceportlist-p ifports).; ss — Guard (vl-scopestack-p ss).; warnings — An ordinary warnings accumulator, which may be extended with fatal and/or nonfatal warnings.
Guard (vl-warninglist-p warnings).
Returns: implicit — Declarations for implicit wires.
Type (vl-vardecllist-p implicit).; newitems — Extended loaditems (with implicit wires added).
Type (vl-genelementlist-p newitems).; warnings — Possibly extended warnings.
Type (vl-warninglist-p warnings).

We try to add declarations for any implicit wires. Unless there is a fatal warning, the resulting module element list will have declarations for all of its identifiers.

Definitions and Theorems

Function: vl-make-implicit-wires-main

(defun vl-make-implicit-wires-main (loaditems ifports ss warnings)
 (declare (xargs :guard (and (vl-genelementlist-p loaditems)
                             (vl-interfaceportlist-p ifports)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-make-implicit-wires-main))
  (declare (ignorable __function__))
  (b*
   ((ifports (vl-interfaceportlist-fix ifports))
    (st
     (make-vl-implicitst
      :decls (make-fast-alist (pairlis$ (vl-portlist->names ifports)
                                        (list-fix ifports)))
      :portdecls nil
      :imports nil
      :ss ss))
    (newitems nil)
    (normal-implicit nil)
    ((mv warnings st normal-implicit newitems)
     (vl-make-implicit-wires-aux
          loaditems
          st normal-implicit newitems warnings))
    (newitems (rev newitems))
    ((vl-implicitst st))
    (port-implicit
         (vl-make-port-implicit-wires st.portdecls st.decls))
    (- (fast-alist-free st.portdecls))
    (- (fast-alist-free st.decls))
    (- (fast-alist-free st.imports))
    (all-implicit
         (append-without-guard normal-implicit port-implicit)))
   (mv all-implicit newitems warnings))))

Theorem: vl-vardecllist-p-of-vl-make-implicit-wires-main.implicit

(defthm vl-vardecllist-p-of-vl-make-implicit-wires-main.implicit
 (b* (((mv ?implicit ?newitems ?warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))
   (vl-vardecllist-p implicit))
 :rule-classes :rewrite)

Theorem: vl-genelementlist-p-of-vl-make-implicit-wires-main.newitems

(defthm vl-genelementlist-p-of-vl-make-implicit-wires-main.newitems
 (b* (((mv ?implicit ?newitems ?warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))
   (vl-genelementlist-p newitems))
 :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-make-implicit-wires-main.warnings

(defthm vl-warninglist-p-of-vl-make-implicit-wires-main.warnings
 (b* (((mv ?implicit ?newitems ?warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: vl-make-implicit-wires-main-of-vl-genelementlist-fix-loaditems

(defthm
     vl-make-implicit-wires-main-of-vl-genelementlist-fix-loaditems
 (equal
      (vl-make-implicit-wires-main (vl-genelementlist-fix loaditems)
                                   ifports ss warnings)
      (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-genelementlist-equiv-congruence-on-loaditems

(defthm
 vl-make-implicit-wires-main-vl-genelementlist-equiv-congruence-on-loaditems
 (implies
  (vl-genelementlist-equiv loaditems loaditems-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems-equiv ifports ss warnings)))
 :rule-classes :congruence)

Theorem: vl-make-implicit-wires-main-of-vl-interfaceportlist-fix-ifports

(defthm
    vl-make-implicit-wires-main-of-vl-interfaceportlist-fix-ifports
 (equal
     (vl-make-implicit-wires-main loaditems
                                  (vl-interfaceportlist-fix ifports)
                                  ss warnings)
     (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-interfaceportlist-equiv-congruence-on-ifports

(defthm
 vl-make-implicit-wires-main-vl-interfaceportlist-equiv-congruence-on-ifports
 (implies
  (vl-interfaceportlist-equiv ifports ifports-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems ifports-equiv ss warnings)))
 :rule-classes :congruence)

Theorem: vl-make-implicit-wires-main-of-vl-scopestack-fix-ss

(defthm vl-make-implicit-wires-main-of-vl-scopestack-fix-ss
  (equal
       (vl-make-implicit-wires-main
            loaditems ifports (vl-scopestack-fix ss)
            warnings)
       (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-make-implicit-wires-main-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems ifports ss-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-make-implicit-wires-main-of-vl-warninglist-fix-warnings

(defthm vl-make-implicit-wires-main-of-vl-warninglist-fix-warnings
 (equal
      (vl-make-implicit-wires-main loaditems ifports
                                   ss (vl-warninglist-fix warnings))
      (vl-make-implicit-wires-main loaditems ifports ss warnings)))

Theorem: vl-make-implicit-wires-main-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-make-implicit-wires-main-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal (vl-make-implicit-wires-main loaditems ifports ss warnings)
         (vl-make-implicit-wires-main
              loaditems ifports ss warnings-equiv)))
 :rule-classes :congruence)