		Search-engine friendly clone of the ACL2 documentation.

E-conversion

Modinsts-to-eoccs

How we convert Verilog modules instances into (preliminary) E module occurrences.

This documentation assumes you have already read e-conversion. Note that the E occurrences we generate in this initial pass are only preliminary and might include multiple drivers of certain wires. See also exploding-vectors, since we are going to be doing a lot of that.

To convert each Verilog module instance into preliminary E occurrences, we need to create E language ACL2::patterns that represent (1) the inputs and outputs of each module, i.e., the :i and :o patterns for each module, and (2) the corresponding "actuals" of each module instance, i.e., the :i and :o patterns for each occurrence.

Basic Idea

Suppose we have a module with port declarations like:

input [3:0] a;
input b;
input [5:3] c;

...

Then we are going to generate an input pattern like:

:i ( (a[0] a[1] a[2] a[3])
     (b)
     (c[3] c[4] c[5])
     ...)

Here, individual bits like a[2] and b are vl-emodwire-ps. The bits for each vector form a vl-emodwirelist-p like (a[0] a[1] a[2] a[3]) or (b). Finally, our full :i and :o patterns are lists of such vectors, and are recognized with vl-emodwirelistlist-p.

Module I/O Patterns

Recall the difference between port declarations (see vl-portdecl-p) and ports (see vl-port-p). For instance:

module mymod (.low(vec[3:0]), .high(vec[5:4]), foo)   <-- ports
  input foo;
  input [5:0] vec;   <-- port declarations
endmodule

We generate the :i and :o patterns for each module from their port declarations, not from thir ports; see vl-portdecls-to-i/o for details. Because of this, the actual input pattern for mymod would look like this:

:i ((foo)
    (vec[0] vec[1] vec[2] vec[3] vec[4] vec[5]))

Port Patterns

An instance of this mymod might look something like this:

mymod myinstance (a[3:0], b[1:0], c[7]);

Unfortunately, the I/O patterns we have generated for mymod are not very useful when we want to translate myinstance, because its entries are not at all in the same shape or order as the ports.

To correct for this, we build a port pattern for each module. For instance, the port pattern for mymod would be:

((vec[3] vec[2] vec[1] vec[0])
 (vec[5] vec[4])
 (foo))

The port pattern matches the shape of the module's port expressions, and lists the wires each port is connected to, in MSB-first order.

Port patterns are generated by vl-portlist-msb-bit-pattern. We can carry out certain checking to ensure that the port pattern mentions every input and output wire without duplication; see port-bit-checking.

Preliminary E Occurrences

Port patterns make it pretty easy to create the E occurrence for a module instance. In particular, for any valid module instance, we can explode the "actuals" into wires that line up perfectly with the port pattern. In the case of myinstance, we sort of intuitively might imagine generating the following "actual pattern":

((a[3] a[2] a[1] a[0])
 (b[1] b[0])
 (c[7]))

We don't actually build this pattern. Instead, we directly construct an alist that binds each formal to its actual; see vl-modinst-eocc-bindings.

The :i and :o patterns for the module may then be instantiated with this pattern to form the :i and :o fields for the occurrence. The main function that does all of this is vl-modinst-to-eocc.

Subtopics

Vl-modinst-to-eocc: Main function for transforming a Verilog module instance into an (preliminary) E language occurrence.
Vl-modinst-eocc-bindings: Build a (slow) alist binding the "formals" for a module to the "actuals" from an instance.
Vl-portdecls-to-i/o: Compute the :i and :o fields for a module.
Vl-plainarglist-lsb-pattern: Build lists of vl-emodwire-ps for a vl-plainarglist-p.
Vl-modinstlist-to-eoccs: Build the preliminary E-language occurrences for a list of module instances.
Vl-portlist-msb-bit-pattern: Compute the port pattern for a module.
Vl-plainarg-lsb-bits: Build the list of vl-emodwire-ps for a vl-plainarg-p, in LSB-first order.
Vl-port-msb-bits: Compute the port pattern for a single port.