Abstract FR:

La complexite des processeurs actuels pose des problemes de validation. L'utilisation de methodes formelles est de ce point de vue une approche interessante. Le travail presente dans cette these s'inscrit dans ce cadre. Une methodologie de specification et de preuve des microprocesseurs a haut niveau d'abstraction y est proposee. Son but est de permettre la verification formelle de l'equivalence entre d'une part une implementation au niveau transfert de registre d'un processeur, et d'une autre part une specification au niveau du langage assembleur. La premiere partie decrit le modele de specification choisi: quelque soit le niveau d'abstraction considere, un processeur est represente par un interprete. Ce modele est implemente en suivant une approche orientee-objet. Le langage fhsl, proche de vhdl, offre une interface entre l'utilisateur et les outils de preuve. La seconde partie traite de la preuve de l'equivalence entre deux interpretes. La technique de base est l'execution symbolique couplee a un systeme de calcul formel dedie: calculf. Les preuves sont ainsi totalement automatiques et rapides. Nous montrons dans la troisieme partie que certaines instructions, dites de boucle, ne peuvent pas etre verifiees par la technique precedente. Pour resoudre ce probleme, nous proposons une extension des diagrammes de moments binaires (*bmds) en vue de verifier certaines instructions arithmetiques. Quand une preuve inductive est necessaire, l'assistant de preuve coq est utilise. Le systeme svp regroupe tous les outils ainsi developpes. Il a permis la verification de plusieurs processeurs et instructions de boucle