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:
  • 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 from SIS.
Each of these can be executed interactively from any point in the design hierarchy.

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

VIS Homepage

Comments, suggestions, complaints can be addressed to vis-users@colorado.edu
©2002-2018 U.C. Regents