Abstract FR:

La verification formelle de circuits integres garantit de facon rigoureuse leur fiabilite. Pour ce faire, les assistants de preuve sont de plus en plus utilises. Le systeme coq, base sur le calcul des constructions inductives avec types co-inductifs, presente des particularites interessantes et originales. Nous etudions ce que ce systeme peut apporter dans le domaine de la specification et de la verification de circuits. Apres avoir montre l'interet des types dependants pour donner des specifications de circuits precises et donc fiables, nous utilisons le mecanisme d'extraction coq pour synthetiser un circuit correct par construction. Nous illustrons ces aspects sur des circuits combinatoires dont l'architecture est lineaire et nous etudions sur cet exemple les diverses strategies de preuve qu'offre coq. Notre etude porte ensuite sur les circuits sequentiels synchrones specifies a l'aide de types co-inductifs. Ces types permettent de definir en coq des objets infinis comme les streams. Les structures et les comportements des circuits sont modelises de facon uniforme par des automates, eux-memes caracterises par des fonctions co-recursives sur les streams. Notre approche est hierarchique et modulaire et repose sur un lemme general qui exprime une equivalence entre deux streams issues respectivement de deux automates. Ce lemme prend en compte l'essentiel de l'aspect temporel de nos preuves de correction. Nous appliquons ensuite cette methodologie a un circuit reel, le fairisle atm switch element.