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
Sv
Vwsim
Fgl
Vl
Syntax
Vl-module
Vl-vardecl
Vl-fundecl
Vl-interface
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-udp-p
Vl-udp-fix
Make-vl-udp
Vl-udp-equiv
Change-vl-udp
Vl-udp->sequentialp
Vl-udp->warnings
Vl-udp->name
Vl-udp->minloc
Vl-udp->inputs
Vl-udp->initval
Vl-udp->comments
Vl-udp->table
Vl-udp->output
Vl-udp->maxloc
Vl-udp->atts
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
Syntax
Vl-udp
Representation of a user defined
primitive
.
This is a product type introduced by
defprod
.
Fields
name —
stringp
The name of this udp as a string.
output —
vl-portdecl
Declaration of the output port, which always comes first.
inputs —
vl-portdecllist
Port declarations for the input ports, in order.
sequentialp —
booleanp
True when this is a sequential (instead of combinational) UDP.
table —
vl-udptable
The UDP state table.
initval —
vl-maybe-expr
For sequential UDPs, the initial value for the register, if specified.
warnings —
vl-warninglist
minloc —
vl-location
maxloc —
vl-location
atts —
vl-atts
comments —
vl-commentmap
Subtopics
Vl-udp-p
Recognizer for
vl-udp
structures.
Vl-udp-fix
Fixing function for
vl-udp
structures.
Make-vl-udp
Basic constructor macro for
vl-udp
structures.
Vl-udp-equiv
Basic equivalence relation for
vl-udp
structures.
Change-vl-udp
Modifying constructor for
vl-udp
structures.
Vl-udp->sequentialp
Get the
sequentialp
field from a
vl-udp
.
Vl-udp->warnings
Get the
warnings
field from a
vl-udp
.
Vl-udp->name
Get the
name
field from a
vl-udp
.
Vl-udp->minloc
Get the
minloc
field from a
vl-udp
.
Vl-udp->inputs
Get the
inputs
field from a
vl-udp
.
Vl-udp->initval
Get the
initval
field from a
vl-udp
.
Vl-udp->comments
Get the
comments
field from a
vl-udp
.
Vl-udp->table
Get the
table
field from a
vl-udp
.
Vl-udp->output
Get the
output
field from a
vl-udp
.
Vl-udp->maxloc
Get the
maxloc
field from a
vl-udp
.
Vl-udp->atts
Get the
atts
field from a
vl-udp
.