A Scalable Formal Debugging Approach with Auto-Correction Capability Based on Static Slicing and Dynamic Ranking for RTL Datapath Designs

作者：Alizadeh Bijan^*; Behnam Payman; Sadeghi Kohan Somayeh

来源：IEEE Transactions on Computers, 2015, 64(6): 1564-1578.

DOI：10.1109/TC.2014.2329687

• Formal verification
• equivalence checking
• debugging and correction
• decision diagram
• RTL datapath designs

By increasing the complexity of digital systems, verification and debugging of such systems have become a major problem and economic issue. Although many computer aided design (CAD) solutions have been suggested to enhance efficiency of existing debugging approaches, they are still suffering from lack of providing a small set of potential error locations and also automatic correction mechanisms. On the other hand, the ever-growing usage of digital signal processing (DSP), computer graphics and embedded systems applications that can be modeled as polynomial computations in their datapath designs, necessitate an effective method to deal with their verification, debugging and correction. In this paper, we introduce a formal debugging approach based on static slicing and dynamic ranking methods to derive a reduced ordered set of potential error locations. In addition, to speed up finding true errors in the presence of multiple design errors, error candidates are sorted in decreasing order of their probability of being an error. After that, a mutation-based technique is employed to automatically correct bugs even in the case of multiple bugs. In order to evaluate the effectiveness of our approach, we have applied it to several industrial designs. The experimental results show that the proposed technique enables us to locate and correct even multiple bugs with high confidence in a short run time even for complex designs of up to several thousand lines of RTL code.

• 出版日期2015-6