# Equivalence checking Equivalence checking proves that two implementations compute the *same* output for **every** input, rather than testing them on a sample. One side is the trusted **reference** (the existing function, the source program, the register-transfer-level (RTL) code); the other is the candidate (the rewrite, the compiled output, the gate-level netlist). A solver either proves they agree everywhere or returns a concrete input on which they differ. The reference is the **oracle** (the same oracle as [differential testing](https://quality.stereobooster.com/differential-testing.md)), but discharged by proof instead of by examples, so the guarantee covers the whole input space. The technique has two names by community. Compiler people call it **translation validation**: proving each optimization pass preserves the meaning of the program it transformed. Hardware people call it **logic-equivalence checking**: proving a synthesized netlist matches its RTL, a routine sign-off step in chip design. ## What it catches - **Miscompilation and bad optimizations.** A transformation that changes a program's meaning. - **Reference-vs-rewrite divergence.** Any optimized, ported, or hand-hardened reimplementation that disagrees with the reference on some input. - **Synthesis errors.** RTL and the gate-level netlist computing different functions. What it does not catch: anything the reference itself gets wrong. Like all [differential testing](https://quality.stereobooster.com/differential-testing.md), it proves *relative* correctness: agreement with the reference, not agreement with intent. Decidability and scale bound it in practice: loops, unbounded state, and large designs force a depth bound or defeat it, and both sides must be expressible in the tool's logic. ## Tools - **Compiler / LLVM:** [alive2](https://github.com/AliveToolkit/alive2) checks that each LLVM optimization refines the program it transformed, modeling undefined behavior so it does not raise false alarms (Lopes et al. 2021)[^lopes2021]. - **Hardware (electronic design automation, EDA):** logic-equivalence checking of a netlist against its RTL is routine; the tools are proprietary EDA suites (Cadence Conformal, Synopsys Formality). - **General software:** bounded model checkers such as [CBMC](https://www.cprover.org/cbmc/) prove equivalence up to an unwinding depth. [CompCert](https://compcert.org/) removes the need to check at all, being a C compiler proved correct *by construction*. ## Where it sits Equivalence checking shares its solver engine with [symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) and [theorem proving](https://quality.stereobooster.com/theorem-proving.md); the difference is the fixed question (*are these two artifacts equal?*) rather than an arbitrary property. ## When to use, when not **Use** it where a rewrite must provably match a reference and both are small or structured enough to model: compiler passes, crypto kernels, hardware, hot inner loops replaced by a hand-tuned version. **Don't** reach for it when the programs are too large or loop-heavy to discharge (fall back to [differential testing](https://quality.stereobooster.com/differential-testing.md) on generated inputs), or when no trusted reference exists to check against. ## Evidence - **Translation validation finds real miscompilations.** Running alive2 over LLVM's own test suite surfaced dozens of real bugs and clarified ambiguities in the LLVM intermediate-representation (IR) specification (Lopes et al. 2021)[^lopes2021]: defects that had survived LLVM's conventional testing, caught because the check is exhaustive up to its unrolling bound rather than a sample. - **Beyond these, the case is industrial, not measured.** Hardware logic-equivalence checking is a standard sign-off step in chip design, but that is established practice rather than a controlled comparison of defect-detection rates. ## Related **Differential oracle** These all answer the same question — *does the candidate match a trusted reference?* — and differ in how rigorously you compare, and in what the reference is. By rigour: - Equivalence checking — *prove* they agree on every input. - [Differential testing](https://quality.stereobooster.com/differential-testing.md) — *test* them on sampled inputs before release. - [Parallel run](https://quality.stereobooster.com/parallel-run.md) — *observe* them side by side on live production traffic. The reference itself varies too: a trusted implementation (a peer, the previous version, a gold-standard library), or a deliberately simple [executable spec](https://quality.stereobooster.com/executable-specifications.md) authored to *be* the reference. ## Classification - **Quality dimensions:** Functionality, Security (constant-time or hardened reimplementations proved equivalent to a reference — security is incidental to the functional equivalence). - **Area:** Compiler-optimization validation, hardware RTL↔netlist, verified reimplementations and ports, crypto kernels. - **Guarantee:** Mathematical, Exhaustive (bounded). ## Referenced by - [Guarantee](https://quality.stereobooster.com/guarantee.md) · The axes - [The axes](https://quality.stereobooster.com/axes.md) · The axes - [Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) · Methods - [Differential testing](https://quality.stereobooster.com/differential-testing.md) · Methods ## References [^lopes2021]: Lopes, Nuno P., Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. "[Alive2: Bounded Translation Validation for LLVM](https://web.ist.utl.pt/nuno.lopes/pubs/alive2-pldi21.pdf)." *Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '21)*, 65–79. . ## Acronyms - EDA — electronic design automation - IR — intermediate representation - RTL — register-transfer level