1. 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 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; and verifying said new target with said satisfiability solver.