		Search-engine friendly clone of the ACL2 documentation.

Esim-vl

Functions for working with E modules produced by VL.

Esim-vl-find-io: Produce an LSB-first list of E wire names corresponding to a particular input or output of the original Verilog module.
Esim-vl-iopattern-p: Recognize a good :i or :o pattern for a VL-translated module.
Esim-vl-designwires: Produce a flat vl-emodwirelist-p that contains the E names of every bit that is visible in the original Verilog module.
Esim-vl-wirealist: Obtain the vl-wirealist-p for an E module produced by VL.
Esim-vl-annotations: Helper for esim-vl-designwires and esim-vl-wirealist.