This document introduces VIS (Verification Interacting with Synthesis). We describe what VIS is, what it can do, how to write limited Verilog code for its input, its commands, and an extended example for the new user. For more details, see the VIS home page http://www-cad.eecs.berkeley.edu/ Respep/Research/vis/doc/packages/index.html.
VIS is a verification and synthesis system for finite-state hardware systems, which is being developed at Berkeley and Boulder. It improves upon first generation tools like HSIS and SMV by:
Many first generation tools for automatic formal verification were based on two theoretical approaches. The first is temporal logic model checking, where the properties to be checked are expressed as formulas in a temporal logic, and the system is expressed as a finite state system. In particular, Computational Tree Logic (CTL) model checking is a technique pioneered by Clarke and Emerson to verify whether a finite state system satisfies properties expressed as formulas in a branching-time temporal logic called CTL. SMV, a system developed at CMU, belongs to this class of tools.
Certain properties are not expressible in CTL, but they can be expressed
as 
-automata. The second approach, language containment, requires the description
of the system and properties as
-automata, and verifies correctness by checking that the language of the
system is contained in the language of the property. Note that certain types
of CTL properties involving existential quantification are not expressible
by
-automata. COSPAN, a system developed at Bell Labs, offers language containment.
A combination of both approaches is offered by the HSIS [6] system, which was developed at the University of California, Berkeley. Our experience with verification tools (in particular HSIS) led to the conclusion that sometimes, the simpler and more limited the approach, the more efficient it can be. A number of design decisions that we made for HSIS made it unacceptably slow for some large examples. With these problems in mind, we set about writing a tool that was more efficient, easily extendible, and offered a good programming environment, in order that it can be more easily upgraded in the future as more efficient algorithms are developed.
VIS also has the capability to interface with SIS to optimize logic modules; hence, VIS is an integrated system for hierarchical synthesis, as well as verification. We plan to pursue research on the interaction between verification and synthesis in the future; hence the name VIS, verification interacting with synthesis.
Fig. 1.1 presents of an overview of VIS.
Figure 1.1:
Block diagram of VIS.
VIS has three main parts: a front-end to read and traverse a hierarchical system described in BLIF-MV, which may have been compiled from a high-level language like Verilog; a verification core, VIS-v, to perform model checking of Fair CTL and test language emptiness; and a path to SIS, VIS-s, to optimize parts of the logic.
We decided to offer limited but efficient capabilities. We felt that in the future, it would be easy to add more features, as they are required, using a well defined programming interface. In line with this keep it simple philosophy, VIS provides the following verification capabilities.
VIS can interact with SIS to assist the task of verification by simplifying parts of the system. Another objective is to support a full-fledged hierarchical synthesis flow, that translates a Verilog description into an optimized multi-level circuit at the gate level. Unlike existing logic optimization systems like SIS, VIS can support hierarchical synthesis.