A framework-based realization of an environment for formal hardware verification

The framework-based realization of the PREVAIL-DM design environment, oriented for formal hardware verification, is discussed. PREVAIL-DM integrates proof tools around a coarse-grain conceptual schema based on VHDL. Tools are integrated according to a black-box approach. Methods to be applied on the design objects are oriented to the application semantics and maintain schema-related integrity constraints. PREVAIL-DM is implemented on the Cadlab framework and uses most of its main features. The use of framework facilities in the implementation of the environment, and specially the aspects of data modeling, total integration, consistency checking, and access management, are discussed