Verification of VHDL descriptions by abstract interpretation.
Vérification de descriptions VHDL par interprétation abstraite.
Résumé
the static analysis then derives systematically by abstraction from this semantics. The analysis computes an over-approximation of the reachable states. To represent the possible values of signals any numerical domain may be freely chosen. This allows for distinct efficiency/precision trade-offs. We present the implementation of a possible instantiation of the analysis. It uses the numerical domain of linear equalities between boolean variables. This prototype was able to validate a Reed Solomon error correcting code. It shows excellent performances and in particular outperforms the BDD-based model checker VIS.
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.
Loading...