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; porting one or more learned clauses and one or more invariants to said second abstraction; choosing as said current abstraction said second abstraction; and verifying said current abstraction with said satisfiability solver.