Formal verification of VHDL: the model checker CV

This article describes a prototype formal verification system for a subset of VHDL. The behavior of a VHDL design can be specified with temporal logic formulas and be verified with an algorithm called symbolic model checking. The model checker applies a number of new techniques to handle larger designs, thus allowing for efficient verification of real circuits. We have completed an initial release of the VHDL model checker and have used it to verify complex circuits, including the control logic of a commercial RISC microprocessor