– SFINCS

Le projet SFINCS (Semi-Formal INstrumentation for Circuits and Systems) recherche, étudie et développe de nouvelles techniques nécessaires à la validation des systèmes sur puce. SFINCS se situe dans le cadre de l'Assertion-Based Verification (ABV). Pendant le processus de conception, des assertions (écrites par exemple en PSL ou SVA) permettent de décrire :
? des fonctionnalités à garantir par le composant (assert). Ces énoncés assert peuvent être testés tout au long du flot de conception par des moniteurs de surveillance.
? des contraintes sur les entrées (assume). Des séquences d'entrées satisfaisant ces énoncés assume peuvent être produites par des générateurs de séquences de test.

Le but de ce projet (voir Figure 1) est de développer et d'intégrer des méthodologies permettant l'application de l'ABV à une palette de composants matériels, au moyen d'une approche uniforme basée sur une technologie conçue au Laboratoire TIMA. Nous nous intéressons aux éléments suivants :
? IPs synchrones décrites au niveau RTL
? fonctions mixtes, pseudo-synchrones et systèmes GALS (Globally Asynchronous Locally Synchronous)
? aspects Systèmes HW/SW décrits au niveau SystemC TLM (transactionnel)
? application aux SoC mixtes, SoC complexes et aux systèmes critiques

L'outil prototype HORUS développé au Laboratoire TIMA permet de générer automatiquement des descriptions Verilog ou VHDL :
? de moniteurs de surveillance synchrones ou asynchrones
? de générateurs de séquences de test
? de mécanismes d'historique et d'interface.
Cette approche utilise une bibliothèque (VHDL et Verilog) de composants élémentaires prouvés corrects associés aux opérateurs primitifs de PSL ou SVA. Une méthode d'interconnexion, elle aussi prouvée correcte, de ces modules primitifs permet l'obtention d'une description VHDL ou Verilog optimisée et synthétisable.
La collaboration entre le Laboratoire TIMA et les sociétés Dolphin et Thales Communications donnera lieu essentiellement aux travaux suivants :
? la mise en oeuvre par Dolphin de la technologie HORUS pour la construction de moniteurs et générateurs de tests synchrones dans l'environnement basé sur la simulation à signaux mixtes. Son outil pour l'estimation de la consommation de puissance permettra aussi d'évaluer la consommation induite par la logique d'assertions. La méthode HORUS pourra être mise à profit depuis les premières simulations jusqu'au prototypage sur FPGA.
? l'étude et la construction de moniteurs asynchrones, et leur mise en oeuvre dans l'environnement de Dolphin. Les domaines d'application de cette approche sont variés (GALS, fonctions mixtes, systèmes critiques,...). Des études de cas seront fournies par Thales Communications. En particulier la technologie sera éprouvée sur des composants critiques en avionique ou en sécurité.
? l'extension aux descriptions de SoCs complexes faites en SystemC au niveau TLM (transactional level modelling). Un modèle orienté-objet pour l'adaptation de l'approche HORUS à ce niveau de description est en cours de définition au Laboratoire TIMA. Cette technique sera entièrement spécifiée et mise en oeuvre sous la forme d'un outil prototype. Une expérimentation sera réalisée sur des études de cas sélectionnées par Thales Communications, notamment des plateformes SoC.