验证包含黑盒的电路设计的有效方法  

An Efficient Method for Verifying Designs with Black Boxes

作　　者：李光辉[1,2,3] 邵明[1,3] 李晓维[1,3] 

机构地区：[1]中国科学院计算技术研究所 [2]浙江林学院信息工程学院杭州311300 [3]中国科学院研究生院北京100039

出　　处：《计算机学报》2004年第6期796-802,共7页Chinese Journal of Computers

基　　金：国家自然科学基金重点项目 ( 90 2 0 70 0 2 );北京市重点科技项目基金(H0 2 0 12 0 12 0 13 0 );浙江省自然科学基金 (M 60 3 0 97)资助

摘　　要：在超大规模集成电路设计中 ,为了进行早期的设计错误检测与调试或层次化验证 ,常常需要使用含黑盒的设计验证方法 .该文提出了一种结合逻辑模拟和布尔可满足性的黑盒验证方法 ,用于验证设计中黑盒外部的功能正确性 .该方法使用量化的合取范式 (CNF)来表示电路中出现的未知约束 ,并且不需要修改电路结构 ,有效地节省了计算资源 .此外 ,通过使用随机并行模拟增强了可满足性算法的错误检测能力 .通过对ISCAS’85电路的实验表明了该方法不仅比以往同类算法速度快 ,而且具有较好的错误检测能力 .In the VLSI design cycle, in order to detect and debug the errors in early stages or to verify the functional correctness hierarchically, black boxing verification methods are often used. In this paper, an efficient method integrating logic simulation and Boolean satisfiability (SAT) is presented, which can verify the designs with black boxes. This method uses quantified conjunctive normal form (CNF) formulas to represent the unknown constraints in the circuit under verification, and needs no modification of the circuit structure so that it saves the computational resources significantly. In addition, this approach enhances the SAT-based algorithm with random parallel pattern simulation, which improves the capability of detecting errors. Experimental results on the ISCAS’85 benchmark circuits demonstrate that, the proposed approach is faster up to one to three orders of magnitude than those approaches in literature.

关 键 词：超大规模集成电路设计 错误检测 层次化验证 黑盒验证方法 合取范式 

分 类 号：TN47[电子电信—微电子学与固体电子学]