Relaxed equivalence checking: a new challenge in logic synthesis

The functional equivalence has always been the integral part of virtually every logic synthesis tool. The formal equivalence checking represents a key process that helps logic synthesis tool guarantee that two representations of a circuit design exhibit exactly the same behavior. Among others, equivalence checking is routinely applied to prove that a synthesized digital circuit is logically equivalent to the RTL source code. Although formal...