Abstract

This paper first presents a binary decision diagram-based implicit algorithm to compute all maximal strongly connected components (SCCs) of directed graphs. The algorithm iteratively applies reachability analysis and sequentially identifies SCCs. Experimental results suggest that the algorithm dramatically outperforms the only existing implicit method which must compute the transitive closure of the adjacency-matrix of the graphs. This paper then applies this SCC algorithm to solve the bad cycle detection problem encountered in formal verification. Experimental results show that our new bad cycle detection algorithm is typically significantly faster than the state-of-the-art, sometimes by more than a factor of ten.

Date

January 1, 1970

Authors

Aiguo Xie, Peter A Beerel

Journal

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

Volume

19

Issue

10

Pages

1225-1230

Publisher

IEEE