A symbolic relation for a subset of VHDL'87 descriptions and its application to symbolic model checking

  • Emmanuelle Encrenaz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)


This paper presents the main principles for building a symbolic transition system from a description written in a subset of VHDL'87 (temporal information is excluded and objects are restricted to bit, bit_vector and Boolean types). This transition system is used for formal verification of the VHDL description. It consist of a system of Boolean equations indicating the next state of the system in terms of its current state. It is automatically generated from an intermediate representation of the VHDL description by means of a Petri Net. The deterministic nature of VHDL 87 and the exclusion of temporal elements in the description permit us to abstract the behavior of the system: only one state per delta cycle is represented instead of all intermediate states encountered in simulation. This abstraction reduces the size of the transition system and the cost of subsequent analysis. The construction of the system of Boolean equations from the Petri Net is presented first, and then an example of verification of a temporal logic property illustrates its use for Symbolic Model Checking. Experimental results are given which demonstrate the feasibility of this approach.


  1. [BCMDH90]
    J.R.Burch, E.M.Clarke, K.L. McMillan, D.L.Dill, L.H.Hwang, “Symbolic Model Checking: 1020 states and beyond”, Proc. 5th IEEE Symposium on Logic in Computer Science, 1990, pp 428–439.Google Scholar
  2. [BEC94]
    R.K.Bawa, E. Encrenaz, J.M. Couvreur, “VPN Technical Report”, technical report IBP-MASI 94-13, Apr.94.Google Scholar
  3. [BPS92]
    D.Borrione, L.Pierre, A.Salem,“PREVAIL: A proof environment for VHDL descriptions”,in Correct Hardware Design Methodologies, ed P.Camurati and P.Prinetto, North Holland 1992Google Scholar
  4. [Bryant86]
    R.E.Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, Transaction on Computers, Vol C-35, pp. 677–691, 1986.Google Scholar
  5. [CBM90]
    O. Coudert, C. Berthet, J-C. Madre, “Verification of sequential machines using functional vectors”, in International Workshop on Applied Formal Methods for Correct VLSI Design, volume VLSI Design Methods II, pp. 179–196, Belgium 1989. IFIP WG 10.2/ WG 10.5, North Holland 1990.Google Scholar
  6. [Clarke94]
    E. Clarke, “A VHDL subset for Model Checking”, CMU Internal Report, feb. 95.Google Scholar
  7. [DJ92]
    A. Debreil, D. Jaillet, “Synchronous description in VHDL for formal proof and resulting guidelines proposed by BULL”, Advanced Report, BULL Produits et Systèmes, Dpt Développements Assistés, Les Clayes sous Bois, France, Jul 1992. BULL/92.0001 rev.A.Google Scholar
  8. [BS-FD-K94]
    P.T.Breuer,L.Sanchez-Fernandez, C.Delgado-Kloos, “Proof Therory and a Validation Condition Generator for VHDL”, Proc of the EURO-DAC,Grenoble, 1994, pp 512–517.Google Scholar
  9. [BSCPB94]
    C.Bayol, B.Soulas, F.Corno, P.Prinetto, D.Borrione,“A Process Algebra Interpretation of a Verification Oriented Overlanguage of VHDL” Proc of the EURO-VHDL, Grenoble France 1994, pp. 506–511.Google Scholar
  10. [DB93]
    D.Déharbe,D.Borrione, “Symbolic Model Checking of VHDL Design Entities”, Technical Report of IMAG Institut, RR 925-I, dec 1993Google Scholar
  11. [DB95]
    D.Déharbe,D.Borrione,“A qualitative finite subset of VHDL and semantics”, Technical Report of IMAG Institut, RR 943-I, feb 1995Google Scholar
  12. [Döhmen94]
    G. Döhmen, “Petri Nets as Intermediate Representation between VHDL and Symbolic Transition Systems”, Proc of the EURO-VHDL, Grenoble France 1994, pp. 572–577.Google Scholar
  13. [DH95a]
    G.Döhmen, R.Herrmann, “A Deterministic Finite-State Model for VHDL”, Formal Semantics for VHDL, edited by C. Delgado Kloos and P.T. Breur, Universitad Politecnica de Madrid, Spain, feb 1995.Google Scholar
  14. [DH95b]
    G.Döhmen, R Herrmann, “Translating VHDL into functional symbolic finite-state models”, special issue of Formal Methods In System Design, D.Borrione Editor, Kluwer Academic Publisher. To appear in 1995.Google Scholar
  15. [ECB93]
    E. Encrenaz, J-M. Couvreur, R-K. Bawa, “Validation of VHDL systems based on Petri Net modeling”, in: Proc Workshop on Design Methodologies for Microelectronics and Signal Processing, Poland, 1993Google Scholar
  16. [EB95]
    E. Encrenaz, R-K. Bawa, “A Petri Net Model for Verifying Properties of VHDL programs”, Research Report MASI-IBP 95-07, Feb 95.Google Scholar
  17. [Long]
    D.E. Long, “A Binary Decision Diagram Package”, manual page.Google Scholar
  18. [McMillan93]
    K. Mc Millan, “Symbolic Model Checking”, Kluwer Academic Publisher, Norwell Massachusetts, 1993Google Scholar
  19. [Murata89]
    T.Murata, “Petri Nets: Properties, Analysis and Applications”. Proc IEEE, vol 77 nℴ4, apr 89, pp 541–580.Google Scholar
  20. [OC93]
    Olcoz — Colom, “A Petri Net Approach for the Analysis of VHDL Descriptions”, in: Proc of the CHARME 1993.Google Scholar
  21. [TSLBS-V90]
    H.J.Touati, H. Savoj, B. Lin, R.V. Brayton, A. Sangiovanni-Vincentelli,“Implicite State enumeration using bdd's”,Repot, University of California, Berkeley, USA, 1990.Google Scholar
  22. [vanTassel93]
    J.P. Van Tassel, “Femto-VHDL: The Semantics of a Subset of VHDL and its Embedding in the HOL Proof Assitant”, PhD Thesis, University of Cambridge, 1993.Google Scholar
  23. [VHDL'87]
    IEEE Standard VHDL Language Reference Manual” IEEE Std 1076–1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Emmanuelle Encrenaz
    • 1
  1. 1.Laboratoire MASI / IBPUniversité Pierre et Marie CurieParis Cedex 05France

Personalised recommendations