A Petri Net approach for the analysis of VHDL descriptions

  • S. Olcoz
  • J. M. Colom
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


In this paper we propose a methodology for the detection of some bad behaviours (e.g. deadlocks) in VHDL descriptions based on structural analysis techniques of Petri nets. The bad behaviours that we consider concern the execution control flow of a VHDL description. This methodology works in three steps. First, a formal description in Petri Net terms of the execution control flow of a VHDL description is realized. We present the basic rules to perform this translation. Second, a method to detect deadlocks using structural analysis techniques of Petri Nets based on structural invariants is applied. Finally, the information of the structural invariants allowing to decide the existence of a deadlock is used to fix the problem in VHDL terms.


Sequential Statement Formal Verification Kernel Process Simulation Cycle Reachability Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    P. Camurati, P. Prinetto: Formal verification of Hardware Correctness: Introduction and Survey of current Research. IEEE Computer, July 1988, pp 8–19.Google Scholar
  2. 2.
    M. Gordon: LCF-LSM. Technical Report N. 41, University of Cambridge (UK), 1984.Google Scholar
  3. 3.
    M. Sheeran: μFP, a Language for VLSI design. Proc. ACM Symposium on LISP and Functional Programming, Austin, Texas (USA), 1984.Google Scholar
  4. 4.
    R. Boute: System Semantics: principles, applications and implementation. ACM Transaction on Programming Languages and Systems, Vol. 10, N. 1, January 1988.Google Scholar
  5. 5.
    A. Bartsch et al.: LOVERT — A logic verifier of Register—Transfer Descriptions. Proc. IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Houthalen (Belgium), November 13–16, 1989.Google Scholar
  6. 6.
    R. Piloty et al.:CONLAN Report, Springer Verlag, 1983.Google Scholar
  7. 7.
    J. Vantassel et al.: Toward a formal verification of VHDL specifications. Proc. IFIP W.G. 10.2 International Workshop on Applied Formal Methods for Correct VLSI Design, Houthalen (Belgium), November 13–16, 1989.Google Scholar
  8. 8.
    IEEE Standard VHDL Language Reference Manual, IEEE, Inc. New York, NY, March, 1988.Google Scholar
  9. 9.
    T. Murata: Petri nets: properties, analysis, and applications. Proceedings of the IEEE, Vol. 77, No. 4, April 1989, pp 541–580.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • S. Olcoz
    • 1
  • J. M. Colom
    • 1
  1. 1.TGI S.A.MadridSpain

Personalised recommendations