Pour satisfaire la demande du marché actuel, plusieurs outils commerciaux de vérification formelle sont apparus ces dernières années. Le niveau le plus abstrait de description accepté dans la plupart de ces outils est le niveau appelé transfert de registres, c'est-à-dire une description avec des cycles d'horloge explicitement définis. Pour rester compétitifs, néanmoins, les concepteurs sont obligés d'élever le niveau d'abstraction et commencent à utiliser des outils de synthèse de haut niveau. Cette thèse a pour objet la vérification formelle des résultats de synthèse de haut niveau par rapport à la spécification initiale décrite en VHDL. Nous proposons une méthodologie de vérification qui épouse le flot de conception et consiste en la vérification de deux étapes principales:<br />l'ordonnancement et l'allocation. La vérification de chaque étape est fondée sur un modèle de machine abstraite que nous avons défini: contrairement au modèle de machine d'états finis classique, il réduit<br />considérablement l'espace d'états d'où les registres de la partie opérative sont exclus. En outre, la machine abstraite est similaire aux descriptions VHDL utilisées lors de la synthèse et offre, par conséquent, un niveau d'abstraction plus élevé de représentation des<br />circuits. La preuve d'équivalence entre la machine abstraite et la machine d'états finis classique justifie la première et constitue une des contributions théoriques de la thèse. Un prototype d'outil basé sur la simulation symbolique a été développé et exécuté sur des benchmarks de la synthèse comportementale. La thèse<br />s'achève sur les problèmes ouverts et les axes de recherche à explorer.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00003009 |
| Date | 10 October 1999 |
| Creators | Dushina, J. |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds