		Search-engine friendly clone of the ACL2 documentation.

Parse-netdecls

Vl-build-netdecls

Signature
(vl-build-netdecls loc x nettype type atts vectoredp scalaredp delay cstrength gstrength) → (mv nets assigns)
Arguments: loc — Guard (vl-location-p loc).; x — Guard (vl-vardeclassignlist-p x).; nettype — Guard (vl-nettypename-p nettype).; type — Guard (vl-datatype-p type).; atts — Guard (vl-atts-p atts).; vectoredp — Guard (booleanp vectoredp).; scalaredp — Guard (booleanp scalaredp).; delay — Guard (vl-maybe-gatedelay-p delay).; cstrength — Guard (vl-maybe-cstrength-p cstrength).; gstrength — Guard (vl-maybe-gatestrength-p gstrength).
Returns: nets — Type (vl-vardecllist-p nets).; assigns — Type (vl-assignlist-p assigns).

Definitions and Theorems

Function: vl-build-netdecls

(defun vl-build-netdecls (loc x nettype type atts vectoredp
                              scalaredp delay cstrength gstrength)
 (declare (xargs :guard (and (vl-location-p loc)
                             (vl-vardeclassignlist-p x)
                             (vl-nettypename-p nettype)
                             (vl-datatype-p type)
                             (vl-atts-p atts)
                             (booleanp vectoredp)
                             (booleanp scalaredp)
                             (vl-maybe-gatedelay-p delay)
                             (vl-maybe-cstrength-p cstrength)
                             (vl-maybe-gatestrength-p gstrength))))
 (declare (xargs :guard (vl-vardeclassignlist-newfree-p x)))
 (let ((__function__ 'vl-build-netdecls))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) (mv nil nil))
    ((vl-vardeclassign x1) (car x))
    (base-vardecl
        (make-vl-vardecl :name x1.id :delay delay :type
                         (if (atom (cdr x))
                             (vl-datatype-update-udims x1.dims type)
                           type)
                         :loc loc
                         :nettype nettype
                         :atts atts
                         :vectoredp vectoredp
                         :scalaredp scalaredp
                         :cstrength cstrength))
    ((when (and (atom (cdr x)) (not x1.rhs)))
     (mv (list base-vardecl) nil))
    (base-assign (make-vl-assign :lvalue |*sized-1'b0*|
                                 :expr |*sized-1'b0*|
                                 :loc loc
                                 :strength gstrength
                                 :delay delay
                                 :atts atts)))
   (vl-build-netdecls-aux x base-vardecl base-assign))))

Theorem: vl-vardecllist-p-of-vl-build-netdecls.nets

(defthm vl-vardecllist-p-of-vl-build-netdecls.nets
  (b* (((mv ?nets ?assigns)
        (vl-build-netdecls loc x nettype type atts vectoredp
                           scalaredp delay cstrength gstrength)))
    (vl-vardecllist-p nets))
  :rule-classes :rewrite)

Theorem: vl-assignlist-p-of-vl-build-netdecls.assigns

(defthm vl-assignlist-p-of-vl-build-netdecls.assigns
  (b* (((mv ?nets ?assigns)
        (vl-build-netdecls loc x nettype type atts vectoredp
                           scalaredp delay cstrength gstrength)))
    (vl-assignlist-p assigns))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-build-netdecls-nets

(defthm true-listp-of-vl-build-netdecls-nets
  (b* (((mv ?nets ?assigns)
        (vl-build-netdecls loc x nettype type atts vectoredp
                           scalaredp delay cstrength gstrength)))
    (true-listp nets))
  :rule-classes :type-prescription)

Theorem: true-listp-of-vl-build-netdecls-assigns

(defthm true-listp-of-vl-build-netdecls-assigns
  (b* (((mv ?nets ?assigns)
        (vl-build-netdecls loc x nettype type atts vectoredp
                           scalaredp delay cstrength gstrength)))
    (true-listp assigns))
  :rule-classes :type-prescription)