FudgeFactor: Syntax-Guided Synthesis for Accurate RTL Error Localization and Correction

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.