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
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 a a a) (b) (c c c) ...)
Here, individual bits like
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 ((foo) (vec vec vec vec vec vec))
An instance of this mymod might look something like this:
mymod myinstance (a[3:0], b[1:0], c);
Unfortunately, the I/O patterns we have generated for
To correct for this, we build a port pattern for each module. For
instance, the port pattern for
((vec vec vec vec) (vec vec) (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.
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
((a a a a) (b b) (c))
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.