Efficient equivalence checking of multi-phase designs using retiming
Gagan Hasteer, Anmol Mathur, Prithviraj Banerjee · 1998
The use of multi-phase clocking scheme, aggressive pipelining and #sparse" encodings in high performance designs results in a tremendous increase in the state space. In this paper, we show that automatically transforming such designs to ones that have more #dense" encodings can result in signi#cant bene#ts in using implicit BDD-based techniques for their veri#cation. 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 #4# #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. 1 Introduction Due to aggressive t...