A Compositional Approach to Asynchronous Design Verification with Automated State Space Reduction

Model checking is the most effective means of verifying the correctness of asynchronous designs, and state space exploration is central to model checking. Although model checking can achieve very high verification coverage, the high degree of concurrency in asynchronous designs often leads to state explosion during state space exploration. To inhibit this explosion, our approach builds on the ideas of compositional verification. In our approach, a design modeled in a high level description is partitioned into a set of parallel components. Before state space exploration, each component is paired with an over-approximated environment to decouple it from the rest of the design. Then, a global state transition graph is constructed by reducing and incrementally composing component state transition graphs. We take great care during reduction and composition to preserve all failures found during the initial state space exploration of each component. To further reduce complexity, interface constraints are automatically derived for the over-approximated environment of each component. We prove that our approach is conservative in that false positive results are never produced. The effectiveness of our approach is demonstrated by the experimental results of several case studies showing that our approach can verify designs that cannot be handled by traditional at approaches. The experiments also show that constraints can reduce the size of the global state transition graph and prevent some false failures.