E. Encrenaz A Symbolic Transition System for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking Nous présentons une approche pour extraire un système de transi­ tions symbolique d'une description écrite en un sous-ensemble de VHDL'87 (les instrustions faisant référence au temps sont ex­ clues, et les objets manipulés sont de type booléen, bit ou bit- vector). Ce système de transitions symbolique peut être utilisé pour la vérification formelle de propriétés de descriptions VHDL (Vérification Symbolique de Modèle, appelée couramment Symbolic Model Checking, ou Équivalence d'Automates). Il consiste en un système d'équations booléennes indicant l'état futur du système en fonction de son état courant. Il est automatiquement construit à partir d'une représentation formelle de la description VHDL en réseaux de Petri. Le déterminisme intrinsèque de VHDL'87 et l'exclusion des descriptions VHDL, permet d'abstraire le com­ portement du système, réduisant la taille du système de transi­ tions et par là même, le coût de la vérification formelle qui s'ensuit. La construction du système d'équations à partir du réseau de Petri intermédiaire est d'abord présentée, puis un ex­ emple de vérification de propriété logico-temporelle illustre l'utilisation d'un tel système pour la Vérification Symbolique de Modèle. Les résultats expérimentaux présentés démontrent la fais­ abilité de l'approche. 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 re­ stricted 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 automat­ ically 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 which reduces the cost of subsequent analy­ sis. 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.