Sequential circuit verification using symbolic model checking

TLDR

The authors modified the Clarke–Emerson–Sistla temporal logic model‑checking algorithm to use binary decision diagrams for state‑graph representation and extended it to support full CTL with fairness constraints. Using this BDD‑based approach, the technique verifies sequential circuits with up to ~5×10²⁰ states, handles important liveness and fairness properties beyond CTL expressiveness, and demonstrates strong empirical performance on both synchronous and asynchronous designs.

Abstract

The temporal logic model checking algorithm developed by Clarke, Emerson, and Sistla [9] is modified to represent a state graph using binary decision diagrams (BDD's) [4]. Because this representation captures some of the regularity in the state space of sequential circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 1020 states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to handle a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.