Deadlock verification for dummies – The easy way using SVA and Formal

RTL simulation cannot directly tell if a digital system is deadlocked. This paper shares new formal automation technology that leverages industry-standard System Verilog Assertion code to specify constraints and properties that detect deadlock in RTL designs, while leveraging linear-temporal logic, computational-tree logic, liveness, and safety analyses under-the-hood.