Diagnostique de bogues utilisant une abstraction de prédicat au niveau mot

 Encadrement

Cecile Braunstein

 

Université P. & M. Curie, LIP6 - CNRS UMR 7606 –

4 Place Jussieu, Paris, France

cecile.braunstein@lip6.fr

Contexte

Ce stage s'inscrit dans le cadre d'un projet de coopération et d'échange avec l'université de Brême (projet DeAR : debugging with abstraction-refinement). L'objectif de ce projet est de fournir une aide à la détection automatique de bogue.

Les systèmes analysés représentent des circuits décrits dans un langage de description de matériel (VHDL, Verilog, SystemC), et peuvent contenir des erreurs (mauvaise variable utilisée dans une expression, mauvais opérateur, ...), que l'on nomme bogue. Les méthodes de simulation, test ou vérification permettent de déterminer si une description ne contient pas d'erreur, et si elle en contient, fournissent une trace d'exécution conduisant à un état dans lequel l'erreur a été détectée. L'erreur détectée peut être distante (temporellement et spatialement) de l'erreur d'origine. Il faut déboguer le code pour déterminer la cause primaire de l'erreur qui a été détectée. Cette tâche est en général ardue, longue et fastidieuse.

Des techniques pour automatiser le déboguage ont été proposées par différents auteurs ([1-4]). Parmi ces méthodes, le déboguage basé sur le problème de satisfiabilité booléenne (SAT) a montré son efficacité et son aptitude à traiter des problèmes variés tels que le diagnostique de bogues ou le déboguage de spécification. Cette approche se sert des informations du système erroné et fournit un ensemble de composants suspects. Évidemment, ce type de technique entraîne un besoin excessivement important de mémoire et de temps d'exécution même pour des circuits de taille modeste. Réduire les besoins en mémoire devient primordial pour l'efficacité de ce type de techniques.

Dans le cadre de ce projet, le laboratoire LIP6 se propose de définir des abstractions adéquates pour faciliter la localisation de la source d'un bogue. Une abstraction réduit la taille du problème en ne gardant qu'un sous-ensemble des informations du modèle. La difficulté est de trouver une abstraction contenant assez de détails pour localiser les sources d'erreurs, tout en restant légère afin d'obtenir un modèle analysable par les outils de model checking. La recherche d'une telle abstraction se fait le plus souvent par raffinements successifs à partir d'une abstraction très grossière du modèle, cette boucle est appelée CEGAR (counter-example guided abstraction refinement) [5].

Objectif

L'objectif de ce stage est de caractériser l'impact d'une abstraction par prédicats niveau mot [7] sur le diagnostique de bogue au niveau RTL (register transfert level). L'objectif est de localiser le bogue au niveau du code Verilog du système. Cette abstraction a été utilisée avec succès pour la vérification de propriété de sûreté dans l'outil VCegar [6]. Lors de la localisation de bogue par abstraction, une partie des suspects peut être faux (dû à l'abstraction). L'abstraction doit alors être raffinée pour restreindre l'ensemble des suspects potentiels aux seuls vrais suspect (existant dans le modèle concret).

 

Travail proposé

Les étapes proposées sont les suivantes :

 

• Se familiariser avec les techniques de localisation de bogue proposées par l'université de Brême (notre partenaire dans ce projet).

• Étudier l'abstraction envisagée.

• Proposer une méthode de raffinement pour enlever les faux suspects.

•  Ã‰valuer les performances liées à l'abstraction par rapport à la méthode sans abstraction.

Prérequis 

• un sens de la bonne programmation en C ou C++
• la validation d’un module d’enseignement niveau M2  sur les bases de vérification par model-checking (module SAR : MSR / VFSR ou module SESI : VERIF)
• Parler et écrire en Anglais

Références bibliographiques

[1] Smith, A.; Veneris, A. G.; Ali, M. F. & Viglas, A. Fault diagnosis and logic debugging using Boolean satisfiability IEEE Trans. on CAD of Integrated Circuits and Systems, 2005, 24, 1606-1621

[2] Fey, G.; Staber, S.; Bloem, R. & Drechsler, R. Automatic Fault Localization for Property Checking IEEE Trans. on CAD of Integrated Circuits and Systems, 2008, 27, 1138-1149

[3] S.Safarpour and A.Veneris, Automated Debugging with High Level Abstraction and Refinement, in IEEE High Level Design Validation and Test 2009

[4] Sülflow, A.; Fey, G.; Braunstein, C.; Kühne, U. & Drechsler, R. Increasing the accuracy of SAT-based debugging DATE, IEEE, 2009, 1326-1331

[5] Clarke, E.; O.Grumberg; Jha, S.; Lu, Y. & Veith, H. Emerson, E. & Sistla, A. (ed.) Counterexample-Guided Abstraction Refinement. CAV'00: Proceedings of the 12th International Conference on Computer Aided Verification, Springer, 2000, 1855, 154-169

[6] Jain, H.; Kroening, D.; Sharygina, N. & Clarke, E. VCEGAR: Verilog CounterExample Guided Abstraction Refinement TACAS'07: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2007

[7] Jain, H.; Kroening, D.; Sharygina, N. & Clarke, E. Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog IEEE Transaction on CAD of Integrated Circuits and Systems, 2008, 27, 366-379