VIS

VIS is partitioned into three main components:

1. VIS-F - The front end. It provides the ability to read and write BLIF-MV files, and supports a hierarchical data structure mimicking the constructs of BLIF-MV.
2. VIS-V - The verification system. This provides facilities for combinational and sequential equivalence checking, fair CTL model checking, and cycle-based simulation.
3. VIS-S - The synthesis system. This provides state minimization, variable encoding, and hierarchical restructuring capabilities.

Figure 1: Components and packages of VIS. An edge from package A to B denotes that A depends on B (edges implied by transitivity are not shown).

Figure 1 is a block diagram showing how the three components interact. The packages that constitute each component are listed along with edges denoting dependencies among the packages. glu is the Generic Libraries Utility, which contains utility packages such as array, list, and bdd . Note that

• VIS-F does not depend on VIS-V or VIS-S, and
• VIS-V and VIS-S are independent.

The first point allows VIS to be easily compiled leaving out VIS-V, VIS-S, or both, to produce an executable containing a subset of the capabilities. The second point forces communication between verification and synthesis to occur via the front end, rather than directly.

The division of VIS into the three components is not reflected in the directory structure of the source code. Instead, all packages are kept within a single directory named src.