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
Svex-stvs
Svtv-data
Defsvtv$
Svtv-run
Defsvtv-phasewise
Svtv-spec
Svtv
Defsvtv
Process.lisp
Svtv-doc
Svtv-chase$
Svtv-versus-stv
Svtv-debug-fsm
Structure.lisp
Svtv-debug
Vcd.lisp
Elab-mod->vcd-wires
Vcd-scope
Vcd-wire
Vcd-wire-fix
Vcd-wire-equiv
Make-vcd-wire
Change-vcd-wire
Vcd-wire->name
Vcd-wire->msb
Vcd-wire->lsb
Vcd-wire->code
Vcd-wire-p
Vcd-print-4vec-aux
Vcd-dump-delta
Vcd-wirelist-add-to-wiremap
Vcd-print-header
Vcd-dump-first-snapshot-aux
Vcd-dump-delta-aux
Vcd-wiremap
4vecarr
Vcd-print-wiredecls
Vcd-4vec-bitstr
Vcd-index->codechars
Vcd-wire->width
Vcd-index->codestr
Vcd-dump-first-snapshot
Vcd-wirelist
Debug.lisp
Def-pipeline-thm
Expand.lisp
Def-cycle-thm
Svtv-utilities
Svtv-debug$
Defsvtv$-phasewise
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vcd.lisp
Vcd-wire
This is a product type introduced by
defprod
.
Fields
name —
stringp
msb —
integerp
lsb —
integerp
code —
stringp
Subtopics
Vcd-wire-fix
Fixing function for
vcd-wire
structures.
Vcd-wire-equiv
Basic equivalence relation for
vcd-wire
structures.
Make-vcd-wire
Basic constructor macro for
vcd-wire
structures.
Change-vcd-wire
Modifying constructor for
vcd-wire
structures.
Vcd-wire->name
Get the
name
field from a
vcd-wire
.
Vcd-wire->msb
Get the
msb
field from a
vcd-wire
.
Vcd-wire->lsb
Get the
lsb
field from a
vcd-wire
.
Vcd-wire->code
Get the
code
field from a
vcd-wire
.
Vcd-wire-p
Recognizer for
vcd-wire
structures.