Abstract
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.
This work is supported by the ESPRIT LTR Project 26241 (PROSPER)
Chapter PDF
Similar content being viewed by others
References
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.
D. Brand. The taming of synthesis. In International Workshop on Logic Synthesis, May 1991.
D. Brand. Incremental synthesis. In Proceedings of the International Conference on Computer Aided Design, pages 126–129, 1992.
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.
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.
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.
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.
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
R. E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
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.
A. Gupta. Formal Hardware Verification Methods: A Survey. Journal of Formal Methods in System Design, 1:151–238, 1992.
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.
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.
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.
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.
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.
M. Tomita and H. H. Jiang. An algorithm for locating logic design errors. In IEEE International Conference of Computer Aided Design (ICCAD), 1990.
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.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoffmann, D.W., Kropf, T. (1999). Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_13
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive