An efficient verification method for a class of multi-phase sequential circuits

Currently, many optimizations of sequential circuits, even as simple as retiming, are avoided due to the lack of verification tools that support them. Doing general sequential equivalence to compare the circuits is impractical for circuits of a reasonable size. On the other hand, combinational optimization is part of the design process, because tools and methods are available to ensure correctness and verify combinational circuits. We present a practical method to verify sequential circuits equivalence using combinational equivalence on a transformed circuit of the same size, for a class of circuits. The constraint imposed is that for each loop in the circuit, there must be a point in both circuits that are in correspondence. The circuits can have a different number of clock phases, and they can be transformed by other scheduling algorithms than retiming and multi-phase retiming.