Top level routine for creating proper port and variable declarations.
(vl-make-ports-and-maybe-nets x &key dir nettype type complete-p atts) → val
Function:
(defun vl-make-ports-and-maybe-nets-fn (x dir nettype type complete-p atts) (declare (xargs :guard (and (vl-parsed-port-identifier-list-p x) (vl-direction-p dir) (vl-maybe-nettypename-p nettype) (vl-datatype-p type) (booleanp complete-p) (vl-atts-p atts)))) (let ((__function__ 'vl-make-ports-and-maybe-nets)) (declare (ignorable __function__)) (b* ((atts (if complete-p atts (hons '("VL_INCOMPLETE_DECLARATION") atts))) (portdecls (vl-build-portdecls x :dir dir :nettype nettype :type type :atts atts)) (netdecls (if (not complete-p) nil (vl-build-netdecls-for-ports x :type type :nettype nettype :atts (hons '("VL_PORT_IMPLICIT") atts))))) (cons portdecls netdecls))))
Theorem:
(defthm return-type-of-vl-make-ports-and-maybe-nets (b* ((val (vl-make-ports-and-maybe-nets-fn x dir nettype type complete-p atts))) (and (consp val) (vl-portdecllist-p (car val)) (vl-vardecllist-p (cdr val)))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-make-ports-and-maybe-nets-1 (true-listp (car (vl-make-ports-and-maybe-nets x :dir dir :type type :complete-p complete-p :nettype nettype :atts atts))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-vl-make-ports-and-maybe-nets-2 (true-listp (cdr (vl-make-ports-and-maybe-nets x :dir dir :type type :complete-p complete-p :nettype nettype :atts atts))) :rule-classes :type-prescription)
Theorem:
(defthm basics-of-vl-make-ports-and-maybe-nets (b* (((cons portdecls netdecls) (vl-make-ports-and-maybe-nets x :dir dir :type type :complete-p complete-p :nettype nettype :atts atts))) (and (equal (len portdecls) (len x)) (equal (consp portdecls) (consp x)) (iff portdecls (consp x)) (equal (len netdecls) (if complete-p (len x) 0)) (equal (consp netdecls) (and complete-p (consp x))) (iff netdecls (and complete-p (consp x))))))