Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching

F. Verbeek, J. Schmaltz

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    7 Citations (Scopus)


    Wormhole switching is a switching technique nowadays commonly used in networks-on-chips (NoCs). It is efficient but prone to deadlock. The design of a deadlock-free adaptive routing function constitutes an important challenge. We present a novel algorithm for the automatic verification that a routing function is deadlock-free in wormhole networks. A sufficient condition for deadlock-free routing and an associated algorithm are defined. The algorithm is proven complete for the condition. The condition, the algorithm, and the correctness theorem have been formalized and checked in the logic of the ACL2 interactive theorem proving system. The algorithm has a time complexity in O(N3), where N denotes the number of nodes in the network. This outperforms the previous solution of Taktak et al. by one degree. Experimental results confirm the high efficiency of our algorithm. This paper presents a formally proven correct algorithm that detects deadlocks in a 2D-mesh with about 4000 nodes and 15000 channels within seconds.
    Original languageEnglish
    Title of host publicationNOCS 2011 (Fifth ACM/IEEE International Symposium on Networks-on-Chip, Pittsburgh PA, USA, May 1-4, 2011)
    PublisherIEEE Computer Society
    ISBN (Print)978-1-4503-0720-8
    Publication statusPublished - 2011


    Dive into the research topics of 'Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching'. Together they form a unique fingerprint.

    Cite this