Formal Verification

Chapter 8

Formal equivalence verification

In this chapter we describe Formal Equivalence Verification (FEV), an FV 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 RTL-RTL equivalence to check design changes or optimizations, ...