1. A machine-readable recordable type storage medium having a plurality of instructions processable by a machine embodied therein, wherein said plurality of instructions, when processed by said machine, causes said machine to perform a method comprising: receiving a design; determining a number of simulation cycles necessary to simulate said design for verification; building for said design an intermediate binary decision diagram set containing one or more nodes representing one or more variables; in response to building said intermediate binary decision diagram set, initializing a plurality of registers associated with said design with initial values; creating a binary decision diagram variable for each input to said design; performing verification of said design by evaluating a property of said intermediate binary decision diagram; building for said design a subsequent intermediate binary decision diagram set containing one or more nodes representing one or more variables; updating said plurality of registers with a set of next state function values; case splitting upon a first fattest variable from among said one or more variables represented by said one or more nodes by setting said first fattest variable to a first value; first cofactoring said intermediate binary decision diagram set with respect to said one or more nodes using an inverse of said first value to generate a first cofactored binary decision diagram set; second cofactoring said intermediate binary decision diagram set with respect to said one or more nodes using said first value to generate a second cofactored binary decision diagram set; in response to determining at least one simulation cycle remains, repeating said building for said design said subsequent intermediate binary decision diagram set; and in response to determining that at least one simulation cycle does not remain, outputting results of said verification.