(vl-make-port-implicit-wires portdecls decls) generates variable declarations for ports that don't have corresponding variable declarations.
(vl-make-port-implicit-wires portdecls decls) → implicit
BOZO what about scalaredp, vectoredp, cstrength, delay? I think we don't care, but it might be good to look into this again.
Function:
(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:
(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)