Cette thèse traite de la vérification automatique de composants matériels décrits en VHDL. C'est une étude de faisabilité d'un outil de vérification automatique qui réunit: exhaustivité, efficacité de calcul et simplicité d'utilisation. La méthodologie de l'interprétation abstraite a été adoptée: l'algorithme de simulation de VHDL est d'abord formalisé par une sémantique opérationnelle, de laquelle une analyse statique est dérivée de façon systématique par abstraction. L'analyse calcule un sur-ensemble des états accessibles. Le domaine numérique utilisé pour représenter les valeurs possibles des signaux de la description peut être choisi librement. Une instance possible de l'analyse a été implémenté en OCaml. Le domaine numérique choisi ici est celui des égalités linéaires entre variables booléennes. L'outil a permi de valider un code correcteur d'erreur de type Reed Solomon. Les performances sont excellentes, en particulier meilleures que celles du model checker à base de BDDs VIS.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00000875 |
| Date | 04 September 2004 |
| Creators | Hymans, Charles |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0015 seconds