Les travaux présentés dans ce document portent sur la vérification<br />de modèles de systèmes sur puce, au niveau transactionnel (TLM).<br />Nous présentons le niveau transactionnel et ses variantes, et<br />rappelons en quoi ce nouveau niveau d'abstraction est aujourd'hui<br />nécessaire en plus du niveau de transfert de registre (RTL) pour<br />répondre aux contraintes de productivités et de qualités de plus en<br />plus fortes, et comment il s'intègre dans le flot de conception.<br /><br />Nous présentons un nouvel outil, LusSy, permettant la vérification<br />formelle de modèles transactionnels écrits en SystemC. Sa structure<br />interne s'apparente à celle d'un compilateur: Une partie frontale,<br />Pinapa, qui lit le programme source, une extraction de la<br />sémantique, Bise, dans notre formalisme intermédiaire \hpiom, une<br />série d'optimisations dans le composant Birth, et des générateurs<br />de code pour les outils de preuves pour Lustre et SMV.<br /><br />Lussy est conçu et écrit de manière à avoir aussi peu de limitation<br />que possible sur la forme du code SystemC accepté en entrée. \pinapa<br />utilise une approche innovante qui lui permet de s'affranchir de la<br />plupart des limitations dont souffrent les outils similaires.<br />L'extraction de la sémantique implémente plusieurs constructions TLM<br />qu'aucun autre outil disponible aujourd'hui ne gère. Il ne demande<br />pas d'annotation manuelle du code source, toute la chaîne étant<br />entièrement automatisée.<br /><br />Lussy est capable de prouver formellement des propriétés sur des<br />modèles de petites taille, et ses composants sont réutilisables pour<br />des outils de preuve compositionnelle, ou d'analyse de code autre<br />que le model-checking qui passeront mieux à l'échelle que l'approche<br />actuelle.<br /><br />Nous présentons les principes de chaque étape de la transformation,<br />ainsi que notre implémentation. Les résultats sont donnés pour des<br />exemples simples et petits, et pour une étude de cas de taille<br />moyenne, EASY. Les expérimentations avec Lussy nous ont permis de<br />comparer les différents outils de preuves que nous avons utilisés,<br />et d'évaluer l'efficacité des optimisations que nous avons<br />implémentées.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00311033 |
| Date | 09 December 2005 |
| Creators | Moy, Matthieu |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.006 seconds