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

An Efficient Method for Verifying Designs with Black Boxes

在超大规模集成电路设计中 ,为了进行早期的设计错误检测与调试或层次化验证 ,常常需要使用含黑盒的设计验证方法 .该文提出了一种结合逻辑模拟和布尔可满足性的黑盒验证方法 ,用于验证设计中黑盒外部的功能正确性 .该方法使用量化的合取范式 (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.