Verification Techniques for System-Level Design

Chapter 6. Equivalence Checking on Higher-Level Design Descriptions

Introduction

In this chapter, we introduce equivalence-checking methods for design descriptions that are higher level than register transfer level (RTL). Because of the nature of high-level design descriptions based on C/C++ languages, word-level variables, such as integer and other multibit variables, are often used. If we always expand such variables into multiples of Boolean variables, the number of variables for Boolean reasoning, like the ones based on SAT solvers and BDD-based routines, easily become too large to be processed. Instead, any reasoning procedures on high-level design descriptions should apply word-level analysis methods, which deal as much as possible with all ...