Abstract
Network on Chip (NoC) plays a significant role in improving computation speed in Tiled Chip Multiprocessor (TCMP) by acting as an efficient interconnection network between the tiles. Designing a NoC satisfying all important functional properties with high efficiency is challenging. Some of the crucial properties to be fulfilled for proper functioning of NoC with efficiency are namely progress, mutual exclusion, starvation freedom, deadlock freedom, congestion freedom and livelock freedom. Exhaustive checking of such system properties in NoC can be done by formal verification method. In existing verification works, NoC are modeled in abstract level. Therefore, the properties verified does not guarantee that they work in real hardware. In our work, we have modeled NoC router using Executable Micro Architectural Specification (xMAS) primitives so that our design becomes near to register transfer level (RTL). In this model, we have verified progress property with help of NuSMV model checker. Experimental results show that our model is scalable for progress verification in Mesh and Ring topologies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Chatterjee, S., Kishinevsky, M., Ogras, U.: xMAS: quick formal modelling of communication fabrics to enable verification. IEEE Des. Test Comput. 29(3), 8088 (2012)
Borrione, D., Helmy, A., Pierre, L., Schmaltz, J.: A generic model for formally verifying NoC communication architectures: a case study. In: First International Symposium on Networks-on-Chip (NOCS 2007), pp. 127–136 (2007)
Borrione, D., Helmy, A., Pierre, L., Schmaltz, J.: Executable formal specification and validation of NoC communication infrastructures. In: Proceedings of the 21st Annual Symposium on Integrated Circuits and System Design, pp. 176–181 (2008)
Verbeek, F., Schmaltz, J.: Easy formal specification and validation of unbounded networks-on-chips architectures. ACM Trans. Des. Autom. Electron. Syst. 17, 1:1–1:28 (2012)
Lan, Y.-C., Lo, S.-H., Lin, Y.-C., Hu, Y.-H., Chen, S.-J.: BiNoC: a bidirectional NoC architecture with dynamic self-reconfigurable channel. In: NOCS 2009, pp. 266–275 (2009)
Chen, Y.R., Su, W.T., Hsiung, P.A., Lan, Y.C., Hu, Y.H., Chen, S.J.: Formal modeling and verification for network-on-chip. In: The 2010 International Conference on Green Circuits and Systems, pp. 299–304 (2010)
Holcomb, D.E., Gotmanov, A., Kishinevsky, M., Seshia, S.A.: Compositional performance verification of NoC designs. In: MEMCODE 2012, pp. 1–10 (2012)
Ray, S., Brayton, R.K.: Scalable progress verification in credit-based flow-control systems. In: DATE 2012, pp. 905–910 (2012)
Gotmanov, A., Chatterjee, S., Kishinevsky, M.: Verifying deadlock-freedom of communication fabrics. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 214–231. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_16
Joosten, S.J.C., Schmaltz, J.: Scalable liveness verification for communication fabrics. In: DATE 2014, pp. 1–6 (2014)
Burns, F., Sokolov, D., Yakovlev, A.: GALS synthesis and verification for xMAS models. In: DATE 2015, pp. 1419–1424 (2015)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_44
Zhang, W., Hou, L., Wang, J., Geng, S., Wu, W.: Comparison research between XY and odd-even routing algorithm of a 2-dimension 3X3 mesh topology network-on-chip. In: 2009 WRI Global Congress on Intelligent Systems, vol. 3, pp. 329–333 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Das, S., Karfa, C., Biswas, S. (2017). xMAS Based Accurate Modeling and Progress Verification of NoCs. In: Kaushik, B., Dasgupta, S., Singh, V. (eds) VLSI Design and Test. VDAT 2017. Communications in Computer and Information Science, vol 711. Springer, Singapore. https://doi.org/10.1007/978-981-10-7470-7_74
Download citation
DOI: https://doi.org/10.1007/978-981-10-7470-7_74
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-7469-1
Online ISBN: 978-981-10-7470-7
eBook Packages: Computer ScienceComputer Science (R0)