ABSTRACT

In the early 1980s, IBM’s mainframe design ow introduced automatic logic synthesis that largely replaced the manual design step. is did not diminish the importance of equivalence checking that became instrumental in verifying the absence of functional discrepancies that

4.6.2.1 SAT-Based Reachability Analysis 98

4.6.2.2 Decomposition as a Way to Reduce Complexity 100

4.6.2.3 Alignability 102

4.7 Summary 105

References 105

are introduced by tool or methodology bugs or through frequent manual intervention. In the early 1990s, IBM began to complement synthesis-based design ows with custom design circuit blocks. Here again, formal equivalence checking between the RTL specication and manually designed transistor-level implementation provided a critical component to ensure functional correctness [2]. A similar approach was followed in the design ow of later versions of the Alpha microprocessor [3] and Intel’s microprocessors [4]. In the mid-1990s, after logic synthesis became broadly adopted in typical ASIC design ows, equivalence checking technology moved into the domain of computer-aided design (CAD) tool vendors. Today, in many ASIC and custom design methodologies, formal equivalence checking is a key component of the overall chip validation procedure, similar to static timing analysis and design rule checking.