Skip to Main content Skip to Navigation
Theses

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

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.
Document type :
Theses
Complete list of metadatas

Cited literature [81 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00000875
Contributor : Ecole Polytechnique <>
Submitted on : Friday, July 23, 2010 - 10:01:05 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:26 PM
Long-term archiving on: : Monday, October 25, 2010 - 10:57:52 AM

Identifiers

  • HAL Id : pastel-00000875, version 1

Collections

Citation

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

Share

Metrics

Record views

614

Files downloads

731