VIS : A System for Verification and Synthesis
- Robert K. Brayton ,
- Gary D. Hachtel ,
- Alberto Sangiovanni-Vincentelli ,
- Fabio Somenziy ,
- 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 ,
- Tiziano Villa
Proceedings of the 8th International Conference in Computer-Aided Verification |
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.