A method for performing rewind functional verification includes identifying state variables that model the number of registers on each edge of a retiming graph for an original design and a retimed design. Random variables are identified that model retiming labels representing a number and direction of register movement relative to a node on a retiming graph for the retimed design. A retiming constraint is identified for each edge on the retiming graph for the design, wherein the retiming constraint reflects a relationship between the state variables and the random variables. A random variable that models a retiming label at a source of an edge is recursively substituted for a random variable that models a retiming label at a sink of the edge when a number of registers on the edge is unchanged after register retiming.