结合逻辑模拟和布尔可满足性的设计错误诊断方法

Error Diagnosis of Logic Simulation and Boolean Satisfiability

在集成电路设计验证与调试过程中,逻辑错误诊断工具通常会给出一定数量的候选错误区域,然后通过特定的算法尽可能多地减少候选区域,以方便错误的准确定位。在此提出一种结合模拟与布尔可满足性(SAT)的错误诊断方法,用于提高错误诊断准确性。该方法首先使用模拟方法对候选的错误区域逐一进行判断,对于不能由模拟方法判别的候选区域,使用基于SAT的形式化方法进一步判断。针对ISCAS′85电路的实验结果表明,该方法具有较高的错误诊断准确性和效率。

In the integrated circuit design verification and debugging process, the diagnosis tools often present some candidate errorneous logic zones,and then reduce these zones as many as possible with special algorithms so that the designers can locate the error conveniently. A novel method integrating logic simulation and Boolean satisfiablity （SAT） for improving the accuracy of design error diagnosis. This method uses logic simulation to decide each candidate zone at first, and then a SAT solver is called to deal with those zones which can＇t be decided by logic simulation. Experimental results on ISCAS＇85 benchmark circuits show the efficiency and precision of the presented method.