| With increasing functional complexity of chips, it has become impractical to reason about their correctness manually. Traditional techniques for verification of a design against its specification such as simulation or emulation based methods are prohibitively time consuming and can leave corner cases untested. In high performance designs, most circuits are either fully custom designed or the synthesized output is modified manually to meet the design specifications. Hence, formal equivalence checking has become a desirable component of such design flows.; Even though there has been much research in equivalence checking over the last few years, little technology has been transferred to industry. The primary reason for the lag is that a tool in the research environment does not fit well with the practical design flows in industry. In this dissertation, we concentrate on the problem of applying equivalence checking in a real design flow of a microprocessor. The techniques presented in this thesis have been implemented in an industrial microprocessor environment.; We address the issue of transforming multi-phase designs, a popular industry practice to equivalent one-phase designs to enable the application of the current equivalence checking techniques. We propose an algorithm to compute the steady states of a machine by relaxing the assumption of a designated set of initial states (DIS). This assumption is used in research but is often restrictive in an industrial design environment. We use the paradigm of sequential hardware equivalence (SHE), which does not make the DIS assumption, for checking the equivalence of two machines. We show that two machines are SHE if the outputs of their product machine are 0 in the steady states. We propose machine partitioning and minimum area retiming to alleviate the problem of large state spaces common in industrial designs. Our techniques result in exponential reductions in the state space and enable equivalence checking of machines which cannot be handled otherwise. Lastly, we address the issue of interface verification arising out of a modular design environment. We show that the constraints required to express the input don't care space for equivalence checking of a module need to be verified formally for the completeness of equivalence checking. We characterize these constraints as combinationally provable and sequentially provable. Subsequently, we develop an assertion checking framework with efficient techniques to handle both types of constraints. |
