June 19, 2006 -- The ability to formally determine functional equivalence between RTL models is seen as a key enabler in physically aware front-end design methodologies that are being practiced in high performance designs. In this article, we describe sequential equivalence checking (SEC) technology and the usage of such a tool in various a practical design flows. We present scenarios that call for modifying the sequential behavior of RTL models while preserving functionality.

The advantages of verifying such sequential modifications using formal methods at the block level are identified. Some attention to front end design methodology can vastly improve the efficiency of sequential equivalence checking tools.

By Nikhil Sharma, Gagan Hasteer and Venkat Krishnaswamy. (Hasteer is Vice President of Engineering at Calypto Design Systems, Krishnaswamy is Vice President of Applications Engineering, and Sharma is Senior R&D Manager.)