Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction

  • Dirk W. Hoffmann
  • Thomas Kropf
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


Boolean equivalence checking has turned out to be a powerful method for verifying combinatorial circuits and has been widely accepted both in academia and industry. In this paper, we present a method for localizing and correcting errors in combinatorial circuits for which equivalence checking has failed. Our approach is general and does not assume any error model. Thus, it allows the detection of arbitrary design errors. Since our method is not structure-based, the pro]duced results are independent of any structural similarities between the implementation circuit and its specification. It can even be applied if the specification is given, e.g., as a propositional formula, a BDD, or in form of a truth table.

Furthermore, we discuss two kinds of circuit abstractions and prove compatibility with our rectification method. In combination with abstractions, we show that our method can be used to rectify large circuits.

We have implemented our approach in the AC/3 equivalence checker and circuit rectifier and evaluated it with the Berkeley benchmark circuits [6] and the ISCAS85 benchmarks [7] to show its practical strength.


Automatic error correction design error diagnosis equivalence checking formal methods 


  1. 1.
    M. S. Abadir, J. Ferguson, and T. E. Kirkland. Logic design verification via test generation. IEEE Transactions on CAD, 7(1):138–148, January 1988.Google Scholar
  2. 2.
    D. Brand. The taming of synthesis. In International Workshop on Logic Synthesis, May 1991.Google Scholar
  3. 3.
    D. Brand. Incremental synthesis. In Proceedings of the International Conference on Computer Aided Design, pages 126–129, 1992.Google Scholar
  4. 4.
    D. Brand. Verification of Large Synthesized Designs. In IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 534–537, Santa Clara, California, November 1993. ACM/IEEE, IEEE Computer Society Press.Google Scholar
  5. 5.
    D. Brand, A. Drumm, S. Kundu, and P. Narain. Incremental synthesis. In Proceedings of the International Conference on Computer Aided Design, pages 14–18, 1994.Google Scholar
  6. 6.
    R. K. Brayton, G. D. Hachtel, C. T. McMullen, and A. L. Sangiovanni-Vincentelli. Logic Minimization Algorithms for VLSI Synthesis. The Kluwer International Series in Engineering and Computer Science. Kluwer Academic Publishers, 1986.Google Scholar
  7. 7.
    F. Brglez and H. Fujiwara. A neutral netlist of 10 combinatorial benchmark circuits and a target translator in FORTRAN. In Int. Symposium on Circuits and Systems, Special Session on ATPG and Fault Simulation, 1985.Google Scholar
  8. 8.
    R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.zbMATHCrossRefGoogle Scholar
  9. 9.
    R. E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.CrossRefGoogle Scholar
  10. 10.
    P. Y. Chung, Y. M. Wang, and I. N. Hajj. Diagnosis and correction of logic design errors in digital circuits. In Proceedings of the 30th Design Automation Conference (DAC), 1993.Google Scholar
  11. 11.
    A. Gupta. Formal Hardware Verification Methods: A Survey. Journal of Formal Methods in System Design, 1:151–238, 1992.CrossRefGoogle Scholar
  12. 12.
    D. W. Hoffmann and T. Kropf. AC/3 V1.00-A Tool for Automatic Error Correction of Combinatorial Circuits. Technical Report 5/99, University of Karlsruhe, 1999. available at
  13. 13.
    Alan J. Hu. Formal hardware verification with BDDs: An introduction. In IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM), pages 677–682, October 1997.Google Scholar
  14. 14.
    S. Y. Huang, K. C. Chen, and K. T. Cheng. Error correction based on verification techniques. In Proceedings of the 33rd Design Automation Conference (DAC), 1996.Google Scholar
  15. 15.
    J. C. Madre, O. Coudert, and J. P. Billon. Automating the diagnosis and the rectification of design errors with PRIAM. In Proceedings of ICCAD, pages 30–33, 1989.Google Scholar
  16. 16.
    S. M. Reddy, W. Kunz, and D. K. Pradhan. Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment. In ACM/IEEE Design Automation Conference, pages 414–419, 1995.Google Scholar
  17. 17.
    M. Tomita and H. H. Jiang. An algorithm for locating logic design errors. In IEEE International Conference of Computer Aided Design (ICCAD), 1990.Google Scholar
  18. 18.
    M. Tomita, T. Yamamoto, F. Sumikawa, and K. Hirano. Rectification of multiple logic design errors in multiple output circuits. In Proceedings of the 31st Design Automation Conference (DAC), 1994.Google Scholar
  19. 19.
    A. Veneris and I. N. Hajj. Correcting multiple design errors in digital VLSI circuits. In IEEE International Symposium on Circuits and Systems (ISCAS), Orlando, Florida, USA, May 1999.Google Scholar
  20. 20.
    A. Wahba and D. Borrione. A method for automatic design error location and correction in combinational logic circuits. Journal of Electronic Testing: Theory and Applications, 8(2):113–127, April 1996.CrossRefGoogle Scholar
  21. 21.
    A. Wahba and D. Borrione. Connection errors location and correction in combinational circuits. In European Design and Test Conference ED&TC-97, Paris, France, March 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Dirk W. Hoffmann
    • 1
  • Thomas Kropf
    • 1
  1. 1.Institut für Technische InformatikUniversität TübingenTübingenGermany

Personalised recommendations