		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-make-port-implicit-wires

Generate variable declarations for ports that don't have corresponding variable declarations.

Signature
(vl-make-port-implicit-wires items decls newitems) → newitems
Arguments: items — Items to process in reverse parse order, with implicit wire declarations already added in.
Guard (vl-genelementlist-p items).; decls — Alist binding all the non-port names that are (ever) declared in the module to anything. This lets us tell, when we get to a port declaration, whether we need to add a corresponding net declaration for it.; newitems — Accumulator for our new items (reverse of items order, i.e., back into parse order.).
Guard (vl-genelementlist-p newitems).
Returns: newitems — Parse order, with port-implicit decls added.
Type (vl-genelementlist-p newitems).

Definitions and Theorems

Function: vl-make-port-implicit-wires

(defun vl-make-port-implicit-wires (items decls newitems)
 (declare (xargs :guard (and (vl-genelementlist-p items)
                             (vl-genelementlist-p newitems))))
 (let ((__function__ 'vl-make-port-implicit-wires))
  (declare (ignorable __function__))
  (b*
   (((when (atom items))
     (vl-genelementlist-fix newitems))
    (item (vl-genelement-fix (car items)))
    ((unless (and (vl-genelement-case item :vl-genbase)
                  (eq (tag (vl-genbase->item item))
                      :vl-portdecl)))
     (vl-make-port-implicit-wires (cdr items)
                                  decls (cons item newitems)))
    ((vl-portdecl portdecl)
     (vl-genbase->item item))
    ((when (hons-get portdecl.name decls))
     (vl-make-port-implicit-wires (cdr items)
                                  decls (cons item newitems)))
    (new-decl
       (make-vl-genbase
            :item (make-vl-vardecl :name portdecl.name
                                   :type portdecl.type
                                   :nettype portdecl.nettype
                                   :atts (cons '("VL_PORT_IMPLICIT")
                                               portdecl.atts)
                                   :loc portdecl.loc))))
   (vl-make-port-implicit-wires
        (cdr items)
        decls (list* item new-decl newitems)))))

Theorem: vl-genelementlist-p-of-vl-make-port-implicit-wires

(defthm vl-genelementlist-p-of-vl-make-port-implicit-wires
 (b* ((newitems (vl-make-port-implicit-wires items decls newitems)))
   (vl-genelementlist-p newitems))
 :rule-classes :rewrite)

Theorem: vl-make-port-implicit-wires-of-vl-genelementlist-fix-items

(defthm vl-make-port-implicit-wires-of-vl-genelementlist-fix-items
  (equal (vl-make-port-implicit-wires (vl-genelementlist-fix items)
                                      decls newitems)
         (vl-make-port-implicit-wires items decls newitems)))

Theorem: vl-make-port-implicit-wires-vl-genelementlist-equiv-congruence-on-items

(defthm
 vl-make-port-implicit-wires-vl-genelementlist-equiv-congruence-on-items
 (implies
   (vl-genelementlist-equiv items items-equiv)
   (equal (vl-make-port-implicit-wires items decls newitems)
          (vl-make-port-implicit-wires items-equiv decls newitems)))
 :rule-classes :congruence)

Theorem: vl-make-port-implicit-wires-of-vl-genelementlist-fix-newitems

(defthm
      vl-make-port-implicit-wires-of-vl-genelementlist-fix-newitems
  (equal (vl-make-port-implicit-wires
              items
              decls (vl-genelementlist-fix newitems))
         (vl-make-port-implicit-wires items decls newitems)))

Theorem: vl-make-port-implicit-wires-vl-genelementlist-equiv-congruence-on-newitems

(defthm
 vl-make-port-implicit-wires-vl-genelementlist-equiv-congruence-on-newitems
 (implies
   (vl-genelementlist-equiv newitems newitems-equiv)
   (equal (vl-make-port-implicit-wires items decls newitems)
          (vl-make-port-implicit-wires items decls newitems-equiv)))
 :rule-classes :congruence)