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
module does_nothing(out, a, b);
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.
- Top-level function for adding drivers for undriven outputs.
- Generate instances of ACL2::*esim-z* to drive undriven output
- Generate an instance of ACL2::*esim-z* to drive an
otherwise-undriven output bit.