Return to search

Construction de Modèles Réduits et Vérification Symbolique de Circuits Industriels décrits au Niveau RTL

La vérification symbolique de systèmes matériels est limitée par la complexité exponentielle en taille de représentation du modèle symbolique sous-jacent. <br />Ce travail porte sur la réduction, manuelle ou non, de ce modèle. Les approches compositionnelles structurelles et comportementales ont été étudiées dans un contexte industriel. Cette étude a précédé le développement d'une nouvelle technique de réduction : la partition fonctionnelle. Cette technique s'applique aux systèmes dont le comportement est séquentiellement décomposable. La partition fonctionnelle est mise en place grâce à une étape préliminaire de simulation symbolique. Elle a été implémentée et appliquée sur un circuit industriel de taille importante, et a permis d'obtenir d'excellents résultats en matière de réduction. L'expérimentation des techniques de preuve présentées s'est appuyée sur un outil d'extraction de machines d'états finis à partir de descriptions VHDL qu'il a été nécessaire de mettre en œuvre.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00003667
Date07 October 2003
CreatorsDumitrescu, E.
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0017 seconds