Abstract FR:

Dans le domaine de la conception des systemes materiels, la validation a toutes les etapes du processus de conception revet une importance de plus en plus grande, compte tenu de la complexite croissante des circuits et systemes. Nous proposons dans cette these, une methodologie et un ensemble d'outils automatiques pour la verification de systemes decrits en langage vhdl. Notre approche repose sur un modele formel de la semantique de vhdl. Nous reduisons l'analyse du systeme a ses etats observables, appeles etats stables, et definissons la semantique d'un sous-ensemble de vhdl en termes de reseaux de petri interpretes et temporises (rpit). Un premier outil appele vpn traduit des programmes vhdl dans ce modele formel (rpit). Le reseau de petri obtenu est un formalisme intermediaire permettant de construire un systeme de transitions caracterisant le comportement du programme vhdl. Ce systeme de transitions sert de support a la verification symbolique de proprietes temporelles exprimees en ctl d'une part et a montrer l'equivalence comportementale de deux descriptions vhdl differentes d'un meme systeme d'autre part. Un algorithme adapte a la construction de l'ensemble des etats stables, base sur le cycle de simulation de vhdl, est propose, implante et compare avec l'algorithme classique de traversee symbolique de l'espace des etats. Une strategie de reordonnancement dynamique controle par l'application pour limiter l'occupation en memoire des bdd est propose. Son efficacite est demontree sur un ensemble de problemes-test concrets. Deux outils exploitant le systeme de transitions obtenu sont ensuite etudies: l'outil vmc, qui permet de faire de la verification symbolique de modele sur les systemes decrits en vhdl ; l'outil psm, qui permet de verifier l'equivalence comportementale de deux machines a etats decrites en vhdl. Certains resultats de verification symbolique, prenant en compte la semantique vhdl, sur des exemples non-triviaux (jusqu'a 1600 lignes vhdl), sont les premiers a etre publies. Enfin, nous proposons une approche originale de reconnaissance des elements memorisants a partir des descriptions vhdl en vue de la synthese comportementale. Contrairement aux outils existants, aussi bien academiques que commerciaux, nous n'imposons aucune contrainte particuliere sur les styles des descriptions. L'ensemble des travaux de conception et de developpement des outils presentes a donne lieu a 8 articles, dont 7 deja parus dans des actes de conferences internationales