Loading...
Please wait, while we are loading the content...
Synthèse de moniteurs asynchrones à partir d'assertions temporelles pour la surveillance robuste de circuits synchrones
| Content Provider | Semantic Scholar |
|---|---|
| Author | Porcher, Alexandre |
| Copyright Year | 2012 |
| Abstract | Avec l'avenement des systemes integres complexes, la verification par assertions(Assertion Based Verification ou ABV) s'est imposee comme une solution pour la verification semi-formelle des circuits. L'ABV permet de valider qu'un circuit satisfait ou non une propriete(ou assertion). Des travaux anterieurs ont montre qu'il etait possible de synthetiser ces proprietes sous la forme de moniteurs materiels. Ces derniers peuvent ainsi etre embarques a demeure sur un circuit afin qu'ils assurent une tâche de monitoring. Avec un objectif de surveillance et de surete, l'utilisation de tels moniteurs est un plus. Neanmoins, ces derniers sont aussi sensibles que les circuits surveilles a une degradation environnementale(tension, temperature, vieillissement, …). Afin de reduire le risque de dysfonctionnement des moniteurs, initialement concus comme des circuits synchrones, une variante asynchrone(quasi-insensible aux delais) est proposee dans cette these. Ces travaux s'inscrivent dans le cadre du projet ANR SFINCS(Thales, Dolphin Integration, TIMA) et ont mene a la definition d'une methode de synthese de moniteurs asynchrones materiels tirant parti de la robustesse et de la modularite des implementations asynchrones. Les etudes menees se focalisent en premier lieu sur la conception d'une bibliotheque de moniteurs elementaires asynchrones et sur une methode d'interconnexion ad hoc permettant de constituer des moniteurs complexes. Afin de garantir les bonnes proprietes de robustesse de ces moniteurs, une etude a ete menee a l'aide de l'outil de verification formelle RAT. Il a notamment ete prouve que la connexion d'un moniteur asynchrone avec un circuit synchrone(a surveiller) etait un point particulierement delicat car les hypotheses du circuit synchrone contraignent le moniteur asynchrone. Il a donc ete propose d'introduire un dispositif de controle de l'horloge du circuit synchrone, appele « clock stretching », afin de relaxer les hypotheses temporelles synchrones qui sont appliquees a la partie asynchrone. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://tel.archives-ouvertes.fr/tel-00986690/document |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
