Verification of VHDL descriptions by abstract interpretation. - Archive ouverte HAL Access content directly
Theses Year : 2004

Verification of VHDL descriptions by abstract interpretation.

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

(1)
1

Abstract

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.
Fichier principal
Vignette du fichier
Hymans.pdf (678.75 Ko) Télécharger le fichier
Loading...

Dates and versions

pastel-00000875 , version 1 (23-07-2010)

Identifiers

  • HAL Id : pastel-00000875 , version 1

Cite

Charles Hymans. Vérification de descriptions VHDL par interprétation abstraite.. Analyse classique [math.CA]. Ecole Polytechnique X, 2004. Français. ⟨NNT : ⟩. ⟨pastel-00000875⟩
366 View
589 Download

Share

Gmail Facebook Twitter LinkedIn More