Vérification formelle de systèmes digitaux synchrones, basée sur la simulation symbolique
Pour satisfaire les exigences du marché, les outils de vérification formelle doivent permettre aux concepteurs de vérifier des descriptions complexes et de raisonner sur des domaines de valeurs grands ou infinis. Il est nécessaire de se concentrer sur la correction d'algorithmes et sur les prop...
| Main Author: | |
|---|---|
| Language: | FRE |
| Published: |
2001
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00002931 http://tel.archives-ouvertes.fr/docs/00/04/53/73/PDF/tel-00002931.pdf |
| Summary: | Pour satisfaire les exigences du marché, les outils de vérification formelle doivent permettre aux concepteurs de vérifier des descriptions complexes et de raisonner sur des domaines de valeurs grands ou infinis. Il est nécessaire de se concentrer sur la correction d'algorithmes et sur les propriétés mathématiques essentielles des blocks à concevoir. La plupart des outils de vérification formelle comme les "Model-checkers" sont restrictifs car ils ne peuvent travailler avec des niveaux plus haut que le "RTL", et ils sont également limités sur le nombre total d'états. Les démonstrateurs de théorèmes ne souffrent pas de ces restrictions, mais ne sont pas automatiques et requièrent des méthodes pour faciliter leur utilisation systématique. Cette thèse aborde la vérification formelle de descriptions VHDL au moyen du démonstrateur ACL2. Nous proposons un environnement combinant simulation symbolique et démonstrateur de théorèmes pour l'analyse formelle de descriptions de haut niveau d'abstraction. Plus précisément, notre approche consiste à développer des méthodes<br />- pour formaliser un sous-ensemble de VHDL,<br />- pour "diriger" le démonstrateur pour effectuer de la simulation symbolique<br />- pour utiliser ces résultats pour les preuves.<br />Un outil a été développé combinant des traducteurs (VHDL vers ACL2), des moteurs de simulation symbolique et de preuves, et une interface utilisateur. Les définitions et les théorèmes sont générés automatiquement. Un même modèle généré est ainsi utilisé pour toutes les tâches. Nous aspirons à fournir au concepteur une méthodologie pour insérer la vérification formelle le plus tôt possible dans le cycle de conception. Le démonstrateur est utilisé pour des manipulations symboliques et pour prouver qu'ils sont équivalents à une fonction spécifiée. Le résultat de cette thèse est de rendre la technique de démonstration de théorèmes acceptable dans une équipe de concepteur du point de vue de la facilité d'utilisation, et de diminuer le temps de vérification. |
|---|