		Search-engine friendly clone of the ACL2 documentation.

Creating-portdecls/vardecls

Vl-build-netdecls-for-ports

Main loop for creating the associated vl-vardecls.

Signature
(vl-build-netdecls-for-ports x &key nettype type atts) → netdecls
Arguments: x — Guard (vl-parsed-port-identifier-list-p x).; nettype — Guard (vl-maybe-nettypename-p nettype).; type — Guard (vl-datatype-p type).; atts — Guard (vl-atts-p atts).
Returns: netdecls — Type (vl-vardecllist-p netdecls).

Definitions and Theorems

Function: vl-build-netdecls-for-ports-fn

(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?")))
    (basedecl (make-vl-vardecl :name (vl-idtoken->name x1.name)
                               :loc (vl-token->loc x1.name)
                               :nettype nettype
                               :type type
                               :atts atts
                               :varp nil
                               :constp nil
                               :lifetime nil
                               :vectoredp nil
                               :scalaredp nil
                               :delay nil
                               :cstrength nil))
    ((when (consp x1.udims))
     (vl-build-subsequent-netdecls-for-ports x basedecl)))
   (cons basedecl
         (vl-build-subsequent-netdecls-for-ports (cdr x)
                                                 basedecl)))))

Theorem: vl-vardecllist-p-of-vl-build-netdecls-for-ports

(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: true-listp-of-vl-build-netdecls-for-ports

(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: len-of-vl-build-netdecls

(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: consp-of-vl-build-netdecls

(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: vl-build-netdecls-under-iff

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

Subtopics

Vl-build-subsequent-netdecls-for-ports: See vl-build-subsequent-portdecls. This is identical but for the vardecls instead of the portdecls.