A formally verified deadlock-free routing function in a fault-tolerant NoC architecture

A. Alhussien; N. Bagherzadeh; F. Verbeek; B. van Gastel; J. Schmaltz

doi:10.1109/SBCCI.2012.6344433

A formally verified deadlock-free routing function in a fault-tolerant NoC architecture

A. Alhussien, N. Bagherzadeh, F. Verbeek, B. van Gastel, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

Abstract

A novel fault-tolerant adaptive wormhole routing function for Networks-on-Chips (NoCs) is presented. The routing function guarantees absence of deadlocks and livelocks up to two faulty channels. The routing logic does not require reconfiguration when a fault occurs. The routes themselves are dynamic. Based on the faults in the network, alternative routes are used to reroute packets. Routing decisions are based only on local knowledge, which allows for fast switching. Our approach does not use any costly virtual channels. As we do not prohibit cyclic dependencies, the routing function provides minimal routing from source to destination even in the presence of faults. We have implemented the architecture design using synthesizable HDL. To ensure deadlock freedom, we have extended a formally verified deadlock detection algorithm to deal with fault tolerant designs. For a 20×20 mesh, we have formally proven deadlock freedom of our design in all of the 2,878,800 configurations in which two channels are faulty. We supply experimental results showing the performance of our architecture.

Original language	English
Title of host publication	25th Symposium on Integrated Circuits and Systems Design (SBCCI 2012
Place of Publication	Piscataway
Publisher	Institute of Electrical and Electronics Engineers
Number of pages	6
ISBN (Electronic)	978-1-4673-2608-7
ISBN (Print)	978-1-4673-2606-3
DOIs	https://doi.org/10.1109/SBCCI.2012.6344433
Publication status	Published - 2012
Externally published	Yes
Event	25th Symposium on Integrated Circuits and Systems Design (SBCCI) - Brasilia, Brazil Duration: 30 Aug 2012 → 2 Sept 2012

Conference

Conference	25th Symposium on Integrated Circuits and Systems Design (SBCCI)
Country/Territory	Brazil
City	Brasilia
Period	30/08/12 → 2/09/12

Access to Document

10.1109/SBCCI.2012.6344433

Cite this

@inproceedings{e567802a43ed4728a1d1541e9a42da31,

title = "A formally verified deadlock-free routing function in a fault-tolerant NoC architecture",

abstract = "A novel fault-tolerant adaptive wormhole routing function for Networks-on-Chips (NoCs) is presented. The routing function guarantees absence of deadlocks and livelocks up to two faulty channels. The routing logic does not require reconfiguration when a fault occurs. The routes themselves are dynamic. Based on the faults in the network, alternative routes are used to reroute packets. Routing decisions are based only on local knowledge, which allows for fast switching. Our approach does not use any costly virtual channels. As we do not prohibit cyclic dependencies, the routing function provides minimal routing from source to destination even in the presence of faults. We have implemented the architecture design using synthesizable HDL. To ensure deadlock freedom, we have extended a formally verified deadlock detection algorithm to deal with fault tolerant designs. For a 20×20 mesh, we have formally proven deadlock freedom of our design in all of the 2,878,800 configurations in which two channels are faulty. We supply experimental results showing the performance of our architecture.",

author = "A. Alhussien and N. Bagherzadeh and F. Verbeek and {van Gastel}, B. and J. Schmaltz",

year = "2012",

doi = "10.1109/SBCCI.2012.6344433",

language = "English",

isbn = "978-1-4673-2606-3",

booktitle = "25th Symposium on Integrated Circuits and Systems Design (SBCCI 2012",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "25th Symposium on Integrated Circuits and Systems Design (SBCCI) ; Conference date: 30-08-2012 Through 02-09-2012",

}

Alhussien, A, Bagherzadeh, N, Verbeek, F, van Gastel, B & Schmaltz, J 2012, A formally verified deadlock-free routing function in a fault-tolerant NoC architecture. in 25th Symposium on Integrated Circuits and Systems Design (SBCCI 2012., 6344433, Institute of Electrical and Electronics Engineers, Piscataway, 25th Symposium on Integrated Circuits and Systems Design (SBCCI), Brasilia, Brazil, 30/08/12. https://doi.org/10.1109/SBCCI.2012.6344433

A formally verified deadlock-free routing function in a fault-tolerant NoC architecture. / Alhussien, A.; Bagherzadeh, N.; Verbeek, F. et al.
25th Symposium on Integrated Circuits and Systems Design (SBCCI 2012. Piscataway: Institute of Electrical and Electronics Engineers, 2012. 6344433.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A formally verified deadlock-free routing function in a fault-tolerant NoC architecture

AU - Alhussien, A.

AU - Bagherzadeh, N.

AU - Verbeek, F.

AU - van Gastel, B.

AU - Schmaltz, J.

PY - 2012

Y1 - 2012

N2 - A novel fault-tolerant adaptive wormhole routing function for Networks-on-Chips (NoCs) is presented. The routing function guarantees absence of deadlocks and livelocks up to two faulty channels. The routing logic does not require reconfiguration when a fault occurs. The routes themselves are dynamic. Based on the faults in the network, alternative routes are used to reroute packets. Routing decisions are based only on local knowledge, which allows for fast switching. Our approach does not use any costly virtual channels. As we do not prohibit cyclic dependencies, the routing function provides minimal routing from source to destination even in the presence of faults. We have implemented the architecture design using synthesizable HDL. To ensure deadlock freedom, we have extended a formally verified deadlock detection algorithm to deal with fault tolerant designs. For a 20×20 mesh, we have formally proven deadlock freedom of our design in all of the 2,878,800 configurations in which two channels are faulty. We supply experimental results showing the performance of our architecture.

AB - A novel fault-tolerant adaptive wormhole routing function for Networks-on-Chips (NoCs) is presented. The routing function guarantees absence of deadlocks and livelocks up to two faulty channels. The routing logic does not require reconfiguration when a fault occurs. The routes themselves are dynamic. Based on the faults in the network, alternative routes are used to reroute packets. Routing decisions are based only on local knowledge, which allows for fast switching. Our approach does not use any costly virtual channels. As we do not prohibit cyclic dependencies, the routing function provides minimal routing from source to destination even in the presence of faults. We have implemented the architecture design using synthesizable HDL. To ensure deadlock freedom, we have extended a formally verified deadlock detection algorithm to deal with fault tolerant designs. For a 20×20 mesh, we have formally proven deadlock freedom of our design in all of the 2,878,800 configurations in which two channels are faulty. We supply experimental results showing the performance of our architecture.

U2 - 10.1109/SBCCI.2012.6344433

DO - 10.1109/SBCCI.2012.6344433

M3 - Conference contribution

SN - 978-1-4673-2606-3

BT - 25th Symposium on Integrated Circuits and Systems Design (SBCCI 2012

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

T2 - 25th Symposium on Integrated Circuits and Systems Design (SBCCI)

Y2 - 30 August 2012 through 2 September 2012

ER -

A formally verified deadlock-free routing function in a fault-tolerant NoC architecture

Abstract

Conference

Access to Document

Fingerprint

Cite this