Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip

Zhen Zhang 1, * Wendelin Serwe 2, * Jian Wu 3 Tomohiro Yoneda 4 Hao Zheng 5 Chris Myers 1, *
* Auteur correspondant
1 Department of Electrical and Computer Engineering
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
3 Marvell Technology Group Ltd.
4 NII - National Institute of Informatics
5 Department of Computer Science and Engineering
Abstract : 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.
Keywords : LNT process algebra fault-tolerant routing Network-on-Chip formal verification
Type de document :
Communication dans un congrès
Frédéric Lang; Francesco Flammini. 19th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2014, Sep 2014, Florence, Italy. Springer, 8718, pp.48-62, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-10702-8_4〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01064829
Contributeur : Wendelin Serwe <>
Soumis le : mercredi 17 septembre 2014 - 11:39:21
Dernière modification le : mercredi 11 avril 2018 - 01:54:08
Document(s) archivé(s) le : jeudi 18 décembre 2014 - 10:47:02

Fichiers

fmics2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UGA | LIG | CONVECS | LIG_SRCPR | INRIA-RENGRE

Citation

Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, et al.. Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip. Frédéric Lang; Francesco Flammini. 19th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2014, Sep 2014, Florence, Italy. Springer, 8718, pp.48-62, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-10702-8_4〉. 〈hal-01064829〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

425

Téléchargements de fichiers

415

Contact


archive-ouverte@inria.fr