• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Expressions
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
            • Vl-interface-p
            • Vl-interface-fix
            • Vl-modport-port
            • Vl-modport
            • Make-vl-interface
              • Vl-interface-equiv
              • Change-vl-interface
              • Vl-interface->paramdecls
              • Vl-interface->loaditems
              • Vl-interface->generates
              • Vl-interface->warnings
              • Vl-interface->vardecls
              • Vl-interface->portdecls
              • Vl-interface->origname
              • Vl-interface->modports
              • Vl-interface->imports
              • Vl-interface->comments
              • Vl-interface->ports
              • Vl-interface->name
              • Vl-interface->minloc
              • Vl-interface->maxloc
              • Vl-interface->atts
            • Vl-plainarglist->exprs
            • Vl-taskdecllist->names
            • Vl-fundecllist->names
            • Vl-package
            • Vl-port
            • Vl-udp
            • Vl-paramdecl
            • Vl-genelement
            • Vl-cycledelayrange
            • Vl-namedarg
            • Vl-sort-blockitems-aux
            • Vl-distitem
            • Vl-gatedelay
            • Vl-repetition
            • Vl-typedef
            • Vl-range
            • Vl-gatestrength
            • Vl-program
            • Vl-config
            • Vl-always
            • Vl-datatype-update-dims
            • Vl-import
            • Vl-enumbasetype
            • Vl-repeateventcontrol
            • Vl-paramargs
            • Vl-initial
            • Vl-eventcontrol
            • Vl-udpsymbol-p
            • Vl-maybe-range
            • Vl-maybe-nettypename
            • Vl-maybe-gatestrength
            • Vl-maybe-gatedelay
            • Vl-maybe-delayoreventcontrol
            • Vl-alias
            • Maybe-string-fix
            • Vl-maybe-packeddimension
            • Vl-fwdtypedef
            • Vl-evatom
            • Vl-packeddimension-p
            • Vl-maybe-udpsymbol
            • Vl-maybe-module
            • Vl-maybe-direction
            • Vl-maybe-datatype
            • Vl-maybe-cstrength
            • Vl-direction-p
            • Vl-arguments
            • Vl-maybe-design
            • Vl-udpline
            • Vl-exprdist
            • Vl-context1
            • Vl-genvar
            • Vl-enumitem
            • Vl-datatype-update-udims
            • Vl-datatype-update-pdims
            • Vl-modelement
            • Vl-udpedge
            • Vl-delaycontrol
            • Vl-context
            • Vl-sort-blockitems
            • Vl-distweighttype-p
            • Vl-ctxelement->loc
            • Vl-blockitem
            • Vl-vardecllist
            • Vl-module->ifports
            • Vl-modelement->loc
            • Vl-ctxelement
            • Vl-coretypename-p
            • Vl-packeddimensionlist
            • Vl-modelementlist->genelements
            • Vl-gatetype-p
            • Vl-paramdecllist
            • Vl-lifetime-p
            • Vl-datatype->udims
            • Vl-datatype->pdims
            • Vl-timeunit-p
            • Vl-repetitiontype-p
            • Vl-port->name
            • Vl-importlist
            • Vl-genelement->loc
            • Vl-delayoreventcontrol
            • Vl-cstrength-p
            • Statements
            • Vl-udpentry-p
            • Vl-packeddimension-fix
            • Vl-nettypename-p
            • Vl-portdecllist
            • Vl-port->loc
            • Vl-enumbasekind-fix
            • Vl-arguments->args
            • Vl-taskdecllist
            • Vl-portlist
            • Vl-importpart-p
            • Vl-importpart-fix
            • Vl-fundecllist
            • Vl-blockstmt-p
            • Vl-assignlist
            • Vl-alwaystype-p
            • Vl-typedeflist
            • Vl-syntaxversion-p
            • Vl-randomqualifier-p
            • Vl-modinstlist
            • Vl-gateinstlist
            • Vl-blockitemlist
            • Vl-udptable
            • Vl-udplist
            • Vl-udpentrylist
            • Vl-programlist
            • Vl-paramvaluelist
            • Vl-packagelist
            • Vl-namedparamvaluelist
            • Vl-namedarglist
            • Vl-modulelist
            • Vl-modportlist
            • Vl-modport-portlist
            • Vl-interfacelist
            • Vl-initiallist
            • Vl-genvarlist
            • Vl-fwdtypedeflist
            • Vl-evatomlist
            • Vl-enumitemlist
            • Vl-distlist
            • Vl-configlist
            • Vl-alwayslist
            • Vl-aliaslist
            • Vl-regularportlist
            • Vl-rangelist-list
            • Vl-rangelist
            • Vl-paramdecllist-list
            • Vl-modelementlist
            • Vl-maybe-range-list
            • Vl-interfaceportlist
            • Vl-argumentlist
            • Data-types
          • Getting-started
          • Utilities
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • 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>] 
                       [:ports <ports>] 
                       [:portdecls <portdecls>] 
                       [:paramdecls <paramdecls>] 
                       [:vardecls <vardecls>] 
                       [:modports <modports>] 
                       [:generates <generates>] 
                       [:imports <imports>] 
                       [:warnings <warnings>] 
                       [:minloc <minloc>] 
                       [:maxloc <maxloc>] 
                       [:atts <atts>] 
                       [:origname <origname>] 
                       [:comments <comments>] 
                       [:loaditems <loaditems>]) 
    

    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)
                             (:ports)
                             (:portdecls)
                             (:paramdecls)
                             (:vardecls)
                             (:modports)
                             (:generates)
                             (:imports)
                             (:warnings)
                             (:minloc)
                             (:maxloc)
                             (:atts)
                             (:origname)
                             (:comments)
                             (:loaditems))
                           'make-vl-interface
                           nil))

    Function: vl-interface

    (defun vl-interface (name ports
                              portdecls paramdecls vardecls modports
                              generates imports warnings minloc
                              maxloc atts origname comments loaditems)
     (declare (xargs :guard (and (stringp name)
                                 (vl-portlist-p ports)
                                 (vl-portdecllist-p portdecls)
                                 (vl-paramdecllist-p paramdecls)
                                 (vl-vardecllist-p vardecls)
                                 (vl-modportlist-p modports)
                                 (vl-genelementlist-p generates)
                                 (vl-importlist-p imports)
                                 (vl-warninglist-p warnings)
                                 (vl-location-p minloc)
                                 (vl-location-p maxloc)
                                 (vl-atts-p atts)
                                 (stringp origname)
                                 (vl-commentmap-p comments)
                                 (vl-genelementlist-p loaditems))))
     (declare (xargs :guard t))
     (let ((__function__ 'vl-interface))
      (declare (ignorable __function__))
      (b* ((name (mbe :logic (str-fix name) :exec name))
           (ports (mbe :logic (vl-portlist-fix ports)
                       :exec ports))
           (portdecls (mbe :logic (vl-portdecllist-fix portdecls)
                           :exec portdecls))
           (paramdecls (mbe :logic (vl-paramdecllist-fix paramdecls)
                            :exec paramdecls))
           (vardecls (mbe :logic (vl-vardecllist-fix vardecls)
                          :exec vardecls))
           (modports (mbe :logic (vl-modportlist-fix modports)
                          :exec modports))
           (generates (mbe :logic (vl-genelementlist-fix generates)
                           :exec generates))
           (imports (mbe :logic (vl-importlist-fix imports)
                         :exec imports))
           (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))
           (loaditems (mbe :logic (vl-genelementlist-fix loaditems)
                           :exec loaditems)))
       (cons
        :vl-interface
        (std::prod-cons
         (std::prod-cons
              (std::prod-cons name (std::prod-cons ports portdecls))
              (std::prod-cons (std::prod-cons paramdecls vardecls)
                              (std::prod-cons modports generates)))
         (std::prod-cons
              (std::prod-cons (std::prod-cons imports warnings)
                              (std::prod-cons minloc maxloc))
              (std::prod-cons (std::prod-cons atts origname)
                              (std::prod-cons comments loaditems))))))))