What is VIS?
VIS (Verification Interacting with Synthesis) is a system for formal
verification, synthesis, and simulation of finite state systems. It
has been developed jointly at the University of California at Berkeley,
the University of Colorado at Boulder, and more recently at
the University of Texas, Austin.
Verification is the process of checking if "what was designed is what
was originally specified". While the traditional and most common
method of verification is through simulation, recently,
interest has increased in methods of formal verification,
such as language containment and temporal logic
model checking. VIS is able to synthesize finite state systems and/or
verify properties of such systems, which have been specified
hierarchically as a collection of interacting finite state machines.
VIS provides the following features:
Each of these can be executed interactively from any point in the
- Simulation of logic circuits (proof of concept only).
- Formal "implementation" verification of combinational and sequential
circuits (proof of concept only).
- State-of-the-art formal "design" verification using fair CTL model
checking and language emptiness.
- Logic synthesis via hierarchy restructuring and a path to and
A Verilog HDL front end, vl2mv, is also provided, which compiles a subset
of Verilog into an intermediate format BLIF-MV.
VIS improves upon first generation tools by:
- providing a better programming environment,
- providing new capabilities, and
- improving performance in many cases.
Email to the VIS group
Last Updated 961205
Comments, suggestions, complaints can be addressed to