Formal Verification, 2nd Edition

Chapter 8: Formal equivalence verification

Abstract

In this chapter, we describe formal equivalence verification (FEV), a formal verification technique focused on checking whether two designs are logically equivalent. There are several ways we can define equivalence for FEV tools: combinational equivalence, which optimizes the problem by breaking up models at latch/flop boundaries; sequential equivalence, which checks that behavior of two models over a period of time results in equivalent outputs; and transactional equivalence, which checks that certain well-defined operations produce identical results on two models. We then discuss how these types of equivalence fit into some common real design flows: using register transfer level (RTL)-RTL ...