CV: Introduction

CV is a toolset for the verification of VHDL descriptions, using a formal technique called "symbolic model checking". This technique makes it possible to verify completely automatically properties of a design. CV is actually best suited for verifying controllers. It has been successfully used to verify properties of an industrial description (a microprocessor controller) in less than five minutes.

The different programs of CV and their interaction in a verification flow are sketched in the following figure:

Verification flow with CV programs

is a standalone VHDL compiler. It takes as input a text file containing a VHDL description and produces VHDL library units in the working library.
is the model checker itself. It takes as input a specification file, loads the corresponding VHDL library unit, and produces a yes or no answer. If the specification is not satisfied by the VHDL description, a VHDL testbench exhibiting the faulty behavior is generated.

In addition to these two programs, CV also includes:

Main Sections: Introduction   Installation   Documentation   Examples

CV / Carnegie Mellon University / / Revised December 1996