Implicit enumeration of strongly connected components and an application to formal verification

This paper first presents a binary decision diagram-based implicit algorith m to compute all maximal strongly connected components (SCCs) of directed g raphs. The algorithm iteratively applies reachability analysis and sequenti ally identifies SCCs. Experimental results suggest that the algorithm drama tically outperforms the only existing implicit method which must compute th e transitive closure of the adjacency-matrix of the graphs. This paper then applies this SCC algorithm to solve the bad cycle detection problem encoun tered in formal verification. Experimental results show that our new bad cy cle detection algorithm is typically significantly faster than the state-of -the-art [1], sometimes by more than a factor of ten.