Formal verification of VHDL: the model checker CV
David Déharbe, Subash Shankar, E. M. Clarke · 1998
. 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. ? This research is sponsored by the Semiconductor Research Corporation (SRC) under Contract No. 97-DJ-294, the National Science Foundation (NSF) under Grant No. CCR-9505472, and the Defense Advanced Research Projects Agency (DARPA) under Contract No. DABT63-96-C-0071. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of SRC, NSF, DARPA, or the United States Government. ?? Contact author. Partly supported by Projeto Nordeste (CAPES-FUNPEC) and CNPq. 1