This article describes a prototype implementation of a symbolic model checker for a subset of VHDL. The model checker applies
a number of techniques to reduce the search space, 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.