Loading...
Please wait, while we are loading the content...
Similar Documents
Vérification semi-formelle et synthèse automatique de circuits à partir de spécifications temporelles écrites en PSL
| Content Provider | Semantic Scholar |
|---|---|
| Author | Oddos, Yann |
| Copyright Year | 2009 |
| Abstract | La verification a base de proprietes (PBV) est devenue un element essentiel des flots de conception pour supporter la verification de circuits complexes. Pour de tels composants ou les techniques de verification formelle ne peuvent s'appliquer, 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. Durant cette these une partie des travaux a consiste a developper une approche de synthese de proprietes pour la generation de vecteurs de test. Dans ce contexte, les proprietes decrivent l'environnement du circuit sous test. Elles sont synthetisees en generateurs produisant des sequences de test respectant la propriete correspondante. Il est alors possible de specifier et d'obtenir un modele pour tout l'environnement du circuit. Alors que notre approche est modulaire, une methode a base d'automates a ete developpee en collaboration avec l'universite de McGill. 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. La correction des generateurs et de la methode de synthese a ete effectuee a l'aide du prouveur de theoreme PVS. Les methodes et outils developpes durant cette these ont ete valides, renforces et transferes dans l'industrie grâce a plusieurs cooperations (Thales Group, Dolphin Integration et ST-Microelectronics) et au projet ANR SFINCS. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://tima.univ-grenoble-alpes.fr/publications/files/th/2009/sfv_0318.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
