VIS : A System for Verification and Synthesis
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-Vincentelli,
Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen Edwards, Sunil Khatri,
Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary,
Thomas R. Shiple, Gitanjali Swamy, and Tiziano Villa
Eight Conference on Computer Aided Verification (CAV'96), LNCS 1102,
pp. 428-432, June 1996.
Abstract
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.
We designed VIS 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:
- providing a better programming environment,
- providing new capabilities, and
- improving performance in some cases.
We have incorporated software engineering methods into the
design of VIS. In particular, we provide extensive documentation that
is automatically extracted from the source files for browsing on the
World Wide Web.
Section 2 describes the major capabilities of VIS as seen by the user,
and Section 3 gives a brief description of the underlying algorithms
of these capabilities. Section 4 discusses the VIS programming
environment, and Section 5 gives conclusions and ideas for future
work.
Click here to download the compressed
postscript version.
BibTeX Entry
@InCollection{VIS96,
author = {R. K. Brayton and others},
title = {VIS: A system for verification and synthesis},
booktitle = {Eigth Conference on Computer Aided Verification (CAV'96)},
publisher = {Springer-Verlag},
year = 1996,
editor = {T. Henzinger and R. Alur},
address = {Rutgers University},
pages = {428-432},
note = {LNCS 1102}
}
Return to the home page