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
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Address
Wire
Wire-fix
Wire-p
Make-wire
Wire-equiv
Change-wire
Wire->name
Wire->low-idx
Wire->delay
Wire->width
Wire->type
Wire->atts
Wirelist
Wire->revp
Wiretype
Module
Lhs
Path
Svar-add-namespace
Design
Modinst
Lhs-add-namespace
Modalist
Path-add-namespace
Modname->submodnames
Name
Constraintlist-addr-p
Svex-alist-addr-p
Svar-map-addr-p
Lhspairs-addr-p
Modname
Assigns-addr-p
Lhs-addr-p
Lhatom-addr-p
Modhier-list-measure
Attributes
Modhier-measure
Modhier-list-measure-aux
Modhier-loopfreelist-p
Modhier-loopfree-p
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Svmods
Wire
Wire info as stored in an svex module.
This is a product type introduced by
defprod
.
Fields
name —
name
width —
posp
The declared width of the wire
low-idx —
integerp
The declared lower index of the wire's range. This may be the MSB or the LSB (depending on revp), or both if the wire is only 1 bit.
delay —
maybe-posp
revp
If true, the range was declared as [low:high] rather than [high:low], so the low-idx is the MSB rather than the LSB.
type —
wiretype
atts —
attributes
Subtopics
Wire-fix
Fixing function for
wire
structures.
Wire-p
Recognizer for
wire
structures.
Make-wire
Basic constructor macro for
wire
structures.
Wire-equiv
Basic equivalence relation for
wire
structures.
Change-wire
Modifying constructor for
wire
structures.
Wire->name
Get the
name
field from a
wire
.
Wire->low-idx
Get the
low-idx
field from a
wire
.
Wire->delay
Get the
delay
field from a
wire
.
Wire->width
Get the
width
field from a
wire
.
Wire->type
Get the
type
field from a
wire
.
Wire->atts
Get the
atts
field from a
wire
.
Wirelist
A list of
wire-p
objects.
Wire->revp
Get the
revp
field from a
wire
.
Wiretype