V rification Semi-Formelle Et Synth se Automatique de Psl Vers Hdl

La vrification base de proprits (PBV) est devenue un lment essentiel des flots de conception pour supporter la vrification de circuits complexes. La vrification dynamique base de proprits connecte au circuit des moniteurs et des gnrateurs de test synthtiss partir de proprits pour construire de manire simple un environnement de test. Une partie des travaux consist dvelopper une approche de synthse de proprits pour la gnration de vecteurs de test. Il est alors possible de spcifier et d'obtenir un modle pour tout l'environnement du circuit.La contribution la plus intressante de cette thse tiens dans la mthode qui a t mise en place pour synthtiser une spcification temporelle en un circuit correct par construction. Alors que les approches de l'tat de l'art ont une complexit polynomiale, la ntre est linaire en la spcification. L'outil SyntHorus a t dvelopp pour supporter cette mthode et synthtise en quelques secondes un circuit correct par construction partir d'une spcification de plusieurs centaines de proprits. Les mthodes et outils dvelopps durant cette thse ont t valids, renforcs et transfrs dans l'industrie.