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
Getting-started
Utilities
Loader
Transforms
Lint
Mlib
Server
Kit
Printer
Ps
Basic-printing
Verilog-printing
Printing-locally
Formatted-printing
Accessing-printed-output
Vl-printedlist
Json-printing
Json-encoders
Vl-jp-module
Vl-jp-warning
Vl-jp-constint
Vl-jp-vardecl
Jp-sym-main
Vl-jp-fundecl
Vl-jp-taskdecl
Vl-jp-modinst
Vl-jp-gateinst
Vl-jp-portdecl
Vl-jp-modport-port
Vl-jp-interfaceport
Vl-jp-expr
Vl-jp-atomguts
Vl-jp-exprlist-aux
Vl-jp-exprlist
Vl-jp-atts-aux
Vl-jp-atts
Vl-jp-assign
Jp-str
Vl-jp-warninglist
Vl-jp-vardecllist
Vl-jp-taskdecllist
Vl-jp-regularportlist
Vl-jp-portdecllist
Vl-jp-plainarglist
Vl-jp-paramvaluelist
Vl-jp-paramdecllist
Vl-jp-paramdecl
Vl-jp-packeddimensionlist
Vl-jp-namedparamvaluelist
Vl-jp-namedarglist
Vl-jp-modport-portlist
Vl-jp-modinstlist
Vl-jp-modelementlist
Vl-jp-interfaceportlist
Vl-jp-initiallist
Vl-jp-genelementlist
Vl-jp-gateinstlist
Vl-jp-fwdtypedef
Vl-jp-fundecllist
Vl-jp-enumitemlist
Jp-nat
Vl-jp-weirdint
Vl-jp-repeateventcontrol
Vl-jp-regularport
Vl-jp-rangelist
Vl-jp-portlist
Vl-jp-plainarg
Vl-jp-namedparamvalue
Vl-jp-namedarg
Vl-jp-modulelist
Vl-jp-modport
Vl-jp-location
Vl-jp-initial
Vl-jp-importlist
Vl-jp-import
Vl-jp-genvarlist
Vl-jp-genvar
Vl-jp-gatestrength
Vl-jp-gatedelay
Vl-jp-eventcontrol
Vl-jp-evatomlist
Vl-jp-enumitem
Vl-jp-enumbasetype
Vl-jp-assignlist
Vl-jp-alwayslist
Vl-jp-always
Vl-jp-aliaslist
Vl-jp-alias
Jp-object
Vl-jp-time
Vl-jp-sysfunname
Vl-jp-range
Vl-jp-evatom
Vl-jp-delaycontrol
Vl-jp-basictype
Vl-jp-typename
Vl-jp-tagname
Vl-jp-string
Vl-jp-real
Vl-jp-keyguts
Vl-jp-id
Vl-jp-hidpiece
Vl-jp-funname
Vl-jp-extint
Vl-jp-arguments
Vl-jp-paramvalue
Vl-jp-packeddimension
Vl-jp-maybe-packeddimension
Vl-jp-maybe-nettypename
Vl-jp-maybe-direction
Vl-jp-maybe-cstrength
Jp-timeunit
Jp-keygutstype
Jp-bool
Jp-bitlist
Jp-bit
Jp-bignat
Jp-basictypekind
Vl-jp-randomqualifier
Vl-jp-port
Vl-jp-nettypename
Vl-jp-maybe-gatedelay
Vl-jp-maybe-exprtype
Vl-jp-lifetime
Vl-jp-gatetype
Vl-jp-exprtype
Vl-jp-evatomtype
Vl-jp-dstrength
Vl-jp-direction
Vl-jp-deassign-type
Vl-jp-cstrength
Vl-jp-coretypename
Vl-jp-casetype
Vl-jp-casecheck
Vl-jp-assign-type
Vl-jp-alwaystype
Jp-maybe-string
Jp-maybe-nat
Jp-sym
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
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-atomguts
Vl-jp-exprlist-aux
Vl-jp-exprlist
Vl-jp-atts-aux
Vl-jp-atts