Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Warnings
Primitives
Use-set
Syntax
Getting-started
Utilities
Loader
Transforms
Expression-sizing
Occform
Oprewrite
Expand-functions
Delayredux
Unparameterization
Caseelim
Split
Selresolve
Weirdint-elim
Vl-delta
Replicate-insts
Rangeresolve
Propagate
Clean-selects
Clean-params
Blankargs
Inline-mods
Expr-simp
Trunc
Always-top
Gatesplit
Gate-elim
Expression-optimization
Elim-supplies
Wildelim
Drop-blankports
Clean-warnings
Addinstnames
Custom-transform-hooks
Annotate
Make-implicit-wires
Vl-modulelist-make-implicit-wires
Vl-make-implicit-wires-aux
Shadowcheck
Vl-stmt-check-undeclared
Vl-stmtlist-check-undeclared
Vl-make-implicit-wires-main
Vl-fundecl-check-undeclared
Vl-warn-about-undeclared-wires
Vl-implicitst
Vl-blockitem-check-undeclared
Vl-taskdecl-check-undeclared
Vl-modinst-exprs-for-implicit-wires
Vl-blockitemlist-check-undeclared
Vl-import-check-undeclared
Vl-make-ordinary-implicit-wires
Vl-gateinst-exprs-for-implicit-wires
Vl-remove-declared-wires
Vl-make-port-implicit-wires
Vl-module-make-implicit-wires
Vl-vardecl-exprs-for-implicit-wires
Vl-design-make-implicit-wires
Resolve-indexing
Origexprs
Argresolve
Portdecl-sign
Designwires
Udp-elim
Vl-annotate-design
Latchcode
Elim-unused-vars
Problem-modules
Lint
Mlib
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-stmt-check-undeclared
Vl-stmtlist-check-undeclared
Signature
(vl-stmtlist-check-undeclared ctx x st warnings) → new-warnings
Arguments
ctx
—
Guard
(
vl-modelement-p
ctx)
.
x
—
Guard
(
vl-stmtlist-p
x)
.
st
—
Guard
(
vl-implicitst-p
st)
.
warnings
—
Guard
(
vl-warninglist-p
warnings)
.
Returns
new-warnings
—
Type
(
vl-warninglist-p
new-warnings)
.