Verification of circuits described in VHDL through extraction of design intent

Verification of an implementation against its specification in the design hierarchy is of paramount importance and becomes increasingly difficult with the size and complexity of the circuit. We present a comprehensive verification framework (VEHICLE) which integrates a BDD package with theorem-proving techniques, and requires minimal user interaction. VEHICLE can verify VHDL designs from the scheduled behavioral level down to the gate level by capturing the design intent, on the basis of a formal semantics, in a form appropriate for input to the verifier. Results are given for the verification of several example circuits