• 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
          • Vl-module
          • Vl-vardecl
          • Vl-fundecl
          • Vl-interface
            • Vl-interface-p
            • Vl-interface-fix
            • Make-vl-interface
              • Vl-modport-port
              • Vl-modport
              • Change-vl-interface
              • Vl-interface-equiv
              • Vl-interface->defaultdisables
              • Vl-interface->parse-temps
              • Vl-interface->warnings
              • Vl-interface->taskdecls
              • Vl-interface->sequences
              • Vl-interface->properties
              • Vl-interface->portdecls
              • Vl-interface->paramdecls
              • Vl-interface->origname
              • Vl-interface->initials
              • Vl-interface->generates
              • Vl-interface->gclkdecls
              • Vl-interface->fundecls
              • Vl-interface->elabtasks
              • Vl-interface->dpiimports
              • Vl-interface->dpiexports
              • Vl-interface->comments
              • Vl-interface->cassertions
              • Vl-interface->assertions
              • Vl-interface->alwayses
              • Vl-interface->vardecls
              • Vl-interface->typedefs
              • Vl-interface->name
              • Vl-interface->modports
              • Vl-interface->modinsts
              • Vl-interface->minloc
              • Vl-interface->maxloc
              • Vl-interface->imports
              • Vl-interface->genvars
              • Vl-interface->finals
              • Vl-interface->clkdecls
              • Vl-interface->classes
              • Vl-interface->binds
              • Vl-interface->assigns
              • Vl-interface->aliases
              • Vl-interface->ports
              • Vl-interface->atts
            • Vl-design
            • Vl-assign
            • Vl-modinst
            • Vl-gateinst
            • Vl-taskdecl
            • Vl-portdecl
            • Vl-commentmap
            • Vl-dpiimport
            • Vl-ansi-portdecl
            • Vl-package
            • Vl-paramdecl
            • Vl-dpiexport
            • Vl-class
            • Vl-sort-blockitems-aux
            • Vl-plainarglist->exprs
            • Vl-taskdecllist->names
            • Expressions-and-datatypes
            • Vl-fundecllist->names
            • Vl-udp
            • Vl-port
            • Vl-genelement
            • Vl-clkdecl
            • Vl-parse-temps
            • Vl-bind
            • Vl-namedarg
            • Vl-exprdist
            • Vl-clkassign
            • Vl-range
            • Vl-propport
            • Vl-typedef
            • Vl-gatedelay
            • Vl-dimension
            • Vl-sequence
            • Vl-clkskew
            • Vl-program
            • Vl-gatestrength
            • Vl-property
            • Vl-config
            • Vl-always
            • Vl-import
            • Vl-repeateventcontrol
            • Vl-timeliteral
            • Vl-initial
            • Vl-eventcontrol
            • Vl-final
            • Vl-udpsymbol-p
            • Vl-maybe-clkskew
            • Vl-function-specialization
            • Vl-alias
            • Vl-maybe-nettypename
            • Vl-maybe-gatedelay
            • Vl-letdecl
            • Vl-direction-p
            • Vl-modelement
            • Vl-maybe-timeprecisiondecl
            • Vl-maybe-scopeid
            • Vl-maybe-gatestrength
            • Vl-maybe-direction
            • Vl-maybe-delayoreventcontrol
            • Vl-gclkdecl
            • Vl-fwdtypedef
            • Vl-maybe-udpsymbol-p
            • Vl-maybe-timeunitdecl
            • Vl-maybe-timeliteral
            • Vl-maybe-parse-temps
            • Vl-maybe-cstrength
            • Vl-arguments
            • Vl-maybe-module
            • Vl-maybe-design
            • Vl-covergroup
            • Vl-udpline
            • Vl-timeunitdecl
            • Vl-genvar
            • Vl-defaultdisable
            • Vl-context1
            • Vl-timeprecisiondecl
            • Vl-sort-blockitems
            • Vl-elabtask
            • Vl-udpedge
            • Vl-delaycontrol
            • Vl-context
            • Vl-ctxelement
            • Vl-ctxelement->loc
            • Vl-modelement->loc
            • Statements
            • Vl-blockitem
            • Vl-vardecllist
            • Vl-interface->ifports
            • Vl-syntaxversion
            • Vl-nettypename-p
            • Vl-module->ifports
            • Vl-lifetime-p
            • Vl-paramdecllist
            • Vl-modelementlist->genelements
            • Vl-importlist
            • Vl-typedeflist
            • Vl-gatetype-p
            • Vl-cstrength-p
            • Vl-port->name
            • Vl-genelement->loc
            • Vl-delayoreventcontrol
            • Vl-udpentry-p
            • Vl-portdecllist
            • Vl-elabtask->loc
            • Property-expressions
            • Vl-taskdecllist
            • Vl-port->loc
            • Vl-fundecllist
            • Vl-sequencelist
            • Vl-propertylist
            • Vl-portlist
            • Vl-dpiimportlist
            • Vl-dpiexportlist
            • Vl-classlist
            • Vl-arguments->args
            • Vl-alwaystype-p
            • Vl-modinstlist
            • Vl-importpart-p
            • Vl-importpart-fix
            • Vl-bindlist
            • Vl-initiallist
            • Vl-genvarlist
            • Vl-gclkdecllist
            • Vl-function-specialization-map
            • Vl-finallist
            • Vl-elabtasklist
            • Vl-defaultdisablelist
            • Vl-clkdecllist
            • Vl-cassertionlist
            • Vl-blockstmt-p
            • Vl-assignlist
            • Vl-assertionlist
            • Vl-alwayslist
            • Vl-aliaslist
            • Vl-udptable
            • Vl-udplist
            • Vl-udpentrylist
            • Vl-propportlist
            • Vl-programlist
            • Vl-packagelist
            • Vl-namedarglist
            • Vl-modulelist
            • Vl-modportlist
            • Vl-modport-portlist
            • Vl-letdecllist
            • Vl-interfacelist
            • Vl-gateinstlist
            • Vl-fwdtypedeflist
            • Vl-covergrouplist
            • Vl-configlist
            • Vl-clkassignlist
            • Vl-blockitemlist
            • Vl-ansi-portdecllist
            • Vl-regularportlist
            • Vl-paramdecllist-list
            • Vl-modelementlist
            • Vl-interfaceportlist
            • Vl-casekey-p
            • Sv::maybe-4veclist
          • Loader
          • Warnings
          • Getting-started
          • Utilities
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-interface

    Make-vl-interface

    Basic constructor macro for vl-interface structures.

    Syntax
    (make-vl-interface [:name <name>] 
                       [:imports <imports>] 
                       [:ports <ports>] 
                       [:portdecls <portdecls>] 
                       [:modports <modports>] 
                       [:vardecls <vardecls>] 
                       [:paramdecls <paramdecls>] 
                       [:fundecls <fundecls>] 
                       [:taskdecls <taskdecls>] 
                       [:typedefs <typedefs>] 
                       [:dpiimports <dpiimports>] 
                       [:dpiexports <dpiexports>] 
                       [:properties <properties>] 
                       [:sequences <sequences>] 
                       [:clkdecls <clkdecls>] 
                       [:gclkdecls <gclkdecls>] 
                       [:defaultdisables <defaultdisables>] 
                       [:binds <binds>] 
                       [:classes <classes>] 
                       [:elabtasks <elabtasks>] 
                       [:modinsts <modinsts>] 
                       [:assigns <assigns>] 
                       [:aliases <aliases>] 
                       [:assertions <assertions>] 
                       [:cassertions <cassertions>] 
                       [:alwayses <alwayses>] 
                       [:initials <initials>] 
                       [:finals <finals>] 
                       [:generates <generates>] 
                       [:genvars <genvars>] 
                       [:warnings <warnings>] 
                       [:minloc <minloc>] 
                       [:maxloc <maxloc>] 
                       [:atts <atts>] 
                       [:origname <origname>] 
                       [:comments <comments>] 
                       [:parse-temps <parse-temps>]) 
    

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

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

    Definition

    This is an ordinary make- macro introduced by defprod.

    Macro: make-vl-interface

    (defmacro make-vl-interface (&rest args)
      (std::make-aggregate 'vl-interface
                           args
                           '((:name)
                             (:imports)
                             (:ports)
                             (:portdecls)
                             (:modports)
                             (:vardecls)
                             (:paramdecls)
                             (:fundecls)
                             (:taskdecls)
                             (:typedefs)
                             (:dpiimports)
                             (:dpiexports)
                             (:properties)
                             (:sequences)
                             (:clkdecls)
                             (:gclkdecls)
                             (:defaultdisables)
                             (:binds)
                             (:classes)
                             (:elabtasks)
                             (:modinsts)
                             (:assigns)
                             (:aliases)
                             (:assertions)
                             (:cassertions)
                             (:alwayses)
                             (:initials)
                             (:finals)
                             (:generates)
                             (:genvars)
                             (:warnings)
                             (:minloc)
                             (:maxloc)
                             (:atts)
                             (:origname)
                             (:comments)
                             (:parse-temps))
                           'make-vl-interface
                           nil))

    Function: vl-interface

    (defun vl-interface (name imports ports portdecls
                              modports vardecls paramdecls fundecls
                              taskdecls typedefs dpiimports dpiexports
                              properties sequences clkdecls gclkdecls
                              defaultdisables binds classes elabtasks
                              modinsts assigns aliases assertions
                              cassertions alwayses initials finals
                              generates genvars warnings minloc maxloc
                              atts origname comments parse-temps)
     (declare
          (xargs :guard (and (stringp name)
                             (vl-importlist-p imports)
                             (vl-portlist-p ports)
                             (vl-portdecllist-p portdecls)
                             (vl-modportlist-p modports)
                             (vl-vardecllist-p vardecls)
                             (vl-paramdecllist-p paramdecls)
                             (vl-fundecllist-p fundecls)
                             (vl-taskdecllist-p taskdecls)
                             (vl-typedeflist-p typedefs)
                             (vl-dpiimportlist-p dpiimports)
                             (vl-dpiexportlist-p dpiexports)
                             (vl-propertylist-p properties)
                             (vl-sequencelist-p sequences)
                             (vl-clkdecllist-p clkdecls)
                             (vl-gclkdecllist-p gclkdecls)
                             (vl-defaultdisablelist-p defaultdisables)
                             (vl-bindlist-p binds)
                             (vl-classlist-p classes)
                             (vl-elabtasklist-p elabtasks)
                             (vl-modinstlist-p modinsts)
                             (vl-assignlist-p assigns)
                             (vl-aliaslist-p aliases)
                             (vl-assertionlist-p assertions)
                             (vl-cassertionlist-p cassertions)
                             (vl-alwayslist-p alwayses)
                             (vl-initiallist-p initials)
                             (vl-finallist-p finals)
                             (vl-genelementlist-p generates)
                             (vl-genvarlist-p genvars)
                             (vl-warninglist-p warnings)
                             (vl-location-p minloc)
                             (vl-location-p maxloc)
                             (vl-atts-p atts)
                             (stringp origname)
                             (vl-commentmap-p comments)
                             (vl-maybe-parse-temps-p parse-temps))))
     (declare (xargs :guard t))
     (let ((__function__ 'vl-interface))
      (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))
        (modports (mbe :logic (vl-modportlist-fix modports)
                       :exec modports))
        (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))
        (typedefs (mbe :logic (vl-typedeflist-fix typedefs)
                       :exec typedefs))
        (dpiimports (mbe :logic (vl-dpiimportlist-fix dpiimports)
                         :exec dpiimports))
        (dpiexports (mbe :logic (vl-dpiexportlist-fix dpiexports)
                         :exec dpiexports))
        (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))
        (binds (mbe :logic (vl-bindlist-fix binds)
                    :exec binds))
        (classes (mbe :logic (vl-classlist-fix classes)
                      :exec classes))
        (elabtasks (mbe :logic (vl-elabtasklist-fix elabtasks)
                        :exec elabtasks))
        (modinsts (mbe :logic (vl-modinstlist-fix modinsts)
                       :exec modinsts))
        (assigns (mbe :logic (vl-assignlist-fix assigns)
                      :exec assigns))
        (aliases (mbe :logic (vl-aliaslist-fix aliases)
                      :exec aliases))
        (assertions (mbe :logic (vl-assertionlist-fix assertions)
                         :exec assertions))
        (cassertions (mbe :logic (vl-cassertionlist-fix cassertions)
                          :exec cassertions))
        (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))
        (generates (mbe :logic (vl-genelementlist-fix generates)
                        :exec generates))
        (genvars (mbe :logic (vl-genvarlist-fix genvars)
                      :exec genvars))
        (warnings (mbe :logic (vl-warninglist-fix warnings)
                       :exec warnings))
        (minloc (mbe :logic (vl-location-fix minloc)
                     :exec minloc))
        (maxloc (mbe :logic (vl-location-fix maxloc)
                     :exec maxloc))
        (atts (mbe :logic (vl-atts-fix atts)
                   :exec atts))
        (origname (mbe :logic (str-fix origname)
                       :exec origname))
        (comments (mbe :logic (vl-commentmap-fix comments)
                       :exec comments))
        (parse-temps (mbe :logic (vl-maybe-parse-temps-fix parse-temps)
                          :exec parse-temps)))
       (cons
        :vl-interface
        (std::prod-cons
         (std::prod-cons
          (std::prod-cons
             (std::prod-cons (std::prod-cons name imports)
                             (std::prod-cons ports portdecls))
             (std::prod-cons
                  (std::prod-cons modports vardecls)
                  (std::prod-cons paramdecls
                                  (std::prod-cons fundecls taskdecls))))
          (std::prod-cons
           (std::prod-cons (std::prod-cons typedefs dpiimports)
                           (std::prod-cons dpiexports properties))
           (std::prod-cons
              (std::prod-cons sequences clkdecls)
              (std::prod-cons gclkdecls
                              (std::prod-cons defaultdisables binds)))))
         (std::prod-cons
          (std::prod-cons
              (std::prod-cons (std::prod-cons classes elabtasks)
                              (std::prod-cons modinsts assigns))
              (std::prod-cons
                   (std::prod-cons aliases assertions)
                   (std::prod-cons cassertions
                                   (std::prod-cons alwayses initials))))
          (std::prod-cons
               (std::prod-cons
                    (std::prod-cons finals generates)
                    (std::prod-cons genvars
                                    (std::prod-cons warnings minloc)))
               (std::prod-cons
                    (std::prod-cons maxloc atts)
                    (std::prod-cons
                         origname
                         (std::prod-cons comments parse-temps))))))))))