• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
          • Scopestack
          • Hid-tools
          • Filtering-by-name
          • Vl-interface-mocktype
          • Stripping-functions
          • Genblob
            • Vl-genblob
              • Vl-genblob-p
              • Vl-genblob-count
              • Vl-genblob-fix
              • Make-vl-genblob
                • Change-vl-genblob
                • Vl-genblob-equiv
                • Vl-genblob->defaultdisables
                • Vl-genblob->fwdtypedefs
                • Vl-genblob->dpiimports
                • Vl-genblob->dpiexports
                • Vl-genblob->covergroups
                • Vl-genblob->cassertions
                • Vl-genblob->vardecls
                • Vl-genblob->typedefs
                • Vl-genblob->taskdecls
                • Vl-genblob->sequences
                • Vl-genblob->scopetype
                • Vl-genblob->properties
                • Vl-genblob->portdecls
                • Vl-genblob->paramdecls
                • Vl-genblob->modports
                • Vl-genblob->modinsts
                • Vl-genblob->letdecls
                • Vl-genblob->initials
                • Vl-genblob->genvars
                • Vl-genblob->generates
                • Vl-genblob->gclkdecls
                • Vl-genblob->gateinsts
                • Vl-genblob->fundecls
                • Vl-genblob->elabtasks
                • Vl-genblob->clkdecls
                • Vl-genblob->assertions
                • Vl-genblob->alwayses
                • Vl-genblob->ports
                • Vl-genblob->imports
                • Vl-genblob->ifports
                • Vl-genblob->id
                • Vl-genblob->finals
                • Vl-genblob->classes
                • Vl-genblob->binds
                • Vl-genblob->assigns
                • Vl-genblob->aliases
              • Vl-sort-genelements
              • Vl-genblob->interface
              • Vl-genblob->module
              • Vl-genblob->elems
              • Vl-interface->genblob
              • Vl-genblob->package
              • Vl-module->genblob
              • Vl-genblob->class
              • Vl-package->genblob
              • Vl-class->genblob
              • Vl-genelementlist->defaultdisables
              • Vl-genelementlist->properties
              • Vl-genelementlist->paramdecls
              • Vl-genelementlist->fwdtypedefs
              • Vl-genelementlist->dpiimports
              • Vl-genelementlist->dpiexports
              • Vl-genelementlist->covergroups
              • Vl-genelementlist->cassertions
              • Vl-genelementlist->assertions
              • Vl-genelementlist->vardecls
              • Vl-genelementlist->typedefs
              • Vl-genelementlist->taskdecls
              • Vl-genelementlist->sequences
              • Vl-genelementlist->portdecls
              • Vl-genelementlist->modports
              • Vl-genelementlist->modinsts
              • Vl-genelementlist->letdecls
              • Vl-genelementlist->initials
              • Vl-genelementlist->imports
              • Vl-genelementlist->genvars
              • Vl-genelementlist->generates
              • Vl-genelementlist->gclkdecls
              • Vl-genelementlist->gateinsts
              • Vl-genelementlist->fundecls
              • Vl-genelementlist->elabtasks
              • Vl-genelementlist->clkdecls
              • Vl-genelementlist->assigns
              • Vl-genelementlist->alwayses
              • Vl-genelementlist->finals
              • Vl-genelementlist->classes
              • Vl-genelementlist->binds
              • Vl-genelementlist->aliases
              • Vl-genblock->genblob
              • Vl-scopetype-p
            • Expr-tools
            • Extract-vl-types
            • Hierarchy
            • Range-tools
            • Finding-by-name
            • Stmt-tools
            • Modnamespace
            • Flat-warnings
            • Reordering-by-name
            • Datatype-tools
            • Syscalls
            • Allexprs
            • Lvalues
            • Port-tools
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-genblob

    Make-vl-genblob

    Basic constructor macro for vl-genblob structures.

    Syntax
    (make-vl-genblob [:portdecls <portdecls>] 
                     [:assigns <assigns>] 
                     [:aliases <aliases>] 
                     [:vardecls <vardecls>] 
                     [:paramdecls <paramdecls>] 
                     [:fundecls <fundecls>] 
                     [:taskdecls <taskdecls>] 
                     [:modinsts <modinsts>] 
                     [:gateinsts <gateinsts>] 
                     [:alwayses <alwayses>] 
                     [:initials <initials>] 
                     [:finals <finals>] 
                     [:typedefs <typedefs>] 
                     [:imports <imports>] 
                     [:fwdtypedefs <fwdtypedefs>] 
                     [:modports <modports>] 
                     [:genvars <genvars>] 
                     [:assertions <assertions>] 
                     [:cassertions <cassertions>] 
                     [:properties <properties>] 
                     [:sequences <sequences>] 
                     [:clkdecls <clkdecls>] 
                     [:gclkdecls <gclkdecls>] 
                     [:defaultdisables <defaultdisables>] 
                     [:dpiimports <dpiimports>] 
                     [:dpiexports <dpiexports>] 
                     [:binds <binds>] 
                     [:classes <classes>] 
                     [:covergroups <covergroups>] 
                     [:elabtasks <elabtasks>] 
                     [:letdecls <letdecls>] 
                     [:generates <generates>] 
                     [:ports <ports>] 
                     [:scopetype <scopetype>] 
                     [:id <id>]) 
    

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

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

    Definition

    This is an ordinary make- macro introduced by defprod.

    Macro: make-vl-genblob

    (defmacro make-vl-genblob (&rest args)
      (std::make-aggregate 'vl-genblob
                           args
                           '((:portdecls)
                             (:assigns)
                             (:aliases)
                             (:vardecls)
                             (:paramdecls)
                             (:fundecls)
                             (:taskdecls)
                             (:modinsts)
                             (:gateinsts)
                             (:alwayses)
                             (:initials)
                             (:finals)
                             (:typedefs)
                             (:imports)
                             (:fwdtypedefs)
                             (:modports)
                             (:genvars)
                             (:assertions)
                             (:cassertions)
                             (:properties)
                             (:sequences)
                             (:clkdecls)
                             (:gclkdecls)
                             (:defaultdisables)
                             (:dpiimports)
                             (:dpiexports)
                             (:binds)
                             (:classes)
                             (:covergroups)
                             (:elabtasks)
                             (:letdecls)
                             (:generates)
                             (:ports)
                             (:scopetype . :vl-anonymous-scope)
                             (:id))
                           'make-vl-genblob
                           nil))

    Function: vl-genblob

    (defun vl-genblob (portdecls assigns aliases
                                 vardecls paramdecls fundecls taskdecls
                                 modinsts gateinsts alwayses initials
                                 finals typedefs imports fwdtypedefs
                                 modports genvars assertions cassertions
                                 properties sequences clkdecls gclkdecls
                                 defaultdisables dpiimports dpiexports
                                 binds classes covergroups elabtasks
                                 letdecls generates ports scopetype id)
     (declare
          (xargs :guard (and (vl-portdecllist-p portdecls)
                             (vl-assignlist-p assigns)
                             (vl-aliaslist-p aliases)
                             (vl-vardecllist-p vardecls)
                             (vl-paramdecllist-p paramdecls)
                             (vl-fundecllist-p fundecls)
                             (vl-taskdecllist-p taskdecls)
                             (vl-modinstlist-p modinsts)
                             (vl-gateinstlist-p gateinsts)
                             (vl-alwayslist-p alwayses)
                             (vl-initiallist-p initials)
                             (vl-finallist-p finals)
                             (vl-typedeflist-p typedefs)
                             (vl-importlist-p imports)
                             (vl-fwdtypedeflist-p fwdtypedefs)
                             (vl-modportlist-p modports)
                             (vl-genvarlist-p genvars)
                             (vl-assertionlist-p assertions)
                             (vl-cassertionlist-p cassertions)
                             (vl-propertylist-p properties)
                             (vl-sequencelist-p sequences)
                             (vl-clkdecllist-p clkdecls)
                             (vl-gclkdecllist-p gclkdecls)
                             (vl-defaultdisablelist-p defaultdisables)
                             (vl-dpiimportlist-p dpiimports)
                             (vl-dpiexportlist-p dpiexports)
                             (vl-bindlist-p binds)
                             (vl-classlist-p classes)
                             (vl-covergrouplist-p covergroups)
                             (vl-elabtasklist-p elabtasks)
                             (vl-letdecllist-p letdecls)
                             (vl-genelementlist-p generates)
                             (vl-portlist-p ports)
                             (vl-scopetype-p scopetype)
                             (vl-maybe-scopeid-p id))))
     (declare (xargs :guard t))
     (let ((__function__ 'vl-genblob))
      (declare (ignorable __function__))
      (b* ((portdecls (mbe :logic (vl-portdecllist-fix portdecls)
                           :exec portdecls))
           (assigns (mbe :logic (vl-assignlist-fix assigns)
                         :exec assigns))
           (aliases (mbe :logic (vl-aliaslist-fix aliases)
                         :exec aliases))
           (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))
           (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))
           (finals (mbe :logic (vl-finallist-fix finals)
                        :exec finals))
           (typedefs (mbe :logic (vl-typedeflist-fix typedefs)
                          :exec typedefs))
           (imports (mbe :logic (vl-importlist-fix imports)
                         :exec imports))
           (fwdtypedefs (mbe :logic (vl-fwdtypedeflist-fix fwdtypedefs)
                             :exec fwdtypedefs))
           (modports (mbe :logic (vl-modportlist-fix modports)
                          :exec modports))
           (genvars (mbe :logic (vl-genvarlist-fix genvars)
                         :exec genvars))
           (assertions (mbe :logic (vl-assertionlist-fix assertions)
                            :exec assertions))
           (cassertions (mbe :logic (vl-cassertionlist-fix cassertions)
                             :exec cassertions))
           (properties (mbe :logic (vl-propertylist-fix properties)
                            :exec properties))
           (sequences (mbe :logic (vl-sequencelist-fix sequences)
                           :exec sequences))
           (clkdecls (mbe :logic (vl-clkdecllist-fix clkdecls)
                          :exec clkdecls))
           (gclkdecls (mbe :logic (vl-gclkdecllist-fix gclkdecls)
                           :exec gclkdecls))
           (defaultdisables
                (mbe :logic (vl-defaultdisablelist-fix defaultdisables)
                     :exec defaultdisables))
           (dpiimports (mbe :logic (vl-dpiimportlist-fix dpiimports)
                            :exec dpiimports))
           (dpiexports (mbe :logic (vl-dpiexportlist-fix dpiexports)
                            :exec dpiexports))
           (binds (mbe :logic (vl-bindlist-fix binds)
                       :exec binds))
           (classes (mbe :logic (vl-classlist-fix classes)
                         :exec classes))
           (covergroups (mbe :logic (vl-covergrouplist-fix covergroups)
                             :exec covergroups))
           (elabtasks (mbe :logic (vl-elabtasklist-fix elabtasks)
                           :exec elabtasks))
           (letdecls (mbe :logic (vl-letdecllist-fix letdecls)
                          :exec letdecls))
           (generates (mbe :logic (vl-genelementlist-fix generates)
                           :exec generates))
           (ports (mbe :logic (vl-portlist-fix ports)
                       :exec ports))
           (scopetype (mbe :logic (vl-scopetype-fix scopetype)
                           :exec scopetype))
           (id (mbe :logic (vl-maybe-scopeid-fix id)
                    :exec id)))
       (cons
        :vl-genblob
        (std::prod-cons
         (std::prod-cons
          (std::prod-cons
               (std::prod-cons (std::prod-cons portdecls assigns)
                               (std::prod-cons aliases vardecls))
               (std::prod-cons (std::prod-cons paramdecls fundecls)
                               (std::prod-cons taskdecls modinsts)))
          (std::prod-cons
              (std::prod-cons (std::prod-cons gateinsts alwayses)
                              (std::prod-cons initials finals))
              (std::prod-cons
                   (std::prod-cons typedefs imports)
                   (std::prod-cons fwdtypedefs
                                   (std::prod-cons modports genvars)))))
         (std::prod-cons
          (std::prod-cons
           (std::prod-cons (std::prod-cons assertions cassertions)
                           (std::prod-cons properties sequences))
           (std::prod-cons
               (std::prod-cons clkdecls gclkdecls)
               (std::prod-cons defaultdisables
                               (std::prod-cons dpiimports dpiexports))))
          (std::prod-cons
             (std::prod-cons (std::prod-cons binds classes)
                             (std::prod-cons covergroups elabtasks))
             (std::prod-cons
                  (std::prod-cons letdecls generates)
                  (std::prod-cons ports
                                  (std::prod-cons scopetype id))))))))))