Colloque

Un outil hybride pour la vérification formelle de circuits

S. Kort

V. Pisini

O. Ait-Mohamed

P. Curzon

X. Song

S. Tahar

Membre a labase

S. Kort

Résumé du colloque

Les circuits logiques n'ont pas cessé d'être de plus en plus complexes. Les techniques classiques de vérification, comme la simulation, se sont avérées incapables d'affronter une telle complexité. De nouvelles techniques de vérification baptisées méthodes formelles ont vu le jour. Ces techniques peuvent impliquer l'utilisation de démonstrateurs de théorèmes ou de vérificateurs d'équivalence. Le principal avantage des démonstrateurs de théorèmes est leur capacité à vérifier des circuits complexes. Cependant, ces outils nécessitent une certaine expertise. D'autre part, ils requièrent une interaction permanente avec l'utilisateur. Les vérificateurs d'équivalence quant à eux sont entièrement autonomes. Cependant, ils échouent à vérifier des circuits de grandes tailles à cause du problème d'explosion d'états. Une utilisation conjointe de ces deux types d'outils appelée aussi hybridation semble être très prometteuse. En effet, cette approche permettra de cumuler les avantages des deux techniques à savoir la puissance des techniques de preuves de théorèmes et l'automatisme des techniques de vérification d'équivalence. On présente ici un outil de vérification formelle qui intègre HOL et MDG. HOL est un démonstrateur de théorèmes basé sur une logique d'ordre supérieur. MDG est un outil de vérification d'équivalence et de modèles basé sur des diagrammes de décision. L'outil hybride accepte une spécification et une implémentation hiérarchiques d'un circuit. Ces deux descriptions sont exprimées dans un sous-ensemble de la logique HOL. L'utilisateur peut ensuite établir la validité d'un bloc soit par le biais d'une preuve HOL classique soit en passant par MDG. L'invocation de MDG s'effectue en utilisant des tactiques. Ces tactiques se chargent de la traduction de la description du circuit en un langage acceptable par MDG, du lancement de cet outil et de l'analyse de ses résultats. Dans le cas où la vérification réalisée par MDG aboutisse, un théorème établissant la validité du bloc en question est généré. Ce théorème est ensuite utilisé pour vérifier des blocs de niveau supérieur. Dans le cas où la vérification réalisée par MDG échoue, l'utilisateur doit recourir à une preuve HOL classique.