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
Symbolic-test-vectors
Esim-primitives
E-conversion
Vl-ealist-p
Modinsts-to-eoccs
Vl-module-make-esim
Exploding-vectors
Vl-wirealist-p
Vl-msb-expr-bitlist
Vl-msb-partselect-bitlist
Vl-msb-bitselect-bitlist
Vl-msb-constint-bitlist
Vl-msb-wire-bitlist
Vl-msb-replicate-bitlist
Vl-msb-exprlist-bitlist
Vl-plain-wire-name
Vl-module-wirealist
Vl-emodwires-from-high-to-low
Vl-vardecl-msb-emodwires
Vl-vardecllist-to-wirealist
Vl-emodwires-from-msb-to-lsb
Vl-verilogify-emodwirelist
Emodwire-encoding
Vl-emodwire-p
Vl-emodwirelistlist
Vl-emodwirelist
Resolving-multiple-drivers
Vl-modulelist-make-esims
Vl-module-check-e-ok
Vl-collect-design-wires
Adding-z-drivers
Vl-design-to-e
Vl-design-to-e-check-ports
Vl-design-to-e-main
Port-bit-checking
Esim-steps
Patterns
Mod-internal-paths
Defmodules
Esim-simplify-update-fns
Esim-tutorial
Esim-vl
Vl2014
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-msb-expr-bitlist
Vl-msb-exprlist-bitlist
Signature
(vl-msb-exprlist-bitlist x walist warnings) → (mv successp warnings bits)
Arguments
x
—
Guard
(
vl-exprlist-p
x)
.
walist
—
Guard
(
vl-wirealist-p
walist)
.
warnings
—
Guard
(
vl-warninglist-p
warnings)
.
Returns
successp
—
Type
(
booleanp
successp)
.
warnings
—
Type
(
vl-warninglist-p
warnings)
.
bits
—
Type
(
vl-emodwirelist-p
bits)
.