Database of Case Studies Achieved Using CADP

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


Last modified: Thu Feb 11 12:22:03 2021.


Back to the CADP case studies page