Méthodes de vérification de circuits digitaux - Université de Lorraine Accéder directement au contenu
Thèse Année : 1994

Verification methods for digital circuits

Méthodes de vérification de circuits digitaux

Stefan Krischer
  • Fonction : Auteur
  • PersonId : 756549
  • IdRef : 18925064X

Résumé

not available
Cette thèse propose des outils pour la vérification formelle de la correction de circuits matériels. Pour la vérification de la correction d'un circuit combinatoire par rapport a sa spécification, une nouvelle méthode pour spécifier des fonctions booléennes est présentée, les systèmes de réécriture booléens (BTRS), puis une transformation d'un BTRS en deux expressions booléennes est décrite qui permet de vérifier la correction, la complétude et la cohérence d'une spécification par rapport a une implémentation. Pour la vérification de circuits séquentiels, deux nouveaux algorithmes qui décident l'équivalence et l'inclusion de deux machines de mealy sont introduits. Ces problèmes de décision peuvent aussi être vus comme cas spécifiques de la vérification d'un invariant d'une machine, a savoir la machine produit. Un survol uniforme et généralise sur les méthodes d'itération de point fixe décrit l'analyse de l'atteignabilité d'une machine et le test de la non-atteignabilité d'un ensemble d'états. Ces algorithmes de test d'équivalence et d'inclusion sont implémentes dans le logiciel fancy. Finalement, les applications en preuve de circuits des démonstrateurs de théorèmes généraux sont explorées. Une méthode de description et de preuve des circuits paramètres combinatoires ou séquentiels par des systèmes de réécriture est présentée. Différentes sortes de preuves qui ont besoin de telles descriptions sont montrées: par réécriture (prouveurs lp ou reve), par induction (lp), par consistance (reve), par des ensembles tests (spike)
Fichier non déposé

Dates et versions

tel-01751838 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01751838 , version 1

Accès intranet

Citer

Stefan Krischer. Méthodes de vérification de circuits digitaux. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 1994. Français. ⟨NNT : 1994INPL043N⟩. ⟨tel-01751838⟩
44 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More