Prevail-dm : a framework-based environment for formal hardware verification

Abstract

This report describes the framework-based PREVAIL-DM design environment for formal hardware verification. PREVAIL-DM integrates proof tools that are available in the PREVAIL environment around a common, VHDL-based conceptual schema. Tools are encapsulated according to a black-box approach. Design data are stored in a uni que data base, and the environment o:ffers a common main user interface, which gives access to design tools and methods and allows browsing through the database objects. Available methods to be applied on the design objects are oriented to the application semantics, thus helping to maintain ali desired schema-related integrity constraints. PREVAIL-DM is implemented upon the Cadlab framework and uses most of its main features.

Ce rapport présente l'environnement de projet PREVAIL-DM, orienté vers la preuve de circuits et systemes éler.troniques et basé sur un framework. PREVAIL-DM integre des outils de preuve disponibles dans l'environnement PREVAIL autour d'un schéma conceptuel de données commun et basé sur VHDL. Les outils sont encapsulés selon une approche black-box. Les objds de projet sont stockés dans une base de données unique, et l'environnement o:ffre une interface-usager communne qui permet l'acces à tous les outils ainsi que la navigation à tr<'l.vers la base de données. Les méthodes qui sont exécutables sur les objets de projet sont orientées vers la sémantique de l'application, de façon à aider l'usager à préserver toutes les contraintes d'intégrité liées au schéma. PREVAIL-DM est réalisé en utilisant le framework Cadlab comme plateforme et se sert de la plupart de ses plus importants services.