Colloque

Vérification formelle de systèmes matériels

S. Tahar

Membre a labase

S. Tahar

Résumé du colloque

Le défi crucial dans la vérification de l’exactitude des systèmes matériels réside dans le fait que de tels systèmes complexes doivent répondre à des exigences de synchronisation strictes pour assumer en même temps la spécification des performances du produit original, ainsi que les diverses contraintes de l’environnement dans lequel ils sont utilisés. Étant donnée le nombre presque infini et la diversification des vecteurs de tests dont on aurait besoin pour atteindre une couverture des erreurs possibles, d’autre techniques ont vu le jour pour complementer la vérification traditionnelle par simulation. L’une de ces nouvelles techniques très prometteuses est la méthode de vérification formelle. Le but de cette présentation est donc de donner un aperçu sur les principales techniques de vérification formelle des systèmes matériels. Ceci comprend une brève introduction à la place de la vérification formelle dans le flux de conception de systèmes digitaux ainsi qu’une taxonomie des divers méthodes et outils existants. En se référant à cette classification, on se penche en premier lieu sur la vérification par équivalence, utilisée surtout au niveau portes. Ensuite on explore les méthodes de vérification basées sur les prouveurs de théorèmes. Pour le reste de la présentation on donne un aperçu plus détaillé sur les techniques de vérification de modèles, incluant un survol des logiques temporelles pour la description des propriétés, et les techniques fondamentales de la manipulation symbolique des diagrammes de décision binaires (BDD). Pour chacune de ces techniques de vérification formelle on donne quelques exemples d’outils académiques ainsi que commercialisés tel que les produits de Cadence ou Synopsys. L’introduction de ces techniques et outils sera aussi accompagnée par quelques études de cas résultants de divers projets pilotes universitaires ainsi qu’en industrie.