Validation fonctionnelle et temporelle de circuits mémoires décrits au niveau transistor par des méthodes formelles – VALMEM

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`es 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, basée sur des abstractions originale 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.