Patent ID: 8185852

Claim:
A data processing system for performing verification, said data processing system comprising: a processor; and data storage coupled to the processor, the data storage including program code stored within the data storage that, when executed by the processor, causes the data processing system to obtain an overapproximated netlist with low input count by: selecting a set of gates to add to a first localization netlist; forming a refinement netlist by adding the selected set of gates to the first localization netlist; computing a min-cut with sinks comprising one or more gates in said refinement netlist and sources comprising one or more inputs of an original netlist and one or more registers of said original netlist which are not part of said refinement netlist, wherein computing said min-cut further comprises, upon determining a register to be within said set of gates, computing said min-cut on both a next state and an initial value cone of said register; and obtaining a final localized netlist by adding one or more gates to said refinement netlist to grow said refinement netlist until reaching one or more cut-gates of said min-cut; wherein said program code causes the data processing system to perform the forming, computing, and obtaining iteratively in response to detection of one or more spurious counterexamples on said final localized netlist.