Fault-Tolerant Routing Algorithm for a Network-on-Chip

Organisation:	University of Utah (United States) CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
Method:	LNT MCL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Hardware Design
Period:	2013-2014
Size:	1350 lines of LNT code up to 6,295,773 states and 83,386,208 transitions
Description:	A fault-tolerant routing algorithm in Network-on-Chip architectures provides adaptivity for on-chip communications. Because adding fault-tolerance to a routing algorithm increases its complexity and makes it prone to deadlock and other problems, formal verification techniques are needed to check the correctness of the algorithm. This case study analyzes an extension of the link-fault tolerant multiflit wormhole routing algorithm for the Network-on-Chip architecture introduced by Wu et al that supports multiflit wormhole routing. To keep the state space manageable, a model of the routing algortihm was constructed in several steps, applying different abstractions (structural and with respect to data). This case study presents several lessons learned during this modeling process. A first lesson was the discovery of a package leakage path that could lead to the complete loss of a packet and a deadlock. This error in the design of an arbiter was corrected in the subsequent models. A second lesson was the necessity of a buffering capacity in an arbiter; this insight also led to a redesign of the arbiters. The resultant changes on the router and arbiter models uncovered interesting symmetries. Finally, this case study explores how deadlock freedom and tolerance of a single-link fault can be verified for a Network-on-Chip architecture.
Conclusions:	The construction and refinement of the formal model taught the designers several valuable lessons. In particular, without the diagnostics provided by CADP, it would have been very challenging to discover the flaws in the original arbiter design.
Publications:	[Zhang-Serwe-Wu-et-al-14] Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers. "Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip". Proceedings of the 19th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2014 (Florence, Italy), volume 8718 of Lecture Notes in Computer Science, pages 48-62, Springer-Verlag, September 2014. Available on-line at: http://cadp.inria.fr/publications/Zhang-Serwe-Wu-et-al-14.html [Zhang-Serwe-Wu-et-al-16] Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers. "An Improved Fault-Tolerant Routing Algorithm for a Network-on-Chip derived with Formal Analysis". Science of Computer Programming, Elsevier, 2016, Volume 118, March 2016. Available on-line at: http://cadp.inria.fr/publications/Zhang-Serwe-Wu-et-al-16.html [Zhang-16] Zhen Zhang. "Verification Methodologies for Fault-Tolerant Network-on-Chip Systems". PhD thesis of the University of Utah, USA, May 2016. Available on-line at: http://www.async.ece.utah.edu/wp-content/uploads/2016/08/zhangZhenDissertation.pdf or from the CADP Web site in PDF or PostScript
Contact:	Zhen Zhang Department of Electrical and Computer Engineering University of Utah Salt Lake City, UT 84112 United States of America E-mail: Zhen.Zhang@utah.edu
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page