RTL Error Diagnosis Using a Word-Level SAT-Solver

We propose a novel methodology for design error diagnosis in the HDL description using a word-level solver. In this approach, the patterns that result in erroneous responses are first used to limit the number of initial error candidates. The RTL description of the design is then modified by adding one multiplexer to each of the possible error locations. For each of the erroneous pattern, the input pattern and the expected correct response are then imposed as constraints to the modified RTL model, resulting in a formula suitable for word-level satisfiability (SAT) solving. The solutions reported by the word-level SAT solver would indicate the potential error candidates. This constraint solving process iterates for each erroneous pattern, eventually resulting in a small set of error candidates. This method is sufficiently flexible to address both single-error and multiple-error diagnosis. We present experimental results for a set of public RTL benchmark designs to demonstrate the effectiveness of this proposed approach.