V rification Semi-Formelle Et Synth se Automatique de Psl Vers Hdl (French, Paperback)

La verification a base de proprietes (PBV) est devenue un element essentiel des flots de conception pour supporter la verification de circuits complexes. La verification dynamique a base de proprietes connecte au circuit des moniteurs et des generateurs de test synthetises a partir de proprietes pour construire de maniere simple un environnement de test. Une partie des travaux a consiste a developper une approche de synthese de proprietes pour la generation de vecteurs de test. Il est alors possible de specifier et d'obtenir un modele pour tout l'environnement du circuit.La contribution la plus interessante de cette these tiens dans la methode qui a ete mise en place pour synthetiser une specification temporelle en un circuit correct par construction. Alors que les approches de l'etat de l'art ont une complexite polynomiale, la notre est lineaire en la specification. L'outil SyntHorus a ete developpe pour supporter cette methode et synthetise en quelques secondes un circuit correct par construction a partir d'une specification de plusieurs centaines de proprietes. Les methodes et outils developpes durant cette these ont ete valides, renforces et transferes dans l'industrie.