Incremental SAT-Based Accurate Auto-Correction of Sequential Circuits Through Automatic Test Pattern Generation

As the complexity of digital designs continuously increases, existing methods to ensure their correctness are facing more serious challenges. Although many studies have been provided to enhance the efficiency of debugging methods, they are still suffering from the lack of scalable automatic correction mechanisms. In this paper, we propose a method for correcting multiple design bugs in gate level circuits. To reduce the correction time, an incremental satisfiability-based mechanism is proposed which not only does not require a complete set of test patterns to produce a gate level implementation which does not exhibit erroneous behavior, but also will not reintroduce old bugs after fixing new bugs. The results show that our method can quickly and accurately suggest corrected gates even for large industrial circuits with many bugs. Average improvements in terms of the runtime and memory usage in comparison with existing methods are 2.8x and 6.5x, respectively. Also, the results show that our method compared to the state-of-the-art methods needs 2.6x less test patterns.