Détails sur le séminaire

Résumé : Les travaux présentés dans cette thèse portent sur la modélisation, la
spécification et la vérification des modèles des Systèmes sur Puce
(SoCs) au niveau d’abstraction transactionnel et à un niveau
d’abstraction plus élevé. Les SoCs sont hétérogènes: ils comprennent
des composants matériels et des processeurs pour réaliser le logiciel
incorporé, qui est en lien direct avec du matériel. La modélisation
transactionnelle (TLM) basée sur SystemC a été très fructueuse à
fournir des modèles exécutables des SoCs à un haut niveau
d’abstraction, aussi appelés prototypes virtuels (VPs). Ces modèles
peuvent être utilisés plus tôt dans le cycle de développement des
logiciels, et la validation des matériels réels. La vérification basée
sur assertions (ABV) permet de vérifier les propriétés tôt dans le
cycle de conception de façon à trouver les défauts et faire gagner du
temps et de l’effort nécessaires pour la correction de ces
défauts. Les modèles TL peuvent être sur-contraints, c’est-à-dire
qu’ils ne presentent pas tous les comportements du matériel. Ainsi,
ceci ne permet pas la détection de tous les défauts de la conception.
Nos contributions consistent en deux parties orthogonales et
complémentaires: D’une part, nous identifions les sources des
sur-contraintes dans les modèles TLM, qui apparaissent à cause de
l’ordre d’interaction entre les composants. Nous proposons une notion
d’ordre mou qui permet la suppression de ces sur-contraintes. D’autre
part, nous présentons un mécanisme généralisé de stubbing qui permet
la simulation précoce avec des prototypes virtuels SystemC/TLM.
Nous offrons un jeu de patrons pour capturer les propriétés d’ordre
mou et définissons une transformation directe de ces patrons en
moniteurs SystemC. Notre mécanisme généralisé du stubbing permet la
simulation précoce avec les prototypes virtuels SystemC/TLM, dans
lesquels certains composants ne sont pas entièrement déterminés sur
les valeurs des données échangées, l’ordre d’interaction et/ou le
timing. Ces composants ne possèdent qu’une spécification abstraite,
sous forme de contraintes entre les entrées et les sorties. Nous
montrons que les problèmes essentielles de la synchronisation entre
les composants peuvent être capturés à l’aide de notre simulation avec
les stubs. Le mécanisme est générique; nous mettons l’accent
uniquement sur les concepts-clés, les principes et les règles qui
rendent le mécanisme de stubbing implémentable et applicable aux
études de cas industriels. N’importe quel language de spécification
satisfaisant nos exigences (par ex. le langage des ordres mou) peut
être utilisé pour spécifier les composants, c’est-à-dire il peut être
branché au framework de stubbing. Nous fournissons une preuve de
concept pour démontrer l’intérêt d’utiliser la simulation avec stubs
pour la détection anticipée et la localisation des défauts de
synchronisation du modèle.



PhD Defense Committee:
Pr. Erika Abraham, RWTH Aachen University, Germany
Pr. Franco Fummi, Verona University, Italy
Pr. Laurence Pierre, Grenoble Alpes University, France
Dr. Kim Gruttner, Carl von Ossietzky University of Oldenburg, Germany
Dr. Laurent Maillet-Contoz, STMicroelectronics, France