The pervasiveness of digital systems in almost all commercial and industrial sectors has led to increased productivity and reduced time-to-market. Moreover, due to the complexity of modern Very Large Scale Integration (VLSI) designs, various verification techniques have been developed to cope with undetected functional failures. As a complement to traditional dynamic simulations, Formal Verification (FV) offers the possibility to mathematically check the functional correctness of the Device Under Verification (DUV) in a drastically shortened time, along with exhaustive coverage of the design state space. Formal Equivalence Verification (FEV) consists in comparing two models, known as specification and implementation, to check whether they are functionally equivalent or not.