Main loop for creating the associated vl-vardecls.
(vl-build-netdecls-for-ports x &key nettype type atts) → netdecls
Function:
(defun vl-build-netdecls-for-ports-fn (x nettype type atts) (declare (xargs :guard (and (vl-parsed-port-identifier-list-p x) (vl-maybe-nettypename-p nettype) (vl-datatype-p type) (vl-atts-p atts)))) (let ((__function__ 'vl-build-netdecls-for-ports)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((vl-parsed-port-identifier x1) (car x)) (- (or (not (vl-datatype->udims type)) (raise "Base datatype already has unpacked dimensions?"))) (type1 (if (consp x1.udims) (vl-datatype-update-udims x1.udims type) type))) (cons (make-vl-vardecl :name (vl-idtoken->name x1.name) :loc (vl-token->loc x1.name) :nettype nettype :type type1 :atts atts :vectoredp nil :scalaredp nil :delay nil :cstrength nil) (vl-build-netdecls-for-ports (cdr x) :type type :nettype nettype :atts atts)))))
Theorem:
(defthm vl-vardecllist-p-of-vl-build-netdecls-for-ports (b* ((netdecls (vl-build-netdecls-for-ports-fn x nettype type atts))) (vl-vardecllist-p netdecls)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-build-netdecls-for-ports (b* ((netdecls (vl-build-netdecls-for-ports-fn x nettype type atts))) (true-listp netdecls)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-build-netdecls (b* ((netdecls (vl-build-netdecls-for-ports-fn x nettype type atts))) (equal (len netdecls) (len x))) :rule-classes :rewrite)
Theorem:
(defthm consp-of-vl-build-netdecls (b* ((netdecls (vl-build-netdecls-for-ports-fn x nettype type atts))) (equal (consp netdecls) (consp x))) :rule-classes :rewrite)
Theorem:
(defthm vl-build-netdecls-under-iff (b* ((netdecls (vl-build-netdecls-for-ports-fn x nettype type atts))) (iff netdecls (consp x))) :rule-classes :rewrite)