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...