Automatic partitioning for efficient combinational verification

A majority of the state-of-the-art combinational verification techniques are based on the extraction and use of internal equivalences between two circuits. Verification can become difficult if the two circuits have none or very few internal correspondences. In this paper we investigate automatic circuit partitioning as a methodology to make otherwise intractable circuits relatively tractable to the verifier. We show that given any two circuits to be verified, finding the best partitions that minimize the verification runtime is NP-hard. Therefore, we propose efficient heuristics to utilize certain characteristics of typical circuit design styles to find good partitions for the circuits. A key difference between our approach and earlier approaches to circuit partitioning is that ours is fully automated and does not require any prior knowledge of the type of function being implemented by the circuit. Using circuit partitioning we are able to verify several hard industrial circuits that could not be verified otherwise.