What is formal equivalence checking and when is it used?

Formal equivalence checking (FEC) mathematically proves two designs are functionally identical without simulation. Uses: RTL to gate-level (verify synthesis), Pre-CTS to post-CTS (verify clock tree), Pre-ECO to post-ECO (verify late changes), and Gate-level to gate-level (verify optimization). Tools map corresponding points (registers, I/O) and prove combinational logic between them is equivalent. Handles state mapping, phase mapping, and retiming. Advantages: exhaustive verification, faster than simulation for equivalence. FEC is essential for signoff quality assurance.