Adding-z-drivers
How we ensure every wire is driven.
The good-esim-modulep well-formedness check requires that
every wire of a module is driven by some occurrence (or is an input). But in
Verilog there is no such requirement, e.g., one can legally write a module like
this:
module does_nothing(out, a, b);
output out;
input a;
input b;
wire internal;
endmodule
Where there aren't any drivers on out or internal.
To correct for this, in our e-conversion we look for any output bits
and also any internal wires that are used as inputs to a submodule but are
never driven by the preliminary occurrences produced by modinsts-to-eoccs. For any such bit, we add an explicit ACL2::*esim-z*
module to drive it.
Subtopics
- Vl-add-zdrivers
- Top-level function for adding drivers for undriven outputs.
- Vl-make-z-occs
- Generate instances of ACL2::*esim-z* to drive undriven output
bits.
- Vl-make-z-occ
- Generate an instance of ACL2::*esim-z* to drive an
otherwise-undriven output bit.
