Abstract
Functional verification occupies a significant amount of the digital circuit design cycle. In this paper, we present a novel approach to improve circuit debugging which not only localizes errors with high confidence, but can also provide semantically-meaningful source code corrections. Our method, which we call FudgeFactor, starts with a buggy design, at least one failing and several correct test vectors, and a list of suspect bug locations. We obtain the suspect location from a state-of-the-art debugging tool that includes a significant number of false positives. Using this list and a library of rules empirically characterizing typical source-code mistakes, we instrument the buggy design to allow each potential error location to either be left unchanged, or replaced with a set of possible corrections. FudgeFactor then combines the instrumented design with the test vectors and solves a 2QBF-SAT problem to find the minimum number of source-level changes from the original code which correct the bug. Our 13 benchmarks demonstrate that our method is able to correct a sizable portion of realistic bugs within a reasonable computational time. With the aid of available golden reference designs, we show that those corrections are, at least on these benchmarks, always valid and non-trivial fixes. We believe that our technique significantly improves over other debugging tools in two respects: When we succeed, we obtain a much more precise bug localization with no false positives and little or no ambiguity. Additionally, we offer bug corrections that are inherently meaningful to the designers and enable designers to quickly recognize and understand the root cause of the bug with a high level of confidence.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Alizadeh, B., Behnam, P., Sadeghi-Kohan, S.: A scalable formal debugging approach with auto-correction capability based on static slicing and dynamic ranking for RTL datapath designs. IEEE Trans. Comput. 64(6), 1564–1578 (2015)
Alur, R., Bodik, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Proceedings of the 13th Conference on Formal Methods in Computer-Aided Design, Portland, OR, pp. 1–8, October 2013
Bloem, R., Wotawa, F.: Verification and fault localization in VHDL programs. J. Telematics Eng. Soc. 2, 30–33 (2002)
Chang, K.H., Markov, I., Bertacco, V.: Fixing design errors with counterexamples and resynthesis. In: Proceedings of the Asia and South Pacific Design Automation Conference, Yokohama, Japan, pp. 944–949, January 2007
Chang, K.H., Wagner, I., Bertacco, V., Markov, I.: Automatic error diagnosis and correction for RTL designs. In: Proceedings of the High Level Design Validation and Test Workshop, Irvine, CA, pp. 65–72, November 2007
Chung, P.Y., Hajj, I.N.: ACCORD: Automatic catching and correction of logic design errors in combinational circuits. In: Proceedings of the International Test Conference, Baltimore, MD, pp. 742–751, September 1992
Chung, P.Y., Wang, Y.M., Hajj, I.N.: Logic design error diagnosis and correction. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 2(3), 320–332 (1994)
Debroy, V., Wong, W.E.: Using mutation to automatically suggest fixes for faulty programs. In: Proceedings of the Third International Conference on Software Testing, Verification and Validation, pp. 65–74, April 2010
Foster, H.: Trends in functional verification: a 2014 industry study. In: 2015 52nd ACM/EDAC/IEEE Design Automation Conference (DAC), pp. 1–6, June 2015
Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226–238. Springer, Heidelberg (2005)
Mahler, J.: A MIPS CPU written in Verilog. https://github.com/jmahler/mips-cpu. Accessed 24 April 2015
OpenCores: Opencores database. http://www.opencores.org
Peischl, B., Wotawa, F.: Automated source level error localization in hardware designs. J. IEEE Des. Test Comput. 23(1), 8–19 (2006)
Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, Seattle, WA, pp. 15–26, June 2013
Smith, A., Veneris, A., Ali, M.F., Viglas, A.: Fault diagnosis and logic debugging using Boolean satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. CAD 24(10), 1606–1621 (2005)
Lezama, A.S.: Program synthesis by sketching. Ph.D. thesis, UC Berkeley, December 2008. http://eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html
Staber, S., Jobstmann, B., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441–460 (2012)
Wolf, C., Glaser, J., Kepler, J.: Yosys - a free Verilog synthesis suite. In: Proceedings of 21st Austrian Workshop on Microelectronics, Linz, Austria, October 2013
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Becker, A. et al. (2015). FudgeFactor: Syntax-Guided Synthesis for Accurate RTL Error Localization and Correction. In: Piterman, N. (eds) Hardware and Software: Verification and Testing. HVC 2015. Lecture Notes in Computer Science(), vol 9434. Springer, Cham. https://doi.org/10.1007/978-3-319-26287-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-26287-1_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26286-4
Online ISBN: 978-3-319-26287-1
eBook Packages: Computer ScienceComputer Science (R0)