Abstract FR:

Ce document presente une approche pour la conception de circuits, se basant sur le langage flot de donnees synchrone signal et le langage de description de materiel vhdl. Deux aspects sont importants pour la conception d'architectures: la synthese et la verification formelle. La synthese permet d'obtenir a partir d'une description abstraite une architecture materielle par des transformations automatiques. La verification formelle, quant a elle, permet d'etablir qu'une abstraction et une mise en uvre sont conformes via-a-vis d'un certain critere. Une partie est consacree a la synthese de circuits a partir de signal, et ceci en s'appuyant sur une traduction vers vhdl qui dispose de nombreux outils de synthese. Une methode pour la synthese de circuits globalement asynchrones localement synchrones est definie. Ce type d'architecture permet d'allier les avantages des circuits synchrones et des circuits asynchrones. Dans la deuxieme partie consacree a la verification formelle, une definition d'un sous-ensemble vhdl en signal est donnee en prelude a la verification des programmes vhdl dans l'environnement signal. Un sous-ensemble synchrone de vhdl est utilise pour la verification formelle a l'aide de l'outil de preuve associe a signal