A method, system and computer program product for performing verification of an electronic design is disclosed. The method includes receiving a design, including a first target set, a primary input set, and a first register set comprising one or more registers. A binary decision diagram analysis of the design is generated. A recursive extraction of one or more next states of selected registers is generated using the binary decision diagram analysis of the first target set and the primary input set. The recursive extraction is decomposed to generate a second target set, and the second target set is verified.