|
|
|
|
|
|
|
|
 
|
|
 
|
Parallélisation de la résolution de problèmes SAT
Introduction Les circuits intégrés deviennent de plus en plus complexes et réduits. Si des moyens et des outils puissants sont mis à la disposition des développeurs, l’usage d’outils de test automatique et de vérification reste marginal alors que les domaines d’application sont de plus en plus critiques (aérospatiale, télécom, nucléaire,…). 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 problème SAT est le problème de déterminer si les variables d’une formule booléenne peuvent être assignées, de façon à évaluer la formule à vraie. Ce problème trouve son importance dans plusieurs domaines d’applications (model-checking, planification, intelligence artificielle….). Cependant il est connu pour être un problème NP–complet (en général) ! 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). Contexte Le stage se déroulera au LIP6, dans l’équipe ALSOC, du département SoC. Il s’intègre dans le cadre 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, maitre de conférences à l’université de Paris Ouest Nanterre la Défense, rattaché au LIP6 (équipe MoVe). Travail à réaliser
Pré-requis
Références
|
