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 proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publication25th Symposium on Integrated Circuits and Systems Design (SBCCI 2012
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Number of pages6
ISBN (Electronic)978-1-4673-2608-7
ISBN (Print)978-1-4673-2606-3
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event25th Symposium on Integrated Circuits and Systems Design (SBCCI) - Brasilia, Brazil
Duration: 30 Aug 20122 Sep 2012

Conference

Conference25th Symposium on Integrated Circuits and Systems Design (SBCCI)
CountryBrazil
CityBrasilia
Period30/08/122/09/12

Fingerprint Dive into the research topics of 'A formally verified deadlock-free routing function in a fault-tolerant NoC architecture'. Together they form a unique fingerprint.

Cite this