What does "equivalent" mean?
Formal equivalence verification (FEV) proves that two models of a design produce the same outputs for the same inputs. "Same" can mean different things:
| Kind | Compared | Requires | Typical use |
|---|---|---|---|
| Combinational | Logic between matching state elements | Same flops in both models (1-to-1 map) | RTL vs synthesised netlist, netlist vs netlist |
| Sequential | Output sequences from reset | Same reset state; state may differ | Retiming, pipelining, clock gating, FSM re-encoding |
| Transaction-level | Results of complete operations, possibly at different times | A notion of "transaction" and alignment | C/C++ model vs RTL, high-level synthesis |
Combinational equivalence is by far the most widely used: virtually every chip's netlist is checked against its RTL this way after synthesis and every later netlist transformation.