Le projet MULTIVAL (Validation of Multiprocessor Multithreaded Architectures) porte sur la modélisation formelle, la vérification fonctionnelle et l'évaluation de performance pour des architectures matérielles à haute valeur ajoutée et comportant un haut degré de parallélisme asynchrone. MULTIVAL cible trois architectures ayant un fort potentiel industriel et commercial :

• FAME2 (Flexible Architecture for Multiple Environments) est le successeur prévu à l'horizon 2008 de l'architecture multiprocesseurs FAME qui équipe les serveurs NovaScale de Bull, ainsi que le supercalculateur Tera10 du CEA. Au sein de FAME2, MULTIVAL cible les circuits ASICs qui implémenteront des protocoles asynchrones complexes de routage et de maintien de la cohérence mémoire.


• FAUST (Flexible Architecture of Unified System for Telecom) est une architecture NoC (Network on Chip) conçue au CEA/LETI pour des applications nomades temps-réel telecom et multimédia (4G, MIMO, etc.). Cette architecture et ses futures évolutions intéressent plusieurs industriels, mais la vérification formelle des protocoles de FAUST constitue un préalable à la valorisation de cette technologie.


• FIMAP (FIls Multiples pour Architectures Parallèles) est une architecture destinée aux futurs microprocesseurs STxxxx de ST Microelectronics. En s’appuyant sur un microprocesseur VLIW, le ST231, déjà largement utilisé dans les SoC (System on Chip) actuels, FIMAP introduit deux innovations essentielles : une extension multifils (multithreaded) du coeur de microprocesseur fournissant du parallélisme à grain fin et un cluster de coeurs de processeurs multifils organisé autour d’une architecture SMP (Symmetric Multi-Processing) et d’une mémoire commune.

Ces architectures comportent un fort parallélisme asynchrone nécessitant la mise en oeuvre de protocoles spécifiques et sont caractérisées par une grande complexité qui rend leur mise au point délicate. Or, aucune solution industrielle n'est aujourd'hui en mesure de garantir formellement le bon fonctionnement de ces protocoles. C'est pourquoi Bull, le CEA/LETI et ST Microelectronics souhaitent s'appuyer sur les outils CADP de l'INRIA, déjà utilisés avec succès par Bull pour la mise au point du circuit FSS (FAME Scalability Switch) qui constitue le coeur de FAME. CADP est d'ailleurs l'un des outils de vérification les plus utilisés dans le monde (contrats de licence signés avec 350 institutions).

Un premier défi majeur sera de vérifier ces modèles formels en maîtrisant la complexité combinatoire induite par le fort parallélisme des architectures FAUST, FAME2 et FIMAP.

Un second défi majeur sera de réutiliser les modèles formels développés pour la vérification afin de valider également les aspects quantitatifs (évaluation de performance). Le projet MULTIVAL s’appuiera sur des outils récents ajoutés à CADP qui, en rapprochant l'évaluation de performance de la vérification fonctionnelle, réduisent l'effort de modélisation et accélèrent la mise sur le marché des produits.

Pour en savoir plus:

• poster de présentation du projet Multival (janvier 2007)
• transparents de présentation du projet Multival (juin 2007)