Vers la prédiction de performance de modèles compositionnels dans les architectures GALS

Validation, comprising functional verification and performance evaluation, is critical for complex hardware designs. Indeed, due to the high level of parallelism in modern designs, a functionally verified design may not meet its performance specifications. In addition, the later a design error is identified, the greater its cost. Thus, validation of designs should start as early as possible. This thesis proposes a compositional modeling framework, taking into account functional and time aspects of hardware systems, and defines a performance evaluation approach to analyze constructed models. The modeling framework, called Interactive Probabilistic Chain (IPC), is a discrete-time process algebra, representing delays as probabilistic phase type distributions. We defined a branching bisimulation and proved that it is a congruence with respect to parallel composition, a crucial property for compositional modeling. IPCs can be considered as a transposition of Interactive Markov Chains in a discrete-time setting, allowing a precise and compact modeling of fixed hardware delays. For performance evaluation, a fully specified IPC is transformed, assuming urgency of actions, into a discrete-time Markov chain, which can then be analyzed. Additionally, we defined a performance measure, called latency, and provided an algorithm to compute its long-run average distribution. The modeling approach and the computation of latency distributions have been implemented in a tool-chain relying on the CADP toolbox. Using this tool-chain, we studied communication aspects of an industrial hardware design, the xSTtream architecture, developed at STMicroelectronics.La validation, incluant vérification fonctionnelle et évaluation de performance, est un processus critique pour la conception de designs matériels complexes : un design fonctionnellement correct peut s'avérer incapable d'atteindre la performance ciblée. Plus un problème dans un design est identifié tard, plus son coût de correction est élevé. La validation de designs devrait donc être entreprise le plus tôt possible dans le flot de conception. Cette thèse présente un formalisme de modélisation par composition, couvrant les aspects fonctionnels et temporisés des systèmes matériels, et définit une approche d'évaluation de performance afin d'analyser les modèles construits. Le formalisme de modélisation défini, appelé Interactive Probabilistic Chain (IPC), est une algèbre de processus a temps discret. Nous avons défini une bisimulation de branchement et prouvé sa congruence par rapport à l'opérateur de composition parallèle, nous permettant une approche compositionnelle. les IPCs peuvent être vues comme une transposition des Interactive Markov Chains dans un espace de temps discret. Pour l'évaluation de performance, une IPC complètement spécifiée est transformée en une chaîne de Markov à temps discret, qui peut être analysée. De plus, nous avons défini une mesure de perfor- mance, appelée latence, et un algorithme permettant de calculer sa distribution moyenne sur le long terme. A l'aide d'outils permettant de traiter les IPCs, développés sur la base de la boîte à outils CADP, nous avons étudié les aspects de communication d'un design industriel, l'architecture xSTream, développée chez STMicroelectronics