Introduction

Le fonctionnement d'un circuit peut être perturbé par des phénomènes tels que des impacts de particules, des perturbations électromagnétiques ou encore des dégradations dû au vieillissement. Dans certain cas, ces phénomènes peuvent provoquer des erreurs et complètement modifier le comportement du système

La robustesse d’un système caractérise la capacité de ce dernier à réagir « convenablement Â» même lorsqu’il évolue dans un environnement perturbé. L’analyse des capacités de robustesse d’un système est un problème important qui intervient dans les différentes étapes de conception d’un système intégré sur puce : d’un point de vue algorithmique lors des différentes étapes de spécification et raffinements et dans la mise en Å“uvre de mécanisme de protection par blindage ou redondance au niveau du circuit implanté.

Des outils d'analyse de robustesse de circuit ont été développés au sein du LIP6, ces outils se basent sur des techniques de model checking utilisé principalement dans le domaine de la vérification.Récemment des progrès significatifs ont été réalisés dans le domaine de la vérification de circuits en employant en particulier des techniques basées sur des « SAT Solvers Â» combinées avec l’approche dite « Bounded Model Checking Â».

Un SAT solver détermine si il existe une configuration des variables d’une formule booléenne qui rende celle-ci vraie.

Ainsi, le but principal du stage est d’étudier la possibilité de parallélisation d’algorithmes de résolution de problèmes SAT (en particulier le problème de comptage du nombre de solutions d’un problème SAT), comme heuristique permettant l’accélération de la résolution. Ensuite, il sera question d’intégrer le résultat de cette étude dans le logiciel VIS (un outil qui intègre la vérification, la simulation et la synthèse des systèmes matériels et les algorithmes de quantification de la robustesse).

Contexte

 

Le stage se déroulera au LIP6, dans l’équipe MOVE, du département RSR. Il s’intègre dans la suite du projet FME3 (Enhancing the Evaluation of Error consequences using Formal Methods), dont l’objectif principal est l’évaluation de la robustesse des circuits intégrés.

Le stage sera encadré par Souheib Baarir, membres du LIP6 (équipe MoVe) et Cécile Braunstein (équipe ALSOC).

Travail à réaliser

• Etat de l’art des techniques et outils existants.

• Construction d’une série de programme de Référence.

• Réalisation d’un prototype.

Pré-requis

• Connaissance de C, C++.

• Des connaissances en (Bounded) Model Cheking seront très appréciées.

Références

1. V. Dahllof, P. Jonsson, M. Wahlstrom. Counting satisfying assignments in 2-SAT and 3-SAT.

2. H. Jin, F. Somenzi. Prime clauses for fast enumeration of satisfying assignments to boolean circuits

3. J. Roberto, Jr. Bayardo, J. D. Pehoushek. Counting Models Using Connected Components.

4. Marc Thurley. SharpSAT - Counting Models with Advanced Component Caching and Implicit BCP.

5. A. Biere, A. Cimatti, E. Clarke and Y. Zhu. Symbolic Model Checking without BDDs

6. R. K. Brayton et all. VIS : A System for Verification and Synthesis.