Thèse réalisée par Matthieu Moy au laboratoire Verimag et dans l'entreprise STMicroelectronics, commencée en octobre 2002 et soutenue le 9 décembre 2005.
Les travaux présentés dans ce document portent sur la vérification de modèles de systèmes sur puce, au niveau transactionnel (TLM). Nous présentons le niveau transactionnel et ses variantes, et rappelons en quoi ce nouveau niveau d'abstraction est aujourd'hui nécessaire en plus du niveau de transfert de registre (RTL) pour répondre aux contraintes de productivités et de qualités de plus en plus fortes, et comment il s'intègre dans le flot de conception.
Nous présentons un nouvel outil, LusSy, permettant la vérification formelle de modèles transactionnels écrits en SystemC. Sa structure interne s'apparente à celle d'un compilateur: Une partie frontale, PINAPA, qui lit le programme source, une extraction de la sémantique, BISE, dans notre formalisme intermédiaire HPIOM, une série d'optimisations dans le composant BIRTH, et des générateurs de code pour les outils de preuves pour LUSTRE et SMV.
LusSy est conçu et écrit de manière à avoir aussi peu de limitation que possible sur la forme du code SystemC accepté en entrée. PINAPA utilise une approche innovante qui lui permet de s'affranchir de la plupart des limitations dont souffrent les outils similaires. L'extraction de la sémantique implémente plusieurs constructions TLM qu'aucun autre outil disponible aujourd'hui ne gère. Il ne demande pas d'annotation manuelle du code source, toute la chaîne étant entièrement automatisée.
LusSy est capable de prouver formellement des propriétés sur des modèles de petites taille, et ses composants sont réutilisables pour des outils d'analyse de code autre que le model-checking qui passeront mieux à l'échelle que l'approche actuelle.
Nous présentons les principes de chaque étape de la transformation, ainsi que notre implémentation. Les résultats sont donnés pour des exemples simples et petits, et pour une étude de cas de taille moyenne, EASY. Les expérimentations avec LusSy nous ont permis de comparer les différents outils de preuves que nous avons utilisés, et d'évaluer l'efficacité des optimisations que nous avons implémentées.
La thèse complete peut être téléchargée ici : these-fr.pdf.
Une version entièrement en anglais est disponible ici : these-en.pdf.
Les transparents présentés le 9 décembre 2005 sont disponibles ici : slides-these.pdf.
Les détails et les entrées BibTeX sont disponibles ici.
Publié dans les proceedings de ACSD 2005
Publié dans les proceedings d'EMSOFT 2005
Paru aux éditions Springer
Dans le journal Design Automation for Embedded Systems, 2006
Pinapa, la partie frontale de LusSy, est disponible sur sourceforge.
La liste des publications citées dans le document de thèse est disponible ici.
Pour citer cette thèse :
@PhdThesis{these-moy,
author = {Matthieu Moy},
title = {Techniques and Tools for the Verification of
Systems-on-a-Chip at the Transaction Level},
school = {INPG, Grenoble, France},
year = 2005,
URL = "http://www-verimag.imag.fr/~moy/phd/",
month = {December}
}