Search-engine friendly clone of the
ACL2 documentation
.
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
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Syntax
Vl-interface
Representation of a single
interface
.
This is a product type introduced by
defprod
.
Fields
name —
stringp
The name of this interface as a string.
ports —
vl-portlist
portdecls —
vl-portdecllist
paramdecls —
vl-paramdecllist
vardecls —
vl-vardecllist
modports —
vl-modportlist
generates —
vl-genelementlist
imports —
vl-importlist
warnings —
vl-warninglist
minloc —
vl-location
maxloc —
vl-location
atts —
vl-atts
origname —
stringp
comments —
vl-commentmap
loaditems —
vl-genelementlist
See
make-implicit-wires
. This is a temporary container to hold the module elements, in program order, until the rest of the design has been loaded.
BOZO incomplete stub -- we don't really support interfaces yet.
Subtopics
Vl-interface-p
Recognizer for
vl-interface
structures.
Vl-interface-fix
Fixing function for
vl-interface
structures.
Vl-modport-port
A single port from a modport declaration.
Vl-modport
A modport declaration within an interface
Make-vl-interface
Basic constructor macro for
vl-interface
structures.
Vl-interface-equiv
Basic equivalence relation for
vl-interface
structures.
Change-vl-interface
Modifying constructor for
vl-interface
structures.
Vl-interface->paramdecls
Get the
paramdecls
field from a
vl-interface
.
Vl-interface->loaditems
Get the
loaditems
field from a
vl-interface
.
Vl-interface->generates
Get the
generates
field from a
vl-interface
.
Vl-interface->warnings
Get the
warnings
field from a
vl-interface
.
Vl-interface->vardecls
Get the
vardecls
field from a
vl-interface
.
Vl-interface->portdecls
Get the
portdecls
field from a
vl-interface
.
Vl-interface->origname
Get the
origname
field from a
vl-interface
.
Vl-interface->modports
Get the
modports
field from a
vl-interface
.
Vl-interface->imports
Get the
imports
field from a
vl-interface
.
Vl-interface->comments
Get the
comments
field from a
vl-interface
.
Vl-interface->ports
Get the
ports
field from a
vl-interface
.
Vl-interface->name
Get the
name
field from a
vl-interface
.
Vl-interface->minloc
Get the
minloc
field from a
vl-interface
.
Vl-interface->maxloc
Get the
maxloc
field from a
vl-interface
.
Vl-interface->atts
Get the
atts
field from a
vl-interface
.