Deadlock Verification for Dummies: The Easy Way Using SVA and Formal

RTL simulation cannot directly tell if a digital system is deadlocked – you can only observe that nothing has happened for a long time (so when should you get worried that nothing is happening?), and you cannot can’t differentiate between situations where your system is truly locked up from a situation where the right stimulus hasn’t come along to take the design out of a local minimum.

Additionally, simulation is dependent on the engineer knowing the right stimulus to trigger a particular problem. 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 non-standard 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 SystemVerilog Assertions (SVA). In this paper 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!

Introduction

The Dining Philosophers Problem1 has long been used as a mechanism in computer science and other disciplines for teaching deadlock and various mechanisms for preventing it. The problem definition has 5 silent philosophers sitting around a table. In front of them are plates of spaghetti and a fork on one side and a spoon on the other. The philosophers can either eat or think.

In order to eat, they need both a spoon and a fork. The philosopher can eat or think for as long as they like. The challenge is to develop a solution such that no philosopher starves. One issue might be that the philosopher switches hands with the fork and spoon so another philosopher would have both of either which is no good. Hence the development of the spork! A classic deadlock scenario in this case is all philosophers have a spork in their left hand, waiting for someone to put theirs down so someone can eat. In short, this case is a model for system deadlock when arbitrating between limited shared resources, and is something that happens in various scenarios in common digital designs.

The problem as defined by system deadlock or lockup is notoriously difficult to detect with RTL VHDL or Verilog simulations. However, exhaustive formal-based analysis is uniquely qualified to deliver results in this domain. Specifically, deadlock properties – concise, human and machine-readable descriptions of the desired design behavior you want to verify – have been extensively studied and can be precisely specified using mathematical languages such as linear-temporal logic² (LTL) or computational-tree logic³ (CTL).

Unfortunately, LTL and CTL are academic constructs, and as such are too cumbersome and lack support for use in industrial verification. Alternatively, formal verification engineers often try to leverage two foundational formal analyses supported by most commercial verification tools: “liveness” (formally prove something good will eventually happen) and “safety” (formally prove something bad will never happen). Unfortunately, the expertise required to manually effectively combine these for deadlock verification is substantial, and even in the hands of an expert the approach is error prone.

Hence, this paper discusses the application of new automation that leverages familiar, industry-standard SystemVerilog Assertion (SVA) code to specify constraints and properties to detect deadlock in RTL designs – while still leveraging the concepts behind LTL, CTL, liveness, and safety analyses under-the-hood.