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

Error Diagnosis of Logic Simulation and Boolean Satisfiability

作　　者：曾松伟[1] 李光辉[1] 

机构地区：[1]浙江林学院信息工程学院,浙江临安311300

出　　处：《现代电子技术》2010年第6期22-25,37,共5页Modern Electronics Technique

基　　金：浙江省自然科学基金资助项目(Y106707)

摘　　要：在集成电路设计验证与调试过程中,逻辑错误诊断工具通常会给出一定数量的候选错误区域,然后通过特定的算法尽可能多地减少候选区域,以方便错误的准确定位。在此提出一种结合模拟与布尔可满足性(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.

关 键 词：设计验证 错误诊断 布尔可满足性 逻辑模拟 

分 类 号：TN710[电子电信—电路与系统]