Hunting deadlocks efficiently in microarchitectural models of communication fabrics

F. Verbeek, J. Schmaltz

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

    21 Citations (Scopus)


    Communication fabries constitute an important challenge for the design and verification of multi-core architectures. To enable their formal analysis, microarchitectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. We propose a novel algorithm to deadlock verification of microarchitectural designs. The basic idea of our algorithm is to capture the structure of the wait-for relations of a microarchitectural model in a labelled waitin-graph and to express a deadlock as a feasible closed subgraph of the waiting-graph. We apply our algorithm to academic and industrial Networks-on-Chip (NoC) designs. With examples we show that our tool is fast, scalable, and capable of detecting intricate message-dependent deadlocks. Deadlocks in networks with thousands of components are detected within a few seconds.
    Original languageEnglish
    Title of host publicationInternational Conference on Formal Methods in Computer-Aided Design (FMCAD '11, Austin TX, USA, October 30-November 02, 2011)
    EditorsP. Bjesse, A. Slobodová
    Place of PublicationAustin TX
    PublisherFMCAD Inc
    ISBN (Print)978-0-9835678-1-3
    Publication statusPublished - 2011


    Dive into the research topics of 'Hunting deadlocks efficiently in microarchitectural models of communication fabrics'. Together they form a unique fingerprint.

    Cite this