Efficient equivalence checking of multi-phase designs using retiming

The use of multiphase clocking scheme, aggressive pipelining and "sparse" encodings in high performance designs results in a tremendous increase in the state space. We show that automatically transforming such designs to ones that have more "dense" encodings can result in significant benefits in using implicit BDD based techniques for their verification. We formulate a relaxed retiming framework which is more powerful than traditional retiming in reducing the number of latches and show that it can be applied to the product machine model for checking sequential hardware equivalence (SHE) without altering the correctness of the SHE check. We combine retiming with phase abstraction (C. Pixley, 1992) (a technique to transform multi phase FSMs to single phase FSMs for equivalence checking). The two transformations enable the SHE check to be performed on high performance controllers with large state space (more than 100 latches) from an industrial setting.