Deadlock bugs are the scariest bugs, and the most difficult to find.
Formal verification techniques have clear advantages over simulation-based verification techniques for finding deadlock bugs, but the traditional formal methods used in industry are difficult to apply and debug.
This presentation shows how a new formal-tool feature substantially simplifies the application of formal verification to detect deadlocks.
We applied this technique to the verification of various units in a high-performance CPU design currently under development. It allowed us to more efficiently find RTL bugs, and formal testbench bugs; and, it made the debugging task shorter and less tedious.
Hide abstract »