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 ) |
Outil
L’outil IMITATOR est développé par Etienne André 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 Definition d'un nouveau modele fonctionnel et temporel pour la verification formelle de circuits memoires (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 Jeu de tests du programme de traduction automatique de programmes VHDL en automates temporisés (dec 2009)
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 décembre 2007 à Paris |
R. Chevallier : Commentaires du document D1.3 R. Bazargan : Commentaires du document D2.3 E. Encrenaz : Différents modèles d'automates temporisés pour les portes logiques E. André : Extraction de contraintes temporisées |
|
|
13 mars 2008 à Crolles |
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 |