Effective Liveness Verification Using a Transformation-Based Framework

Liveness properties such as "will every request eventually get a grant?" are crucial to the verification of a variety of design types. Liveness properties may only be falsified by infinite-length counterexamples, represented using lasso-shaped traces with a prefix (e.g., showing a particular request) followed by a repeating suffix loop (e.g., showing no grant). A variety of techniques have been developed to solve liveness properties, including BDD-based model checkers, various bounded liveness checking methods, and liveness-to-safety conversion. Nonetheless, the verification of such properties is computationally very challenging, no single algorithm works best, and many industrialsized liveness problems remain practically unsolvable. In this paper, we detail three approaches to solve liveness properties in our verification toolset SixthSense. The first is in the context of dynamic verification, enhancing a simulation engine to support native liveness checking. The second approach is formal, using abstraction-guided liveness-to-safety conversion for greater scalability. The third approach leverages complementary transformation algorithms to enhance the scalability of liveness checking algorithms. We additionally address automated verification of liveness properties on designs with memories, which has not received significant prior research. Experiments are provided to confirm the effectiveness of our techniques.