8. The computer-implemented method of claim 3 , wherein performing the localization abstraction process comprises: initializing the localization abstraction process with every design component replaced by a cutpoint; performing satisfiability-based (SAT-based) bounded model checking (BMC) for a first timestep on the abstracted design; identifying and analyzing spurious counterexamples; refining the localization abstraction by adding sufficient design components, to the abstracted design to eliminate the spurious counterexamples, wherein the design components added are selected based on an analysis of assigned priorities for the design components; in response to completion of elimination of spurious counterexamples at a specific timestep, performing proof-based abstraction (PBA) up to that specific timestep to eliminate unnecessary logic from the abstracted design; and incrementing a timestep and iterating through processes including the performing SAT-based BMC, the identifying and analyzing, the refining, and the performing PBA processes up to the configured resource limit, wherein counterexample based abstraction (CBA) and proof-based abstraction (PBA) are interleaved utilizing the assigned priorities of the design components to complete the refining.
8. The computer-implemented method of claim 3 , wherein performing the localization abstraction process comprises: initializing the localization abstraction process with every design component replaced by a cutpoint; performing satisfiability-based (SAT-based) bounded model checking (BMC) for a first timestep on the abstracted design; identifying and analyzing spurious counterexamples; refining the localization abstraction by adding sufficient design components, to the abstracted design to eliminate the spurious counterexamples, wherein the design components added are selected based on an analysis of assigned priorities for the design components; in response to completion of elimination of spurious counterexamples at a specific timestep, performing proof-based abstraction (PBA) up to that specific timestep to eliminate unnecessary logic from the abstracted design; and incrementing a timestep and iterating through processes including the performing SAT-based BMC, the identifying and analyzing, the refining, and the performing PBA processes up to the configured resource limit, wherein counterexample based abstraction (CBA) and proof-based abstraction (PBA) are interleaved utilizing the assigned priorities of the design components to complete the refining. 9. The computer-implemented method of claim 8 , wherein refining the localization abstraction comprises: in response to encountering a spurious counterexample within the abstracted design: identifying cutpoints introduced to the design that correspond to design components having a next highest priority; assigning the next highest priority as the priority for use in determining which design components to retain; and replacing each identified cutpoints with the corresponding design components to generate a refined abstraction.