In: Milne, George J.; Pierre, Laurence: Lecture Notes in Computer Science, Vol. 683; Correct Hardware Design and Verification Methods, pages 15-26. Berlin: Springer-Verlag, 1993.
Abstract: 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.