Return to search

Vérification de descriptions VHDL par interprétation abstraite.

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.

Identiferoai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00000875
Date04 September 2004
CreatorsHymans, Charles
PublisherEcole Polytechnique X
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0021 seconds