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:

cva

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.

cvc

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:

• libcv.a, a C library defining the format of library units and functions to access them (cvc and cva have both been developed with this library);
• (small) examples of VHDL code and their specifications;
• additional documentation, in HTML and/or man page format.

Main Sections: Introduction   Installation   Documentation   Examples