ABSTRACT

This chapter analyses the problem of formally checking whether two design specifications are functionally equivalent. In general, there is a wide range of possible definitions of functional equivalence covering comparisons between different levels of abstraction and varying granularity of timing details. The chapter focuses on the aforementioned machine equivalence, which in practical design flows is the most established application of functionally comparing two design specifications. It examines the role of equivalence checking in the design cycle and reviews the major approaches and techniques applied to this problem. The key to the practical success of formal equivalence checking is the separation of function and timing concerns in contemporary design flows. The need for formal equivalence checking methods was triggered by the necessity to use multiple models in hardware design flows. In the initial methodology which predated automatic logic synthesis, the actual logic implementation was designed independently and verified against the register transfer level by formal equivalence checking.