However, if verification fails, most tools only allow the computation of counterexamples in form of input patterns for which the output of the optimized circuit (called the implementation) differs from the unoptimized circuit (called the specification). Design Error Diagnosis and Correction methods (DEDC) try to overcome this limit. Instead of computing counterexamples, automatic error localization and correction is performed. In particular, DEDC algorithms try to modify the implementation circuit with a minimal number of changes such that it becomes equivalent to the specification. DEDC methods reflect a real industrial demand since debugging time by far exceeds the design time of state-of-the-art digital circuits.
The objective of this thesis is to develop a method for automatic error localization and correction of combinational circuits at the gate level. The core rectification method is based on symbolic methods. Therefore, the method does not need to assume an error model and can detect and correct arbitrary design errors. Furthermore, the method is robust, meaning that the computed results are independent of any structural similarities between the specification and the implementation circuit. Two algorithms for locating design errors are presented: The node traversal algorithm is well suited for rectifying circuits with single error sources while the component refinement algorithm implements multiple error localization and correction. Scalability of the rectification method is achieved by two abstraction techniques: Component-extraction and node-abstraction. Furthermore, it is shown how the rectification of tri-state circuits and sequential circuits can be solved by reduction to combinational rectification problems.