Avec la complexité croissante des circuits VLSI, la recherche de méthodes formelles de conception de circuits devient nécessaire pour atteindre l'objectif de circuits zéro-défaut dans les délais escomptés. Dans le cadre des circuits digitaux synchrones, nous proposons une méthodologie de conception de circuits descendante par transformations de programmes. La transformation de programmes consiste à dériver une réalisation à partir de sa spécification comportementale de haut niveau. La synthèse de circuits par transformations de programmes qualifie ce processus de réalisation. Pour cela, nous avons choisi deux langages: l'un pour spécifier le comportement d'un circuit et l'autre pour décrire sa réalisation. Ces deux langages sont des sous-langages du langage purement fonctionnel Miranda. Un circuit digital est spécifié à un niveau comportemental pur. Chaque transformation produit une nouvelle description, équivalente à celle de départ. A une certaine étape des transformations, la forme de la spécification prend un sens en termes de circuit. Cette forme est obtenue par application de transformations particulières que sont le schéma d'introduction de flots ou le théorème de réalisation. Les transformations suivantes ont pour but d'optimiser le circuit. Une réalisation de circuit ainsi obtenue est correcte par construction. Une preuve a posteriori n'est donc pas nécessaire. La première partie de cette thèse présente une étude bibliographique des recherches qui ont été effectuées dans le domaine de la conception de circuits digitaux zéro défaut. La seconde partie propose une méthodologie de conception de circuits digitaux synchrones, un langage de description de circuits, des schémas de transformations et une stratégie de leur application. Enfin un ensemble d'exemples de synthèse de circuits est donné.