Formal Verification of VHDL Models

The goal of this project is to create tools to support the formal verification of VHDL designs. Two existing formal verification tools will be enhanced to support VHDL. The first, Spectool, will allow a class of designs, the synchronous finite-state controlled systems, to be specified and verified and then translated into VHDL. This capability will allow VHDL to be used as an interface between Spectool, which has been used to verify several large designs, and other CAD tools. The second tool, Penelope, will be enhanced to allow specification and verification of arbitrary VHDL designs. Phase I will complete the enhancement of Spectool to allow translation of verified designs into VHDL. Examples will be worked using the enhanced tool and will guide the development of the VHDL interface language to be used in the VHDL-enhanced Penelope. Penelope will be enhanced to support the core language constructs of VHDL, laying a foundation for the Phase II effort. In Phase II of the project, the VHDL- enhanced Penelope system will be completed to support all of VHDL and integrated with the Ada part of Penelope so that mixed hardware/software systems can be verified.