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.
|Title of host publication||International Conference on Formal Methods in Computer-Aided Design (FMCAD '11, Austin TX, USA, October 30-November 02, 2011)|
|Editors||P. Bjesse, A. Slobodová|
|Place of Publication||Austin TX|
|Publication status||Published - 2011|