Exploding-vectors
How we convert Verilog wires (which might be vectors) into E
wires (which are just bits).
A significant difference between E and Verilog is that there are no
vectors in E. Whereas our Verilog module might have a vector like wire
[7:0] w, our E module will instead have eight individual wires, whose names
are ACL2::|w[7]| through ACL2::|w[0]|.
There is a fair bit of code geared towards making this bit-level conversion
safe and efficient. As a quick summary:
- We represent each of these "exploded" wires like ACL2::|w[0]| as an
vl-emodwire-p. This representation includes an encoding scheme that
usually produces readable names and avoids name clashes, even when escaped
identifiers are used.
- The E wires for all of a module's net and register declarations can be
bundled into a vl-wirealist-p. A wire alist is generally constructed
with vl-module-wirealist, which provides certain uniqueness
guarantees.
- Certain "simple" expressions (similar to sliceable expressions) can be converted into wires using
vl-msb-expr-bitlist, which does lots of sanity checking to ensure that
the sizes and bounds of the expressions are correct and that only defined wires
are being used.
BOZO much of this code predates the exprsesion slicing code. We may wish to
eventually redo significant portions of the wirealist stuff to instead be based
on the expression-slicing code.
Subtopics
- Vl-wirealist-p
- Associates wire names (strings) to lists of vl-emodwire-ps
which represent the wire's bits in msb-first order.
- Emodwire-encoding
- A simple encoding scheme to basenames that are free of certain
special characters.
- Vl-emodwire-p
- (vl-emodwire-p x) recognizes symbols that VL generates as wire
names for E modules.
- Vl-emodwirelistlist
- A list of vl-emodwire-p lists.
- Vl-emodwirelist
- A list of vl-emodwire-p objects.
