any boolean reasoning problem can be expressed as a SAT problem. Commercial applications for equivalence checking Major products in the Logic Equivalence Checking (LEC) area of EDA are: FormalPro by Mentor Graphics Questa SLEC by Mentor Graphics Conformal by Cadence JasperGold by Cadence Formality by Synopsys VC Formal by Synopsys 360 EC by OneSpin Solutions ATEC by ATEC Generalizations Equivalence Checking of Retimed Circuits: Sometimes it is helpful to move logic from one side of a register to another, and this complicates the checking problem. Sequential Equivalence Checking: Sometimes, two machines are completely different at the combinational level, but should give the same outputs if given the same inputs. The classic example is two identical state machines with different encodings for the states. Since this cannot be reduced to a combinational problem, more general techniques are required. Equivalence of Software Programs, i.e. checking if two well-defined programs that take N inputs and produce M outputs are equivalent: Conceptually, you can turn software into a state machine (that's what the combination of a compiler does, since a computer plus its memory form a very large state machine.) Then, in theory, various forms of property checking can ensure they produce the same output. This problem is even harder than sequential equivalence checking, since the outputs of the two programs may appear at different times; but it is possible, and researchers are working on it. See also Formal methods References Electronic Design Automation For Integrated Circuits Handbook, by Lavagno, Martin, and Scheffer, A survey of the field. This article was derived, with permission, from Volume 2, Chapter 4, Equivalence Checking, by Fabio Somenzi and Andreas Kuehlmann. R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers., C-35, pp. 677–691, 1986. The original reference on BDDs. Sequential equivalence checking for RTL models. Nikhil Sharma, Gagan Hasteer and Venkat Krishnaswamy. EE Times. External links CADP – provides equivalence checking tools for asynchronous designs OneSpin 360 EC-FPGA – Functional correctness of FPGA synthesis from RTL code to final netlist Electronic circuit verification Formal methods