Logical equivalence checking (LEC)
Beginner
A math-based check that the finished parts list gives the same answers as the original design, for every possible input.
Novice
A mathematical proof, rather than a test, that two versions of a design (for example the RTL code and the synthesized netlist) produce the same outputs for every possible input.
Expert
LEC first pairs up state points (flip-flops, ports, black boxes) between the reference and the implementation, then proves the logic feeding each pair identical, using AIGs, random simulation, SAT solvers and BDDs. Retiming, state re-encoding and merged or deleted flip-flops break the pairing and need guidance from the synthesis tool or sequential checking.