High performance designs must conform to stringent timing requirements. Designers frequently utilize lowlevel 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 we 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 we decided to integrate this capability into our design flow. This paper will describe our experience and will also address some of the problems that were exposed and how we plan to deal with them.