		Search-engine friendly clone of the ACL2 documentation.

Vl-design

Make-vl-design

Basic constructor macro for vl-design structures.

Syntax

(make-vl-design [:version <version>] 
                [:mods <mods>] 
                [:udps <udps>] 
                [:interfaces <interfaces>] 
                [:programs <programs>] 
                [:classes <classes>] 
                [:packages <packages>] 
                [:configs <configs>] 
                [:vardecls <vardecls>] 
                [:taskdecls <taskdecls>] 
                [:fundecls <fundecls>] 
                [:paramdecls <paramdecls>] 
                [:imports <imports>] 
                [:dpiimports <dpiimports>] 
                [:dpiexports <dpiexports>] 
                [:fwdtypes <fwdtypes>] 
                [:typedefs <typedefs>] 
                [:binds <binds>] 
                [:properties <properties>] 
                [:sequences <sequences>] 
                [:warnings <warnings>] 
                [:comments <comments>] 
                [:plusargs <plusargs>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-design

(defmacro make-vl-design (&rest args)
  (std::make-aggregate 'vl-design
                       args
                       '((:version . *vl-current-syntax-version*)
                         (:mods)
                         (:udps)
                         (:interfaces)
                         (:programs)
                         (:classes)
                         (:packages)
                         (:configs)
                         (:vardecls)
                         (:taskdecls)
                         (:fundecls)
                         (:paramdecls)
                         (:imports)
                         (:dpiimports)
                         (:dpiexports)
                         (:fwdtypes)
                         (:typedefs)
                         (:binds)
                         (:properties)
                         (:sequences)
                         (:warnings)
                         (:comments)
                         (:plusargs))
                       'make-vl-design
                       nil))

Function: vl-design

(defun vl-design (version mods udps
                          interfaces programs classes packages
                          configs vardecls taskdecls fundecls
                          paramdecls imports dpiimports dpiexports
                          fwdtypes typedefs binds properties
                          sequences warnings comments plusargs)
 (declare (xargs :guard (and (vl-syntaxversion-p version)
                             (vl-modulelist-p mods)
                             (vl-udplist-p udps)
                             (vl-interfacelist-p interfaces)
                             (vl-programlist-p programs)
                             (vl-classlist-p classes)
                             (vl-packagelist-p packages)
                             (vl-configlist-p configs)
                             (vl-vardecllist-p vardecls)
                             (vl-taskdecllist-p taskdecls)
                             (vl-fundecllist-p fundecls)
                             (vl-paramdecllist-p paramdecls)
                             (vl-importlist-p imports)
                             (vl-dpiimportlist-p dpiimports)
                             (vl-dpiexportlist-p dpiexports)
                             (vl-fwdtypedeflist-p fwdtypes)
                             (vl-typedeflist-p typedefs)
                             (vl-bindlist-p binds)
                             (vl-propertylist-p properties)
                             (vl-sequencelist-p sequences)
                             (vl-warninglist-p warnings)
                             (vl-commentmap-p comments)
                             (string-listp plusargs))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-design))
  (declare (ignorable __function__))
  (b* ((version (mbe :logic (vl-syntaxversion-fix version)
                     :exec version))
       (mods (mbe :logic (vl-modulelist-fix mods)
                  :exec mods))
       (udps (mbe :logic (vl-udplist-fix udps)
                  :exec udps))
       (interfaces (mbe :logic (vl-interfacelist-fix interfaces)
                        :exec interfaces))
       (programs (mbe :logic (vl-programlist-fix programs)
                      :exec programs))
       (classes (mbe :logic (vl-classlist-fix classes)
                     :exec classes))
       (packages (mbe :logic (vl-packagelist-fix packages)
                      :exec packages))
       (configs (mbe :logic (vl-configlist-fix configs)
                     :exec configs))
       (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                      :exec vardecls))
       (taskdecls (mbe :logic (vl-taskdecllist-fix taskdecls)
                       :exec taskdecls))
       (fundecls (mbe :logic (vl-fundecllist-fix fundecls)
                      :exec fundecls))
       (paramdecls (mbe :logic (vl-paramdecllist-fix paramdecls)
                        :exec paramdecls))
       (imports (mbe :logic (vl-importlist-fix imports)
                     :exec imports))
       (dpiimports (mbe :logic (vl-dpiimportlist-fix dpiimports)
                        :exec dpiimports))
       (dpiexports (mbe :logic (vl-dpiexportlist-fix dpiexports)
                        :exec dpiexports))
       (fwdtypes (mbe :logic (vl-fwdtypedeflist-fix fwdtypes)
                      :exec fwdtypes))
       (typedefs (mbe :logic (vl-typedeflist-fix typedefs)
                      :exec typedefs))
       (binds (mbe :logic (vl-bindlist-fix binds)
                   :exec binds))
       (properties (mbe :logic (vl-propertylist-fix properties)
                        :exec properties))
       (sequences (mbe :logic (vl-sequencelist-fix sequences)
                       :exec sequences))
       (warnings (mbe :logic (vl-warninglist-fix warnings)
                      :exec warnings))
       (comments (mbe :logic (vl-commentmap-fix comments)
                      :exec comments))
       (plusargs (mbe :logic (string-list-fix plusargs)
                      :exec plusargs)))
   (cons
    :vl-design
    (std::prod-cons
     (std::prod-cons
         (std::prod-cons
              (std::prod-cons version mods)
              (std::prod-cons udps
                              (std::prod-cons interfaces programs)))
         (std::prod-cons
              (std::prod-cons classes
                              (std::prod-cons packages configs))
              (std::prod-cons vardecls
                              (std::prod-cons taskdecls fundecls))))
     (std::prod-cons
      (std::prod-cons
           (std::prod-cons paramdecls
                           (std::prod-cons imports dpiimports))
           (std::prod-cons dpiexports
                           (std::prod-cons fwdtypes typedefs)))
      (std::prod-cons
          (std::prod-cons binds
                          (std::prod-cons properties sequences))
          (std::prod-cons warnings
                          (std::prod-cons comments plusargs)))))))))