		Search-engine friendly clone of the ACL2 documentation.

Make-implicit-wires

Vl-make-port-implicit-wires

(vl-make-port-implicit-wires portdecls decls) generates variable declarations for ports that don't have corresponding variable declarations.

Signature
(vl-make-port-implicit-wires portdecls decls) → implicit
Arguments: portdecls — Alist binding names to port declarations.
Guard (vl-portdecl-alist-p portdecls).; decls — Alist binding names declared in the module to nil.
Returns: implicit — A list of new variable declarations, one for each port declaration without a corresponding ordinary declaration.
Type (vl-vardecllist-p implicit).

BOZO what about scalaredp, vectoredp, cstrength, delay? I think we don't care, but it might be good to look into this again.

Definitions and Theorems

Function: vl-make-port-implicit-wires

(defun vl-make-port-implicit-wires (portdecls decls)
 (declare (xargs :guard (vl-portdecl-alist-p portdecls)))
 (let ((__function__ 'vl-make-port-implicit-wires))
   (declare (ignorable __function__))
   (b*
    (((when (atom portdecls)) nil)
     ((when (atom (car portdecls)))
      (vl-make-port-implicit-wires (cdr portdecls)
                                   decls))
     ((vl-portdecl portdecl)
      (cdar portdecls))
     ((when (hons-get portdecl.name decls))
      (vl-make-port-implicit-wires (cdr portdecls)
                                   decls))
     (new-decl
          (make-vl-vardecl :name portdecl.name
                           :type portdecl.type
                           :nettype :vl-wire
                           :atts (cons (cons "VL_PORT_IMPLICIT" nil)
                                       portdecl.atts)
                           :loc portdecl.loc)))
    (cons new-decl
          (vl-make-port-implicit-wires (cdr portdecls)
                                       decls)))))

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

(defthm vl-vardecllist-p-of-vl-make-port-implicit-wires
  (b* ((implicit (vl-make-port-implicit-wires portdecls decls)))
    (vl-vardecllist-p implicit))
  :rule-classes :rewrite)