Introduction to VIS

VIS (Verification Interacting with Synthesis) is a tool that integrates the verification, simulation, and synthesis of finite-state hardware systems. It uses a Verilog front end and supports fair CTL model checking, language emptiness checking, combinational and sequential equivalence checking, cycle-based simulation, and hierarchical synthesis.

VIS was designed to maximize performance by using state-of-the-art algorithms, and to provide a solid platform for future research in formal verification. VIS improves upon existing verification tools by:

1.

providing a better programming environment,

2.

providing new capabilities, and

3.

improving performance in some cases.

In addition, software engineering methods were used in the design of VIS in order to encourage further development by a diverse set of researchers. In particular, we provide extensive documentation that is automatically extracted from the source files for browsing on the World Wide Web.

In this tutorial, we will briefly describe each of the capabilities built into VIS and then concentrate on how to use and control VIS to make maximum use of its potential.