HDL-based integration of formal methods and CAD tools in the PREVAIL environment

We present an open environment for the integration of formal methods applied to HDL descriptions of circuits. The system currently accepts SMAX[4] and VHDL, and provides equivalence checking, model checking, theorem proving, and automatic diagnosis of simple design errors. After an overview of the system, we discuss the salient features of the common intermediate format, of the diagnosis tools, and of the automatic generation of NQTHM[11] models from VHDL functional descriptions.