		Search-engine friendly clone of the ACL2 documentation.

Vl-module

Make-vl-module

Basic constructor macro for vl-module structures.

Syntax

(make-vl-module [:name <name>] 
                [:params <params>] 
                [:imports <imports>] 
                [:ports <ports>] 
                [:portdecls <portdecls>] 
                [:vardecls <vardecls>] 
                [:paramdecls <paramdecls>] 
                [:fundecls <fundecls>] 
                [:taskdecls <taskdecls>] 
                [:assigns <assigns>] 
                [:aliases <aliases>] 
                [:modinsts <modinsts>] 
                [:gateinsts <gateinsts>] 
                [:alwayses <alwayses>] 
                [:initials <initials>] 
                [:genvars <genvars>] 
                [:generates <generates>] 
                [:atts <atts>] 
                [:minloc <minloc>] 
                [:maxloc <maxloc>] 
                [:origname <origname>] 
                [:warnings <warnings>] 
                [:comments <comments>] 
                [:loaditems <loaditems>] 
                [:esim <esim>])

This is the usual way to construct vl-module structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-module structure from scratch. See also change-vl-module, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-module

(defmacro make-vl-module (&rest args)
  (std::make-aggregate 'vl-module
                       args
                       '((:name)
                         (:params)
                         (:imports)
                         (:ports)
                         (:portdecls)
                         (:vardecls)
                         (:paramdecls)
                         (:fundecls)
                         (:taskdecls)
                         (:assigns)
                         (:aliases)
                         (:modinsts)
                         (:gateinsts)
                         (:alwayses)
                         (:initials)
                         (:genvars)
                         (:generates)
                         (:atts)
                         (:minloc)
                         (:maxloc)
                         (:origname)
                         (:warnings)
                         (:comments)
                         (:loaditems)
                         (:esim))
                       'make-vl-module
                       nil))

Function: vl-module

(defun vl-module (name params imports ports
                       portdecls vardecls paramdecls fundecls
                       taskdecls assigns aliases modinsts
                       gateinsts alwayses initials genvars
                       generates atts minloc maxloc origname
                       warnings comments loaditems esim)
 (declare (xargs :guard (and (stringp name)
                             (vl-importlist-p imports)
                             (vl-portlist-p ports)
                             (vl-portdecllist-p portdecls)
                             (vl-vardecllist-p vardecls)
                             (vl-paramdecllist-p paramdecls)
                             (vl-fundecllist-p fundecls)
                             (vl-taskdecllist-p taskdecls)
                             (vl-assignlist-p assigns)
                             (vl-aliaslist-p aliases)
                             (vl-modinstlist-p modinsts)
                             (vl-gateinstlist-p gateinsts)
                             (vl-alwayslist-p alwayses)
                             (vl-initiallist-p initials)
                             (vl-genvarlist-p genvars)
                             (vl-genelementlist-p generates)
                             (vl-atts-p atts)
                             (vl-location-p minloc)
                             (vl-location-p maxloc)
                             (stringp origname)
                             (vl-warninglist-p warnings)
                             (vl-commentmap-p comments)
                             (vl-genelementlist-p loaditems))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-module))
  (declare (ignorable __function__))
  (b* ((name (mbe :logic (str-fix name) :exec name))
       (imports (mbe :logic (vl-importlist-fix imports)
                     :exec imports))
       (ports (mbe :logic (vl-portlist-fix ports)
                   :exec ports))
       (portdecls (mbe :logic (vl-portdecllist-fix portdecls)
                       :exec portdecls))
       (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                      :exec vardecls))
       (paramdecls (mbe :logic (vl-paramdecllist-fix paramdecls)
                        :exec paramdecls))
       (fundecls (mbe :logic (vl-fundecllist-fix fundecls)
                      :exec fundecls))
       (taskdecls (mbe :logic (vl-taskdecllist-fix taskdecls)
                       :exec taskdecls))
       (assigns (mbe :logic (vl-assignlist-fix assigns)
                     :exec assigns))
       (aliases (mbe :logic (vl-aliaslist-fix aliases)
                     :exec aliases))
       (modinsts (mbe :logic (vl-modinstlist-fix modinsts)
                      :exec modinsts))
       (gateinsts (mbe :logic (vl-gateinstlist-fix gateinsts)
                       :exec gateinsts))
       (alwayses (mbe :logic (vl-alwayslist-fix alwayses)
                      :exec alwayses))
       (initials (mbe :logic (vl-initiallist-fix initials)
                      :exec initials))
       (genvars (mbe :logic (vl-genvarlist-fix genvars)
                     :exec genvars))
       (generates (mbe :logic (vl-genelementlist-fix generates)
                       :exec generates))
       (atts (mbe :logic (vl-atts-fix atts)
                  :exec atts))
       (minloc (mbe :logic (vl-location-fix minloc)
                    :exec minloc))
       (maxloc (mbe :logic (vl-location-fix maxloc)
                    :exec maxloc))
       (origname (mbe :logic (str-fix origname)
                      :exec origname))
       (warnings (mbe :logic (vl-warninglist-fix warnings)
                      :exec warnings))
       (comments (mbe :logic (vl-commentmap-fix comments)
                      :exec comments))
       (loaditems (mbe :logic (vl-genelementlist-fix loaditems)
                       :exec loaditems)))
   (cons
       :vl-module
       (cons (cons (cons (cons name (cons params imports))
                         (cons ports (cons portdecls vardecls)))
                   (cons (cons paramdecls (cons fundecls taskdecls))
                         (cons assigns (cons aliases modinsts))))
             (cons (cons (cons gateinsts (cons alwayses initials))
                         (cons genvars (cons generates atts)))
                   (cons (cons minloc (cons maxloc origname))
                         (cons (cons warnings comments)
                               (cons loaditems esim)))))))))