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:
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.