1. A computer-implemented method of invariant-guided abstraction within a design under verification, the method comprising: initiating a verification process for an identified design; generating by a processor of a computing device one or more invariants corresponding to the design under verification by executing a proof algorithm with an input comprising at least a portion of the design and a specified resource limit; deterministically assigning priority information to the one or more invariants generated, and to components of said design referenced by said invariants; and generating an abstracted design model by performing invariant-guided localization abstraction on a design model utilizing the assigned priority information as a localization hint that results in abstractions that are at least one of (a) smaller abstractions and (b) easier to verify abstractions.
1. A computer-implemented method of invariant-guided abstraction within a design under verification, the method comprising: initiating a verification process for an identified design; generating by a processor of a computing device one or more invariants corresponding to the design under verification by executing a proof algorithm with an input comprising at least a portion of the design and a specified resource limit; deterministically assigning priority information to the one or more invariants generated, and to components of said design referenced by said invariants; and generating an abstracted design model by performing invariant-guided localization abstraction on a design model utilizing the assigned priority information as a localization hint that results in abstractions that are at least one of (a) smaller abstractions and (b) easier to verify abstractions. 2. The computer-implemented method of claim 1 , wherein executing the proof algorithm comprises: establishing the specified resource limit to enable less than a complete run of the proof algorithm on the design model, wherein a pre-specified resource limit is selected from among a time limit, a depth limit, and a hardware resource usage limit; and executing the proof algorithm for only a preset limit, wherein the proof algorithm iterates over a series of timesteps corresponding to states extending from an initial state (t0) to a subsequent state (tk) at which a proof condition holds true over a first k timesteps for a set of bounded invariants identified at the respective states, wherein said set of bounded invariants hold true for a particular state from the initial state and wherein the invariants each refer to one or more components of said design.