This HTML5 document contains 44 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Subject Item

n2:id

rdf:type

frbr:Work rdac:C10001

marcrel:ths

n5:id n8:id n10:id n13:id n14:id n25:id n28:id

marcrel:pra

n18:id

marcrel:aut

n9:id

skos:altLabel

Towards performance prediction of compositional models in GALS designs

dc:subject

Evaluation de performance Hardware architectures Latence Chaîne de Markov 3 Markov chain Bisimulation 4 Architectures matérielles 5 Process algebra Algèbre de processus 1 Interactive probabilistic chain 2 Architecture matérielle Algèbre de processus Performance evaluation Langages de description de matériel informatique Latency Interactive probabilistic chain (IPC) Chaîne de Markov Thèses et écrits académiques

skos:prefLabel

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

dcterms:language

n23:eng

dcterms:subject

n16:id n27:id

dc:title

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

marcrel:dgg

n6:id

marcrel:opn

n7:id n24:id

skos:note

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. 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.

dc:type

Text

n19:P1001

n20:T1009

rdaw:P10219

2010

rdau:P60049

n22:1020