University of Utah (United States)
CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
1350 lines of LNT code
up to 6,295,773 states and 83,386,208 transitions
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.
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.
Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and
"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
Department of Electrical and Computer Engineering
University of Utah
Salt Lake City, UT 84112
United States of America
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|