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-repeateventcontrol-weirdint-elim
Vl-maybe-delayoreventcontrol-weirdint-elim
Vl-module-add-x/z-wire
Vl-delayoreventcontrol-weirdint-elim
Vl-plainarglist-weirdint-elim
Vl-namedarglist-weirdint-elim
Vl-modinstlist-weirdint-elim
Vl-initiallist-weirdint-elim
Vl-gateinstlist-weirdint-elim
Vl-eventcontrol-weirdint-elim
Vl-delaycontrol-weirdint-elim
Vl-arguments-weirdint-elim
Vl-evatomlist-weirdint-elim
Vl-assignlist-weirdint-elim
Vl-alwayslist-weirdint-elim
Vl-plainarg-weirdint-elim
Vl-namedarg-weirdint-elim
Vl-module-weirdint-elim
Vl-gateinst-weirdint-elim
Vl-assign-weirdint-elim
Vl-modinst-weirdint-elim
Vl-maybe-expr-weirdint-elim
Vl-initial-weirdint-elim
Vl-evatom-weirdint-elim
Vl-always-weirdint-elim
Vl-weirdint-to-concat
Vl-weirdint-bits-to-exprs
Vl-modulelist-weirdint-elim-aux
Vl-modulelist-weirdint-elim
Vl-design-weirdint-elim
*vl-z-wire-expr*
*vl-x-wire-expr*
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
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
Weirdint-elim
*vl-x-wire-expr*
Definition:
*vl-x-wire-expr*
(
defconst
*vl-x-wire-expr* (
vl-idexpr
"vl-x-wire" 1 :vl-unsigned))