A BDD-based verification method for large synthesized circuits

Nowadays, logic synthesis tools are widely used to optimize and implement digital systems. Verifying the correctness of the generated circuits is an important practical problem. We present a new formal verification method for large synthesized circuits. It combines the use of binary decision diagrams (BDDs) with techniques to exploit the structural similarities of the circuits under comparison. These similarities are detected automatically. We show that the proposed method significantly extends the capability of BDD-based methods to verify large synthesized circuits.