Formal deadlock verification is an effective and pragmatic method for discovering deadlocks in complex SoC IP blocks. For the MC design, the authors used Level 4 formal techniques to find deadlock bugs that were undetected through many millions of cycles of dynamic testing.
Deadlock in IC design occurs when there is a circular-wait condition. It may happen when there is communication between blocks. This paper from DVcon Europe looks at the challenges to be addressed when verifying a design for absence of deadlock through traditional dynamic testing