Rajesh K. Bawa, E. Encrenaz Expressing and Verifying Properties of VHDL Programs Nous proposons une méthode de vérification de systèmes décrits en VHDL. Cette approche repose sur la vérification symbolique de propriétés logico-temporelles. Un système de transitions symbol­ ique représenté sous forme de BDD est extrait d'une description VHDL. Les propriétés à vérifier sont exprimées dans un environ­ nement associant la syntaxe de VHDL et de CTL. In this paper we propose a method for design verification based on Symbolic Model Checking. A symbolic transition system, based on BDD representation, is derived from a VHDL description and properties expressed in a mixed environment of VHDL and CTL are used for formal verification of VHDL systems.