Released on June 2nd, 2020
RTL simulation cannot directly tell if a digital system is deadlocked — you can only observe that nothing has happened for a long time, and this is highly dependent on the “right” stimulus being applied. In contrast, Formal verification has the ability to find deadlock conditions in your design. However, the traditional iterative approach using written liveness and safety properties in combination with manually written constraints can be time consuming and error prone even in expert hands. While there are nonstandard assertion languages that can be used, these are reserved for academic practitioners and not useful for the typical RTL-aware design and verification engineers who use industry standard System Verilog Assertions (SVA). In this session we will show how combining the above concepts using normal SVA liveness properties allows for RTL engineers to achieve the benefit of formal deadlock analysis without the iterative component or learning a non-standard assertion language. Deadlock verification for dummies!
