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

F. Verbeek, J. Schmaltz

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    7 Citaten (Scopus)

    Samenvatting

    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.
    Originele taal-2Engels
    TitelNOCS 2011 (Fifth ACM/IEEE International Symposium on Networks-on-Chip, Pittsburgh PA, USA, May 1-4, 2011)
    UitgeverijIEEE Computer Society
    Pagina's25-32
    ISBN van geprinte versie978-1-4503-0720-8
    StatusGepubliceerd - 2011

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit