Establishing latch correspondence for sequential circuits using distinguishing signatures

This paper addresses the problem of establishing the unknown correspondence for the latch variables of two sequential circuits which have the same state encoding. This has direct application in finite state machine verification: If a one-to-one correspondence can be established between the latches of two circuits, then checking for their equivalence reduces to a much simpler combinational equivalence check problem. The approach presented in this paper is based on methods used to solve the unknown correspondence problem for inputs and outputs in combinational circuits. It computes input and novel latch output signatures, using ROBDDs, for each latch variable of a circuit that help to establish correspondence. Experimental results on a large set of benchmarks show the efficacy of this approach.