Abstract
Systems and Networks on Chips (NoCs) are a prime design focus of many hardware manufacturers. In addition to functional verification, which is a difficult necessity, the chip designers are facing extremely demanding performance prediction challenges, such as the need to estimate the latency of memory accesses over the NoC. This paper attacks this problem in the setting of designing globally asynchronous, locally synchronous systems (GALS). We describe foundations and applications of a combination of compositional modeling, model checking, and Markov process theory, to arrive at a viable approach to compute performance quantities directly on industrial, functionally verified GALS models.
Chapter PDF
Similar content being viewed by others
Keywords
- Performance Prediction
- Markov Decision Process
- Operational Semantic
- Steady State Probability
- Virtual Channel
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Coste, N., Garavel, H., Hermanns, H., Hersemeule, R., Thonnart, Y., Zidouni, M.: Quantitative evaluation in embedded system design: Validation of multiprocessor multithreaded architectures. In: DATE (March 2008)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier Science, Amsterdam (1994)
Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hermanns, H., Lohrey, M.: Priority and maximal progress are completely axiomatisable (extended abstract). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 237–252. Springer, Heidelberg (1998)
ISO/IEC. LOTOS — a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807 (1989)
Jonsson, B., Yi, W., Larsen, K.G.: Probabilistic Extensions of Process Algebras, ch. 11, pp. 685–710. North Holland, Amsterdam (2001)
Larsen, K.G., Skou, A.: Compositional verification of probabilistic processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 456–471. Springer, Heidelberg (1992)
Nicollin, X., Sifakis, J.: An overview and synthesis on timed process algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 376–398. Springer, Heidelberg (1992)
Nicollin, X., Sifakis, J.: The algebra of timed processes ATP: Theory and application. Information and Computation 114(1), 131–178 (1994)
Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)
Swartz, K.L., Cottrell, R.L., Dart, M.: Adventures in the evolution of a high-bandwidth network for central servers. In: LISA. USENIX (1994)
Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. In: QAPL 2008. Electronic Notes in Theoretical Computer Science, vol. 220, pp. 129–143 (2008)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics (extended abstract). In: IFIP congress, pp. 613–618 (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W. (2009). Towards Performance Prediction of Compositional Models in Industrial GALS Designs. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)