LIP6 2000/029

• Rapports de recherche
  Extension des diagrammes de décisions binaires pour la représentation de programmes VHDL en vue de leur vérification
• G. Decuq, E. Encrenaz-Tiphène
• 23 pages - 06/12/2000- document en - http://www.lip6.fr/lip6/reports/2000/lip6.2000.029.ps.gz - 315 Ko
• Contact : Emmanuelle.Encrenaz (at) nulllip6.fr
• Ancien Thème : ANP
Ce document présente une adaptation des diagrammes de décisions de données (DDD ou D3), développés au LABRI, pour la représentation de programmes VHDL utilisant des variables booléennes et entières. Il décrit le modèle des D3 utilisés, leur interprétation pour la représentation d'ensembles d'états et de relations de transitions, ainsi que les principaux algorithmes de parcours d'espace d'états nécessaires à la vérification par model-checking.
• Mots clés : BDD, vérification symbolique, programmes VHDL, variables booléennes et entières
• Directeur de la publication : Emmanuelle.Encrenaz (at) nulllip6.fr