Abstract
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 language | English |
---|---|
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 |
Publisher | FMCAD Inc |
Pages | 223-231 |
ISBN (Print) | 978-0-9835678-1-3 |
Publication status | Published - 2011 |