Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction
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  and the ISCAS85 benchmarks  to show its practical strength.
KeywordsAutomatic error correction design error diagnosis equivalence checking formal methods
- 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.D. Brand. The taming of synthesis. In International Workshop on Logic Synthesis, May 1991.Google Scholar
- 3.D. Brand. Incremental synthesis. In Proceedings of the International Conference on Computer Aided Design, pages 126–129, 1992.Google Scholar
- 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.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.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.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
- 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
- 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 http://goethe.ira.uka.de/~hoff.
- 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.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.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.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.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.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.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
- 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