«La preuve formelle pourrait bien changer la donne en conception»

摘要

La vérification formelle investit peu à peu les flots de conception de systèmes numériques. Sans constituer une alternative à la simulation elle propose des approches nouvelles. Technologie déjà bien au point, la preuve d'équivalence permet de comparer deux représentations d'un même circuit. La comparaison est statique et basée sur l'identification deux à deux des unités de mémorisation et des fonctions combinatoires. Les entrées sont soit des modèles synthétisables, soit des «netlists» synthétisées.