Towards Performance Prediction of Compositional Models in GALS Designs

Nicolas Coste

Thèse de doctorat en informatique de l'Université de Grenoble, June 2010.

Abstract:

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.

223 pages

PDF

PostScript