Laurent Arditi's PhD

Spécification et Preuve des Microprocesseurs

Laurent Arditi

Thèse de Doctorat de l'Université de Nice - Sophia Antipolis.

Soutenue le 31 Octobre 1996 devant le jury composé de :

• Michel Rueher (président), professeur à l'UNSA,
• Francois Anceau (rapporteur), professeur au CNAM,
• Dominique Borrione (rapporteur), professeur au TIMA-UJF,
• Jacques Chazarain (directeur), professeur à l'UNSA,
• Hélène Collavizza (directeur), maître de conférences à l'UNSA,
• Fernand Boeri (examinateur), professeur à l'UNSA,
• Paolo Camurati (examinateur), professeur au Politecnico di Torino,
• Gilles Kahn (examinateur), directeur de recherche à l'INRIA

Version PDF ou postscript du manuscript

Version PDF ou postscript des transparents

Résumé

La complexité des processeurs actuels pose des problèmes de validation. L'utilisation de méthodes formelles est de ce point de vue une approche intéressante. Le travail présenté dans cette thèse s'inscrit dans ce cadre. Une méthodologie de spécification et de preuve des microprocesseurs à haut niveau d'abstraction y est proposée. Son but est de permettre la vérification formelle de l'équivalence entre d'une part une implémentation au niveau transfert de registres d'un processeur, et d'une autre part une spécification au niveau du langage assembleur. La première partie décrit le modèle de spécification choisi : quelque soit le niveau d'abstraction considéré, un processeur est représenté par un interprète. Ce modèle est implémenté en suivant une approche orientée-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'équivalence entre deux interprètes. La technique de base est l'exécution symbolique couplée à un système de calcul formel dédié : CALCULF. Les preuves sont ainsi totalement automatiques et rapides. Nous montrons dans la troisième partie que certaines instructions, dites de boucle, ne peuvent pas être vérifiées par la technique précédente. Pour résoudre ce problème, nous proposons une extension des diagrammes de moments binaires (*BMDs) en vue de vérifier certaines instructions arithmétiques. Quand une preuve inductive est nécessaire, l'assistant de preuve COQ est utilisé. Le système SVP regroupe tous les outils ainsi développés. Il a permis la vérification de plusieurs processeurs et instructions de boucles.

Mots-clés : spécification, vérification formelle, preuve, processeur, exécution symbolique, démonstrateur de théorèmes, Coq, BMD, SVP, VHDL.

Microprocessor Specification and Proof

Abstract

We propose in this thesis a methodology for the specification of processors and different proof techniques. This work applies to abstract levels of processors: from the ``register transfer level'' up to the assembly language level. The first part of this thesis describes our specification model: a processor is modeled by an interpreter at all abstraction levels. This model is implemented using an object-oriented approach. The language FHSL is the interface between the user, because it is close to a VHDL subset, and the proof systems. The second part concerns the proof of equivalence between two interpreters. The main technique is symbolic execution aided by a dedicated computer algebra system: CALCULF. Using this technique, proofs are completely automatic and efficient. We show in the third part that this proof method does not apply for verifying some ``looping'' instructions. We propose an extension of Binary Moment Diagrams (*BMDs) to verify some arithmetic instructions. When an inductive proof is needed, the COQ proof assistant is used. We developed the system SVP using these specification and verification methodologies. It has been used to verify several processors and some looping instructions.

Key-words: specification, formal verification, proof, processor, symbolic execution, theorem prover, Coq, BMD, SVP, VHDL.