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
Fgl
Vwsim
Vl
Syntax
Loader
Warnings
Getting-started
Utilities
Printer
Ps
Verilog-printing
Basic-printing
Printing-locally
Formatted-printing
Accessing-printed-output
Json-printing
Json-encoders
Vl-jp-expr
Vl-jp-valuerangelist-aux
Vl-jp-valuerangelist
Vl-jp-valuerange
Vl-jp-structmemberlist-aux
Vl-jp-structmemberlist
Vl-jp-structmember
Vl-jp-streamexprlist-aux
Vl-jp-streamexprlist
Vl-jp-streamexpr
Vl-jp-slicesize
Vl-jp-scopeexpr
Vl-jp-range
Vl-jp-plusminus
Vl-jp-patternkey
Vl-jp-partselect
Vl-jp-maybe-range
Vl-jp-maybe-exprlist-aux
Vl-jp-maybe-exprlist
Vl-jp-maybe-expr
Vl-jp-maybe-dimension
Vl-jp-maybe-datatype
Vl-jp-keyvallist-aux
Vl-jp-keyvallist
Vl-jp-hidindex
Vl-jp-hidexpr-aux
Vl-jp-hidexpr
Vl-jp-exprlist-aux
Vl-jp-exprlist
Vl-jp-evatomlist-aux
Vl-jp-evatomlist
Vl-jp-evatom
Vl-jp-enumitemlist-aux
Vl-jp-enumitemlist
Vl-jp-enumitem
Vl-jp-dimensionlist-aux
Vl-jp-dimensionlist
Vl-jp-dimension
Vl-jp-datatype
Vl-jp-casttype
Vl-jp-call-namedargs-aux
Vl-jp-call-namedargs
Vl-jp-atts-aux
Vl-jp-atts
Vl-jp-assignpat
Vl-jp-arrayrange
Vl-jp-module
Vl-jp-interface
Vl-jp-design
Vl-jp-warning
Vl-jp-package
Vl-jp-vardecl
Vl-jp-class
Vl-jp-ansi-portdecl
Vl-jp-constint
Jp-sym-main
Vl-jp-udp
Vl-jp-taskdecl
Vl-jp-fundecl
Vl-jp-clkdecl
Vl-jp-modinst
Vl-jp-gateinst
Vl-jp-dpiimport
Vl-jp-typedef
Vl-jp-propport
Vl-jp-program
Vl-jp-portdecl
Vl-jp-paramdecl
Vl-jp-modport-port
Vl-jp-interfaceport
Vl-jp-dpiexport
Vl-jp-config
Vl-jp-assign
Jp-str
Vl-jp-warninglist
Vl-jp-vardecllist
Vl-jp-udpentrylist
Vl-jp-typedeflist
Vl-jp-taskdecllist
Vl-jp-sequencelist
Vl-jp-sequence
Vl-jp-propportlist
Vl-jp-propertylist
Vl-jp-property
Vl-jp-programlist
Vl-jp-portdecllist
Vl-jp-plainarglist
Vl-jp-parse-temps
Vl-jp-paramvaluelist
Vl-jp-paramdecllist
Vl-jp-packagelist
Vl-jp-namedparamvaluelist
Vl-jp-namedarglist
Vl-jp-modportlist
Vl-jp-modport-portlist
Vl-jp-modinstlist
Vl-jp-locationlist
Vl-jp-interfacelist
Vl-jp-initiallist
Vl-jp-gclkdecllist
Vl-jp-gateinstlist
Vl-jp-fwdtypedeflist
Vl-jp-fwdtypedef
Vl-jp-fundecllist
Vl-jp-exprdistlist
Vl-jp-elabtasklist
Vl-jp-dpiimportlist
Vl-jp-dpiexportlist
Vl-jp-defaultdisablelist
Vl-jp-covergrouplist
Vl-jp-clkdecllist
Vl-jp-clkassignlist
Vl-jp-clkassign
Vl-jp-cassertionlist
Vl-jp-blockitemlist
Vl-jp-bind
Vl-jp-assertionlist
Vl-jp-ansi-portdecllist
Jp-nat
Vl-jp-udplist
Vl-jp-udplinelist
Vl-jp-udpline
Vl-jp-timeunitdecl
Vl-jp-timeprecisiondecl
Vl-jp-repetition
Vl-jp-repeateventcontrol
Vl-jp-regularport
Vl-jp-propspec
Vl-jp-portlist
Vl-jp-plainarg
Vl-jp-namedparamvalue
Vl-jp-namedarg
Vl-jp-modulelist
Vl-jp-modport
Vl-jp-initial
Vl-jp-importlist
Vl-jp-import
Vl-jp-genvarlist
Vl-jp-gclkdecl
Vl-jp-gatestrength
Vl-jp-gatedelay
Vl-jp-finallist
Vl-jp-eventcontrol
Vl-jp-distitemlist
Vl-jp-distitem
Vl-jp-defaultdisable
Vl-jp-covergroup
Vl-jp-configlist
Vl-jp-classlist
Vl-jp-bindlist
Vl-jp-assignlist
Vl-jp-alwayslist
Vl-jp-always
Vl-jp-aliaslist
Vl-jp-alias
Jp-object
Vl-jp-udpedge
Vl-jp-timeliteral
Vl-jp-maybe-timeunitdecl
Vl-jp-maybe-timeprecisiondecl
Vl-jp-maybe-gatestrength
Vl-jp-maybe-delayoreventcontrol
Vl-jp-genvar
Vl-jp-final
Vl-jp-exprdist
Vl-jp-delaycontrol
Vl-jp-clkskew
Vl-jp-maybe-udpsymbol
Vl-jp-maybe-timeliteral
Vl-jp-maybe-scopeid
Vl-jp-maybe-rhs
Vl-jp-maybe-parse-temps
Vl-jp-maybe-paramvalue
Vl-jp-maybe-nettypename
Vl-jp-maybe-module
Vl-jp-maybe-gatedelay
Vl-jp-maybe-exprdist
Vl-jp-maybe-clkskew
Vl-jp-elabtask
Vl-jp-weirdint
Vl-jp-value
Vl-jp-time
Vl-jp-string
Vl-jp-maybe-direction
Vl-jp-maybe-cstrength
Vl-jp-extint
Jp-timeunit
Jp-bool
Jp-bitlist
Jp-bit
Jp-bignat
Vl-jp-real
Vl-jp-maybe-exprsign
Vl-jp-gatetype
Vl-jp-exprsign
Vl-jp-evatomtype
Vl-jp-dstrength
Vl-jp-direction
Vl-jp-deassign-type
Vl-jp-cstrength
Vl-jp-casetype
Vl-jp-casekey
Vl-jp-casecheck
Vl-jp-assign-type
Vl-jp-alwaystype
Jp-maybe-string
Jp-maybe-nat
Jp-sym
Vl-printedlist
Kit
Mlib
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Json-encoders
Vl-jp-expr
Signature
(vl-jp-expr x &key (ps 'ps)) → ps
Arguments
x
—
Guard
(
vl-expr-p
x)
.
Subtopics
Vl-jp-valuerangelist-aux
Vl-jp-valuerangelist
Vl-jp-valuerange
Vl-jp-structmemberlist-aux
Vl-jp-structmemberlist
Vl-jp-structmember
Vl-jp-streamexprlist-aux
Vl-jp-streamexprlist
Vl-jp-streamexpr
Vl-jp-slicesize
Vl-jp-scopeexpr
Vl-jp-range
Vl-jp-plusminus
Vl-jp-patternkey
Vl-jp-partselect
Vl-jp-maybe-range
Vl-jp-maybe-exprlist-aux
Vl-jp-maybe-exprlist
Vl-jp-maybe-expr
Vl-jp-maybe-dimension
Vl-jp-maybe-datatype
Vl-jp-keyvallist-aux
Vl-jp-keyvallist
Vl-jp-hidindex
Vl-jp-hidexpr-aux
Vl-jp-hidexpr
Vl-jp-exprlist-aux
Vl-jp-exprlist
Vl-jp-evatomlist-aux
Vl-jp-evatomlist
Vl-jp-evatom
Vl-jp-enumitemlist-aux
Vl-jp-enumitemlist
Vl-jp-enumitem
Vl-jp-dimensionlist-aux
Vl-jp-dimensionlist
Vl-jp-dimension
Vl-jp-datatype
Vl-jp-casttype
Vl-jp-call-namedargs-aux
Vl-jp-call-namedargs
Vl-jp-atts-aux
Vl-jp-atts
Vl-jp-assignpat
Vl-jp-arrayrange
