Validation fonctionnelle et temporelle des mémoires embarquées,
décrites au niveau transistor, par des méthodes formelles
Objectifs
Le projet VALMEM s'intéresse la vérification fonctionnelle et temporelle de circuits mémoires.
Les circuits mémoires ont la particularité d'intégrer des fonctionnalités toujours plus complexes tout en devant répondre des objectifs de performances accrues. Pour ces raisons, ces circuits sont conçus directement au niveau transistor, ce qui rend très difficile leur validation.
VALMEM regroupe des partenaires universitaires (LSV, LIP6) et industriel (STMicroelectronics) aux compétences complémentaires qui abordent ce problème de vérification avec une approche formelle spécialisée pour les circuits mémoires, en partant de leur description en transistors. L'objectif est de fournir une plate-forme logicielle prototype, base sur des abstractions originales du modèle en transistors, et des méthodes de vérification spécifiques, dans le but de vérifier un jeu d'exemples de circuits mémoires commercialisés.
Partenaires
LIP6 (Laboratoire d’Informatique de Paris 6) P. Bazargan-Sabet, E. Encrenaz, D. Le Du, P. Renault, A. Bara
LSV (Laboratoire Spécification et Vérification) E. André, L. Fribourg
STMicroelectronics (Research & Development Crolles), R. Chevallier
Durée du projet : janvier 2007 – décembre 2010
Définition du projet : le descriptif du projet
Articles
| • | . Weiwen Xu, Timed Verification of a Generic Architecture of a Memory Circuit using Parametric Timed Automata. International Journal of Formal Methods in System Design, vol 34(1), pp 59-81, 2009. |
| • | . An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science, vol 20(5), pp 819-836, 2009. |
| • | . An Inverse Method for Parametric Timed Automata. In Vesa Halava and Igor Potapov (eds.), RP'08, ENTCS 223, pages 29-46. Elsevier Science Publishers, 2008. ( PDF | BibTeX + Abstract ) |
| • | and Patricia Renault. Formal Verification of Timed VHDL Programs. International Forum on Specification and Design Languages, 2010. |
| • | |
| • |
Outils
L’outil IMITATOR est développé par Etienne André dans le cadre du projet VALMEM.
L’outil MYGALE est développé par Pirouz Bazargan-Sabet dans le cadre du projet VALMEM.
L’outil TIMEX est développé par Dominique Le Du dans le cadre du projet VALMEM.
L’outil VHDL2TA est développé par Abdelrezzak Bara dans le cadre du projet VALMEM.
Delivrables
D1.1 Etat de l’art sur la conception des mémoires embarquées (jun. 2007)
D2.1 Etat de l’art des méthodes de validation des mémoires (jun. 2007)
D2.1-partie 1 : Abstraction fonctionnelle et Abstraction temporelle
D2.1-partie 2 : Analyse fonctionnelle et temporelle à l’aide d’automates temporisés
D2.2 Définition d’un nouveau modèle fonctionnel et temporel pour la vérification de circuits mémoire (oct. 2007)
D1.3 Flot de conception (dec 2007)
D2.3 Combinaison de méthodes d'abstraction fonctionnelle et de méthodes de caractérisation temporelle d'un réseau de transistors (dec 2007)
D3.1 Modeles d'automates temporisés pour l'analyse de circuits mémoire (jan 2008)
D3.2 Model-checking temporisé spécialisé pour les circuits mémoire (jun 2008)
D3.3 Outil prototype de synthese de parametres temporises pour la verification de circuits memoire (dec 2008)
D2.4 Outil prototype d'abstraction fonctionnelle et temporelle de circuits memoire (dec 2008)
vhdl2ta : programme Traduction automatique de programmes VHDL en automates temporisés (dec 2009)
vhdl2ta : jeu de tests
D4.2 et D4.3
Experiments of the prototype tools on case studies, comparison of obtained results and conclusion (dec 2010) Réunions date compte-rendu documents de travail / présentations 10 janvier 2007 à Paris Présentation des différents participants et de
leur domaine d'activités 27 mars 2007 à Paris R. Chevallier : Design
flow des mémoires
P. Bazargan : Extraction
fonctionnelle et temporelle E. Encrenaz : Vérification
des temps de réponses de mémoire par automates
temporisés 03 juillet 2007 à Crolles Discussions sur la première étude de cas fournie
par ST : la mémoire SPSMALL.
Commentaires des délivrables D1.1 et D2.1
12 octobre 2007 à Paris R. Chevallier : Description de la mémoire SPREG
(confidentiel)
R. Bazargan : Commentaires
du document D2.2
13 mars 2008 à Paris R. Bazargan : Abstraction
fonctionnelle d'une netlist en transistors
E. Encrenaz : Vérification
temporisée d'une portion de la mémoire SPSMALL
02 juin 2008 à Crolles R. Bazargan : Functional
and Timing Abstraction
28 aout 2008 à Crolles Réunion préparatoire à la revue ANR du 11/09 11 decembre 2008 à Crolles Avancement du projet A. Andre : Presentation du prototype IMITATOR
12 juillet 2009 à Cachan Avancement du projet P. Bazargan : Point d'avancement sur l'abstraction fonctionnelle
E. Encrenaz : Transformation automatique de description VHDL en automates temporisés pour Hytech
03 novembre 2009 à Paris Avancement du projet P. Bazargan : Extraction temporelle A. Bara : Transformation automatique de description VHDL en automates temporisés
E. Andre : Point sur IMITATOR
25 mai 2010 à Paris Avancement du projet A. Bara : Vérification de descriptions VHDL + temps
P. Bazargan : Problèmes liés à l'extraction temporelle
E. Andre : Point sur IMITATOR-II