Publications

Thèses


< retour aux thèses

« Synthèse de moniteurs asynchrones à partir d'assertions temporelles pour la surveillance robuste de circuits synchrones ».

Auteur : A. Porcher
Directeur de thèse : L. Fesquet
Co-directeur de thèse : K. Morin-Allory
Président du jury : I. O'Connor
Rapporteur(s) de thèse : H. Mehrez, A. Salem,
These de Doctorat Université de Grenoble
Spécialité : Nanoélectronique et Nanotechnologies
Soutenance : 03/05/2012
ISBN : 978-2-84813-187-0

Résumé

Avec l’avènement des systèmes intégrés complexes, la vérification par assertions (Assertion Based Verification ou ABV) s’est imposée comme une solution pour la vérification semi-formelle des circuits. L’ABV permet de valider qu’un circuit satisfait ou non une propriété (ou assertion). Des travaux antérieurs ont montré qu’il était possible de synthétiser ces propriétés sous la forme de moniteurs matériels. Ces derniers peuvent ainsi être embarqués à demeure sur un circuit afin qu’ils assurent une tâche de monitoring. Avec un objectif de surveillance et de sûreté, l’utilisation de tels moniteurs est un plus. Néanmoins, ces derniers sont aussi sensibles que les circuits surveillés à une dégradation environnementale (tension, température, vieillissement, …). Afin de réduire le risque de dysfonctionnement des moniteurs, initialement conçus comme des circuits synchrones, une variante asynchrone (quasi-insensible aux délais) est proposée dans cette thèse. Ces travaux s'inscrivent dans le cadre du projet ANR SFINCS (Thalès, Dolphin Integration, TIMA) et ont mené à la définition d’une méthode de synthèse de moniteurs asynchrones matériels tirant parti de la robustesse et de la modularité des implémentations asynchrones. Les études menées se focalisent en premier lieu sur la conception d’une bibliothèque de moniteurs élémentaires asynchrones et sur une méthode d'interconnexion ad hoc permettant de constituer des moniteurs complexes. Afin de garantir les bonnes propriétés de robustesse de ces moniteurs, une étude a été menée à l’aide de l’outil de vérification formelle RAT. Il a notamment été prouvé que la connexion d’un moniteur asynchrone avec un circuit synchrone (à surveiller) était un point particulièrement délicat car les hypothèses du circuit synchrone contraignent le moniteur asynchrone. Il a donc été proposé d’introduire un dispositif de contrôle de l’horloge du circuit synchrone, appelé « clock stretching », afin de relaxer les hypothèses temporelles synchrones qui sont appliquées à la partie asynchrone.