Abstract
As an efficient interconnection network, Network-on-Chip (NoC) provides significant flexibility for increasingly prevalent many-core systems. It is desirable to deploy fault-tolerance in a dependable safety-critical NoC design. However, this process can easily introduce deeply buried flaws that traditional simulation-based NoC design approaches may miss. This paper presents a case study on applying scalable formal verification that detects, corrects, and proves livelock in a dependable fault-tolerant NoC using the IVy verification tool. We formally verify correctness at the routing algorithm level. We first present livelock verification using refutation-based simulation scaled to a 15-by-15 two-dimensional NoC. We then present a novel zone-based approach to livelock verification in which finite coordinate-based routing conditions are abstracted as positional zones relative to a packet’s destination. This abstraction allows us to detect and remove livelock patterns on an arbitrarily large network. The resultant improved routing algorithm is free of livelock and maintains a high level of fault tolerance.
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
Alhussien, A., Verbeek, F., van Gastel, B., Bagherzadeh, N., Schmaltz, J.: Fully reliable dynamic routing logic for a fault-tolerant NoC architecture. J. Integr. Circuits Syst. 8(1), 43–53 (2013)
Berkeley Logic Synthesis and Verification Group: ABC: A system for sequential synthesis and verification (September 2020). http://www.eecs.berkeley.edu/~alanmi/abc/ and https://github.com/berkeley-abc/abc
Borrione, D., Helmy, A., Pierre, L., Schmaltz, J.: A formal approach to the verification of networks on chip. EURASIP J. Embed. Syst. 2009(1), 1–14 (2009). https://dl.acm.org/doi/10.1155/2009/548324
Boutekkouk, F.: Formal specification and verification of communication in Network-on-Chip: an overview. Int. J. Recent Contrib. Eng. Sci. IT (iJES) 6(4), 15–31 (2018). https://doi.org/10.3991/ijes.v6i4.9416
Bozga, M., Graf, S., Mounier, L.: IF-2.0: a validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 343–348. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_26
Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_5
Champelovier, D., et al.: Reference manual of the LNT to LOTOS translator (version 6.0). INRIA/VASY/CONVECS (June 2014)
Chatterjee, S., Kishinevsky, M., Ogras, U.Y.: Quick formal modeling of communication fabrics to enable verification. In: 2010 IEEE International High Level Design Validation and Test Workshop (HLDVT), pp. 42–49 (2010). https://doi.org/10.1109/HLDVT.2010.5496662
Din, C.C., Tapia Tarifa, S.L., Hähnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217–233. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_14
Dridi, M., Lallali, M., Rubini, S., Singhoff, F., Diguet, J.P.: Modeling and validation of a mixed-criticality NoC router using the IF language. In: Proceedings of the 10th International Workshop on Network on Chip Architectures. NoCArc 2017, Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145/3139540.3139543
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). https://doi.org/10.1007/s10009-012-0244-z
van Gastel, B., Schmaltz, J.: A formalisation of xMAS. In: Gamboa, R., Davis, J. (eds.) Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, 30–31 May 2013, EPTCS, vol. 114, pp. 111–126 (2013). https://doi.org/10.4204/eptcs.114.9
Helmy, A., Pierre, L., Jantsch, A.: Theorem proving techniques for the formal verification of NoC communications with non-minimal adaptive routing. In: DDECS, pp. 221–224. IEEE (2010)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521
Imai, M., Yoneda, T.: Improving dependability and performance of fully asynchronous on-chip networks. In: Proceedings of the 2011 17th IEEE International Symposium on Asynchronous Circuits and Systems, pp. 65–76. ASYNC 2011, IEEE Computer Society, Washington, DC, USA (2011). https://doi.org/10.1109/ASYNC.2011.15, http://dx.doi.org/10.1109/ASYNC.2011.15
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_8
Lecler, J.J., Baillieu, G.: Application driven network-on-chip architecture exploration & refinement for a complex SoC. Des. Autom. Embed. Syst. 15, 133–158 (2011). https://doi.org/10.1007/s10617-011-9075-5, https://link.springer.com/article/10.1007/s10617-011-9075-5
McMillan, K.L.: IVy (2019). http://microsoft.github.io/ivy/, https://github.com/kenmcmil/ivy
McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 190–202. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_12
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Tsai, W.C., Lan, Y.C., Hu, Y.H., Chen, S.J.: Networks on chips: structure and design methodologies. J. Electr. Comput. Eng. 2012, 15 (2012). https://doi.org/10.1155/2012/509465
Verbeek, F., Schmaltz, J.: A decision procedure for deadlock-free routing in wormhole networks. IEEE Trans. Parallel Distrib. Syst. 25(8), 1935–1944 (2014). https://doi.org/10.1109/TPDS.2013.121
Verbeek, F., Schmaltz, J.: Automatic verification for deadlock in Networks-on-Chips with adaptive routing and wormhole switching. In: Proceedings of the fifth ACM/IEEE International Symposium on Networks-on-Chip, pp. 25–32. NOCS 2011, Association for Computing Machinery, New York, NY, USA (2011). https://doi.org/10.1145/1999946.1999951
Verbeek, F., Schmaltz, J.: Easy formal specification and validation of unbounded Networks-on-Chips architectures. ACM Trans. Des. Autom. Electron. Syst. 17(1) (2012). https://doi.org/10.1145/2071356.2071357
Wu, J., Zhang, Z., Myers, C.: A fault-tolerant routing algorithm for a Network-on-Chip using a link fault model. In: Virtual Worldwide Forum for PhD Researchers in Electronic Design Automation (2011)
Yoneda, T., et al.: Network-on-Chip based multiple-core centralized ECUs for safety-critical automotive applications. In: Asai, S. (ed.) VLSI Design and Test for Systems Dependability, pp. 607–633. Springer, Tokyo (2019). https://doi.org/10.1007/978-4-431-56594-9_19
Zaman, A., Hasan, O.: Formal verification of circuit-switched Network on chip (NoC) architectures using SPIN. In: 2014 International Symposium on System-on-Chip, SoC 2014. Institute of Electrical and Electronics Engineers Inc. (December 2014). https://doi.org/10.1109/ISSOC.2014.6972449
Zhang, Z., Serwe, W., Wu, J., Yoneda, T., Zheng, H., Myers, C.: Formal analysis of a fault-tolerant routing algorithm for a Network-on-Chip. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 48–62. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10702-8_4
Zhang, Z., Serwe, W., Wu, J., Yoneda, T., Zheng, H., Myers, C.: An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysis. Sci. Comput. Program. 118, 24–39 (2016). https://doi.org/10.1016/j.scico.2016.01.002, http://www.sciencedirect.com/science/article/pii/S0167642316000125, Formal Methods for Industrial Critical Systems (FMICS 2014)
Acknowledgment
The authors would like to thank Ken McMillan for his assistance in understanding the IVy formal specification language and utilizing the IVy verification tool. Landon Taylor was supported in part by National Science Foundation grant (CAREER-1253024). Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. The authors would also like to thank Adobe Systems Incorporated for their support.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Taylor, L., Zhang, Z. (2022). Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms. In: Finkbeiner, B., Wies, T. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2022. Lecture Notes in Computer Science(), vol 13182. Springer, Cham. https://doi.org/10.1007/978-3-030-94583-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-94583-1_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-94582-4
Online ISBN: 978-3-030-94583-1
eBook Packages: Computer ScienceComputer Science (R0)