Patent ID: 8181132

Claim:
A method comprising: simulating by one or more computer systems a larger circuit, as compared to one or more reduced circuits, to assign one or more values to one or more latch variables associated with the larger circuit; generating by the one or more computer systems the one or more reduced circuits from the larger circuit according to the one or more values assigned to the one or more latch variables; generating by the one or more computer systems a transition relation (TR) for each reduced circuit; and generating by the one or more computer systems an initial state set for one or more instances of validation on the one or more reduced circuits according to the TRs, wherein: simulating by the one or more computer systems the larger circuit comprises: simulating by the one or more computer systems the larger circuit from an initial state to generate one or more vectors that each comprise one or more reachable states of the larger circuit; selecting by the one or more computer systems one or more latch variables associated with the larger circuit; and assigning by the one or more computer systems the one or more values to the one or more latch variables according to some of the one or more reachable states in the one or more vectors; generating by the one or more computer systems the one or more reduced circuits comprises: synthesizing by the one or more computer systems the larger circuit according to the one or more values assigned to the one or more latch variables; and generating by the one or more computer systems the initial states for the one or more instances of validation on the one or more reduced circuits comprises: generating the initial states according to some of the one or more reachable states in the one or more vectors different from the some of the one or more reachable states in the one or more vectors used to assign the one or more values to the one or more latch variables.