Abstract FR:

Nous presentons dans cette these une methode de verification automatique des regles de testabilite. Nous nous interessons a trois problemes: le traitement des circuits de grande complexite, l'adaptabilite a differents jeux de regles et la portabilite vers differents environnements de conception. La diversite des regles de testabilite fait que celles-ci ne peuvent pas etre couvertes par une methode generale et efficace de verification. Nous mettons en evidence, a l'issue d'une classification d'un ensemble de regles effectivement utilisees en industrie, en fonction des besoins de verification, que la plupart de celles-ci portent sur l'existence ou la configuration de chemins dans une description au niveau portes d'un circuit. Pour la verification de ce genre de regles, nous montrons comment une application de la technique de simulation symbolique permet de garantir une meilleure performance en comparaison a la technique classique de trace de chemins. Pour les autres classes de regles, en faible nombre mais qui sont tres importantes du point de vue du test, nous utilisons la simulation logique et l'inspection structurelle comme moyens supplementaires de verification. L'adaptabilite de l'outil de verification suppose que celui-ci puisse etre facilement parametrable pour faire face au changement des regles. La rigidite des verificateurs utilisant la simulation symbolique ne leur permet pas de resoudre ce probleme. Nous proposons pour cela un concept de generateur de simulateur symbolique. A partir d'une description structurelle du circuit a verifier au niveau portes, un simulateur symbolique peut ainsi etre defini pour chaque jeu de regles. Un prototype a ete developpe pour valider les concepts definis. L'utilisation de celui-ci sur plusieurs circuits, d'une part, et les resultats de performance obtenus de l'autre, confirment que la methode proposee constitue la voie la plus efficace permettant de repondre aux problemes poses par la verification des regles