Concluding Remarks

We have described VIS, a verification and synthesis tool, which offers a better programming environment, new capabilities, and improved performance over existing verification tools. VIS has been implemented in the C programming language, and it has been ported to many different operating systems and architectures. We have tested VIS on the sequential circuits from the ISCAS benchmark set and some industrial designs.

One of the key goals of VIS is to serve as a platform for developing new verification algorithms. We have used the object-oriented programming style of SIS as our paradigm. VIS is composed of 18 packages; each exports a set of routines for manipulating a particular data structure, or for performing a set of related functions (e.g., there are packages for model checking, variable ordering, and manipulating the network data structure). New packages can be added easily. This wealth of exported functions can be used by future programmers to quickly assemble new algorithms. All functions adhere to a common naming convention so that it is easy to find functions in the documentation.

For more information about VIS or to get a copy, visit the VIS home page [ 5 ].