		Search-engine friendly clone of the ACL2 documentation.

Creating-portdecls/vardecls

Vl-make-ports-and-maybe-nets

Top level routine for creating proper port and variable declarations.

Signature
(vl-make-ports-and-maybe-nets x &key dir nettype type complete-p atts) → val
Arguments: x — Guard (vl-parsed-port-identifier-list-p x).; dir — Guard (vl-direction-p dir).; nettype — Guard (vl-maybe-nettypename-p nettype).; type — Guard (vl-datatype-p type).; complete-p — Guard (booleanp complete-p).; atts — Guard (vl-atts-p atts).
Returns: val — Type (and (consp val) (vl-portdecllist-p (car val)) (vl-vardecllist-p (cdr val))) .

Definitions and Theorems

Function: vl-make-ports-and-maybe-nets-fn

(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: return-type-of-vl-make-ports-and-maybe-nets

(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: true-listp-of-vl-make-ports-and-maybe-nets-1

(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: true-listp-of-vl-make-ports-and-maybe-nets-2

(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: basics-of-vl-make-ports-and-maybe-nets

(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))))))