Skip to content

Software Quality

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), 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, 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 checks that each LLVM optimization refines the program it transformed, modeling undefined behavior so it does not raise false alarms (Lopes et al. 2021)1.
  • 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 prove equivalence up to an unwinding depth. CompCert 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 and theorem proving; 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 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)1: 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.

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 — test them on sampled inputs before release.
  • Parallel run — 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 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

References

  1. Lopes, Nuno P., Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. "Alive2: Bounded Translation Validation for LLVM." Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '21), 65–79. https://doi.org/10.1145/3453483.3454030. ↩↩