Retiming Verification Using Sequential Equivalence Checking

High performance designs must conform to stringent timing requirements. Designers frequently utilize low-level optimization techniques and develop many iterations of the same block in order to close a timing gap. Simulation with random stimulus is the traditional method for verifying that these changes do not introduce a change in the functional behavior of the block. For the development of a new high-performance core at Freescale Semiconductor the authors decided to instead research the possibility of using formal techniques, in the form of sequential equivalence checking, for this form of verification. Various equivalence checking tools were evaluated for this task. Initial results looked promising and the authors decided to integrate this capability into our design flow. This paper describes the experience and also addresses some of the problems that were exposed and how we plan to deal with them