A fault-tolerant routing algorithm in Network-on-Chip architectures provides adaptivity for on-chip communications. Adding fault-tolerance adaptivity to a routing algorithm increases its design complexity and makes it prone to deadlock and other problems if improperly implemented. Formal verification techniques are needed to check the correctness of the design. This paper performs formal analysis on an extension of the link-fault tolerant Network-on-Chip architecture introduced by Wu et al that supports multiflit wormhole routing. This paper describes several lessons learned during the process of constructing a formal model of this routing architecture. Finally, this paper presents how the deadlock freedom and tolerance to a single-link fault is verified for a two-by-two mesh version of this routing architecture. © 2014 Springer International Publishing.
CITATION STYLE
Zhang, Z., Serwe, W., Wu, J., Yoneda, T., Zheng, H., & Myers, C. (2014). Formal analysis of a fault-tolerant routing algorithm for a network-on-chip. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8718 LNCS, pp. 48–62). Springer Verlag. https://doi.org/10.1007/978-3-319-10702-8_4
Mendeley helps you to discover research relevant for your work.