Patent ID: 7448005

Claim:
A method of performing verification, said method comprising: creating and designating as a current abstraction a first abstraction of an initial design netlist containing a first target; unfolding said current abstraction by a selectable depth; verifying a composite target using a satisfiability solver; and in response to determining that said composite target is unreachable, increasing said selectable depth; in response to determining that said verifying step has hit said composite target, examining a counterexample to identify one or more reasons for said first target to be asserted; building one or more refinement pairs by examining said counterexample; building a second abstraction by composing said refinement pairs; building a new target over one or more cutpoints in said first abstraction that is asserted when said one or more cutpoints assume values in said counterexample; verifying said new target with said satisfiability solver; in response to ascertaining that said new target has been not been hit: creating a new unfolded target in said second abstraction; verifying said new unfolded target in said second abstraction; in response ascertaining that said new unfolded target is not hit and ascertaining that said new unfolded target is unreachable, increasing said selectable depth.