The same function, twice
A subject the papers are about. The loosest grouping, and the one to reach for last.
Two descriptions of one device, and the question whether they agree. This set collects equivalence checking -- proving that an implementation computes the same function as a specification, or that two implementations compute the same function as each other. Membership requires the claim to be an equality between descriptions. A proof that a design satisfies a property belongs in the model-checking or program-logic sets; this set is for the cases where the property *is* another description.
**Why it is a separate question from the sets it borders.** state-space-not-proof collects exhaustive search over a state space: there is a system, a temporal property, and a traversal. Here there is no traversal and often no state -- a miter is built and asked whether it can be satisfied. Two records were moved out of that set and into this one for exactly that reason, and the reasoning is recorded on burch1992symbolic.
**What makes the problem hard is stated early and never goes away.** bryant1986graphbased is where equivalence becomes cheap: reduced ordered binary decision diagrams are a canonical form, so "testing for equivalence simply involves testing whether the two graphs match exactly". That one sentence is the foundation of the industry. Its appendix is also where the trouble starts, proving that integer multiplier outputs grow exponentially for **every** variable ordering.
1986 bryant1986graphbased canonical form makes equivalence a graph comparison -- except for multipliers 1987 bryant1987boolean a symbolic analysis of switch-level networks shown equivalent to MOSSIM II's behaviour 1994 burch1994automatic a pipelined implementation against an architectural description, by flushing 1996 kapur1996mechanically a family of multipliers against one specification, by induction, since BDDs cannot 2013 davis2013verified the AIG algorithms industrial equivalence checkers rely on, verified in ACL2 2018 huang2018instructionlevel an accelerator's manufactured instruction set against its hardware state machine 2025 yang2025forword sweeping for equivalence at word level rather than bit level 2026 zhu2026equivfusion one framework from algorithms down to netlists 2026 shen2026proving equivalence proved to a party who is not allowed to see the design
**Three things the set shows that no member states.**
First, **the hard case has been the same for forty years**. Bryant proves multipliers exponential in 1986; Kapur and Subramaniam route around the representation in 1996; FORWORD abandons the bit level in 2025; and manjrekar2025automating, held elsewhere, is still automating multiplier adder-tree proofs. Arithmetic is where this technique stops.
Second, **what counts as the two descriptions keeps moving upward**. In 1987 it is a transistor network against a simulator's behaviour; in 1994 a pipeline against an instruction set; in 2018 an accelerator against an instruction set that had to be *invented* for it, because accelerators had none. The technique is stable and the objects it compares are not.
Third, **the newest member changes who the proof is for**. Every other member assumes the checker may see both descriptions. shen2026proving proves equivalence under zero knowledge because the intellectual-property vendor will not show the netlist, revealing only the proof size and the gate count.