Mise en œuvre de techniques de démonstration automatique pour la vérification formelle des NoCs

ISBN : 978-2-84813-152-8The current technology allows the integration on a single die of complex systems-on-chip (SoC's) composed of manufactured blocks (IP's) that can be interconnected through specialized networks-on-chip (NoCs). IP's have usually been validated by diverse techniques (simulation, test, formal verification) and the key problem remains the validation of the communication infrastructure. This thesis addresses the formal verification of NoCs by means of a mechanized proof tool, the ACL2 theorem prover. A meta-model for NoCs has been developed and implemented in ACL2. It satisfies generic correctness statements, which are logical consequences of a set of proof obligations for each one of the NoC constituents (topology, routing, switching technique,...). Thus the verification of a particular NoC instance is reduced to discharging this set of proof obligations. The purpose of this thesis is to extend this meta-model in several directions: more accurate timing modeling, flow control, priority mechanisms,... The methodology is demonstrated on realistic and state-of-the-art NoC designs: Spidergon (STMicroelectronics), Hermes (The Federal University of Rio Grande do Sul, Brazil, and LIRMM) , and Nostrum (Royal Institute Of Technology, Sweden) .Les technologies actuelles permettent l'intégration sur une même puce de systèmes complexes (SoCs) qui sont composés de blocs préconçus (IPs) pouvant être interconnectés grâce à un réseau sur la puce (NoCs). De manière générale, les IPs sont validés par diverses techniques (simulation, test, vérification formelle) et le problème majeur reste la validation des infrastructures des communications. Cette thèse se concentre sur la vérification formelle des réseaux sur puce à l'aide d'un outil de preuve automatique, le démonstrateur de théorèmes ACL2. Un méta-modèle pour les réseaux sur puce a été développé et implémenté dans ACL2. Il satisfait des propriétés de correction générique, conséquences logiques d'un ensemble d'obligations de preuve sur les constituants principaux du réseau (topologie, routage, technique de commutation,...). La preuve de correction pour une instance spécifique de réseau sur puce est alors réduite à la vérification de ces obligations de preuve. Cette thèse poursuit les travaux entrepris dans ce domaine en étendant ce méta-modèle dans plusieurs directions : prise en compte plus fine de la modélisation temporelle, du contrôle de flux, des mécanismes de priorités,... Les résultats sont démontrés sur plusieurs réseaux actuels : Hermes (Université fédérale du Rio Grande do Sul, Brésil et LIRMM) et Nostrum (Royal Institute Of Technology, Suéde)