1. A method for preserving critical inputs in a digital design, said method comprising: receiving an initial design including one or more primary inputs which cannot be eliminated, one or more primary inputs which can be eliminated, one or more targets, and one or more state elements; identifying a cut of said initial design including one or more cut gates; computing a relation of one or more values producible to said one or more cut gates in terms of said one or more primary inputs which cannot be eliminated, said one or more primary inputs which can be eliminated and said one or more state elements; synthesizing said relation to form a gate set; forming an abstracted design from said gate set; and performing verification on said abstracted design to generate verification results.