LIP6 2000/029

• Reports
  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 - 12/06/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
This document presents an adaptation of Data Decision Diagrams (DDD or D3 for short), proposed by LABRI (Bordeaux I University), for the representation of VHDL programs using boolean and integer variables. The paper describes the D3 model we defined, its interpretation for the representation of sets of states and transiton relations, and the main symbolic state space traversals based on this structure.
• Keywords : BDD, symbolic verification, VHDL programs, boolean and integer variables
• Publisher : Emmanuelle.Encrenaz (at) nulllip6.fr