Note publique d'information : 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).
Note publique d'information : The 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) .
paprika.idref.fr
data.idref.fr
Documentation
