Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Cited literature [81 references]  Display  Hide  Download
Contributor : Ecole Polytechnique Connect in order to contact the contributor
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


  • HAL Id : pastel-00000875, version 1



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



Record views


Files downloads