Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

In this paper we develop a theory of equivalence checking (EC) and logic synthesis of circuits with a common specification (CS). We show that two combinational circuits N1 N2 have a CS iff they can be partitioned into subcircuits that are connected "in the same way" and are toggle equivalent. This fact allows one to represent a specification of a circuit implicitly as a partitioning into subcircuits. We give an efficient procedure for checking if circuits N1, N2 have the same predefined specification. As a "by-product", this procedure performs EC of N1 and N2. We show how, given a circuit N1 with a predefined specification, one can efficiently build a circuit N2 satisfying the same specification. We give experimental evidence that EC of N1 N2 is hard if their CS is unknown.

REFERENCES

• 1: Berman,C.L., and Trevillyan,L.H. Functional comparison of logic designs for VLSI circuits. ICCAD-89, pp.456--459.
• 2: Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
• 3: Jerry R. Burch , Vigyan Singhal, Tight integration of combinational verification methods, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.570-576, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289088]
• 4: Goldberg, E. Equivalence Checking of Dissimilar Circuits II. Technical report. CDNL-TR-2004-0830, August 2004, available at http://eigold.tripod.com/papers.html
• 5: Goldberg, E. Equivalence checking and logic synthesis of circuits with a common specification. Technical report. CDNL-TR-2004--1220, August 2004.
• 6: Goldberg, E., and Novikov, Y. Equivalence Checking of Dissimilar Circuits, IWLS-2003. May 28-30, USA. Available at http://eigold.tripod.com/papers/dissim-iwls.zip
• 7: C. A. J. van Eijk , Geert Janssen, Exploiting Structural Similarities in a BDD-Based Verification Method, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.110-125, September 26-28, 1994
• 8: Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266090]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Automatic synthesis

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Optimization; Verification

General Terms:
Algorithms, Design, Theory, Verification

Keywords:
common specification, scalable equivalence checking, scalable logic synthesis, toggle equivalence