【作者】 杨志；

【导师】 马光胜；

【作者基本信息】 哈尔滨工程大学 ， 计算机应用技术， 2009， 博士

【摘要】 随着数字集成电路设计规模的增大和功能复杂性的提高,功能验证已经成为设计流程中的瓶颈。传统的模拟验证方法无法满足现时复杂集成电路设计带来的巨大的验证需求。形式验证技术,例如模型检验和等价验证,因此发展成为模拟验证方法的一种重要补充,正日益受到学术界的关注。现有的形式验证技术大多基于传统的位级方法,例如BDD或布尔SAT,它们主要针对低层次门级电路和以控制流为主的电路的验证,难以胜任以数据流为主的高层次复杂电路设计的验证。作为一种新近提出的电路表示和计算方法,多项式符号代数能够克服BDD和布尔SAT方法的某些不足。本文深入研究了多项式符号代数方法在数字电路形式验证中的应用,取得了如下创新性成果：(1)提出了基于多项式符号代数的模型检验方法。首先,扩展了传统的Kripke结构的概念,得到了所谓状态转换系统的新概念。用该状态转换系统代替传统的Kripke结构来抽象高层次设计中的控制逻辑,并统一用多项式方法描述高层次设计中的数据通路和控制逻辑,从而有效地避免了数据域和控制域之间频繁的约束传播和回溯操作。进而,给出了一个高层次设计模型检验的方法框架。在该方法框架之下,原有的模型检验问题被转化为一个假设和结论均具有多项式形式的一阶逻辑定理证明问题,一个基于多项式符号计算的判定过程被用来有效地解决该定理证明问题。针对典型高层次设计的实验结果表明,与现有的基于非线性求解器的高层次模型检验方法相比,该方法在保证验证准确性的情况下,平均要快1到5倍。(2)提出了基于多项式符号代数的等价验证方法。该方法直接在高层次建模数据通路设计,给出了高层次数据通路的多项式集合表示的一般形式及构造方法。由于避免了将高层次数据通路设计展开为门级网表,对于同样的验证问题,该方法涉及的信号变量的数目和约束表达式的数目要比基于BDD和布尔SAT的等价验证方法少得多。进而,从多项式集合公共零点的角度定义了高层次数据通路的功能等价性,并给出了一个基于多项式符号计算的有效的代数求解算法。针对高层次基准数据通路的实验结果表明,与现有的基于*BMD和整数线性规划的高层次等价验证方法相比,该方法在保证错误诊断能力的情况下,平均要快1倍到1个数量级。(3)提出了基于多项式符号代数的层次化验证方法。首先,引入了一种基于广义表数据结构的层次化电路表示模型。基于此种层次化表示,并应用多项式代数中的消元定理和扩张定理,得到了一种层次化的电路功能计算方法。该方法将原本规模较大的计算问题划分为一些小的计算问题,并以一种逐层递归的方式完成原有计算,从而有效地提高了计算效率。进而,将这种新的电路功能计算方法用于设计验证,实现了层次化的模型检验和等价验证算法。实验结果表明,采用层次化策略能够有效地提高原有模型检验和等价验证算法的验证效率。就本文的实验电路而言,模型检验算法的效率平均提高了23%,等价验证算法的效率平均提高了17%。更多还原

【Abstract】 As the size and functional complexity of integrated circuits increase, functional verification has been the main bottleneck of the design flow. Traditional simulation based verification methods cannot meet with the tremendous verification demand of today’s complex integrated circuit designs. Because of this, formal verification techniques, such as model checking and equivalence verification, receive more and more attention from academic circle as an important assistant. Existing formal verification techniques are mostly based on bit-level methods, such as BDD and Boolean SAT, which are generally geared towards verification of low-level control-dominated circuits, and are hard to satisfy the verification requirements of high-level data-dominated designs. As a newly devolopted technique for circuit representation and computation, polynomial symbolic algebra can overcome some drawbacks of BDD and Boolean SAT. This thesis investigates the application of polynomial symbolic algebra in digital cricuit verification deeply. The contributions of this thesis are as follows.(1) A model checking approach based on polynomial symbolic algebra has been proposed. First, a new concept called state transition system is obtained by extending the concept of classical Kripke structure, which is used to represent the control logic of high-level designs as a substitution of the latter. Datapath and control logic of high-level designs can thus be modeled in a unified framework using polynomial method, and frequent constraint propagation and backtracking between data domain and control domain are therefore avoided. Then, a framework for high-level model checking is presented. In the framework, the original model checking problem is translated into a first-order theorem proving problem, in which both hypothesis and conclusion of the theorem are of polynomial form. A symbolic computation based decision procedure is ultilized to prove the theorem efficiently. The experimental results on some typical high-level designs show that, the proposed approach is on average one to five times faster than the nonlinear solver based high-level model checking approache, while keeping the verification accuracy. (2) An equivalence verification method based on polynomial symbolic algebra has been proposed. Datapaths are modeled at higher levels of abstraction directly. The general form of the polynomial set representations of high-level datapaths and the method to construct it are presented. Since high-level datapaths no longer need to be transformed into gate-level netlists, our approach usually involves much less signal variables and constraints for a given verification problem compared with the BDD and Boolean SAT based equivalence verification methods. Furthermore, the functional equivalence of high-level datapaths is defined from the prospective of common zeros of polynomial sets, and an efficient algebraic solution based on symbolic computation is presented. The experimental results on some benchmark datapaths show that, the proposed method is on everage one factor to one order of magnitude faster than the *BMD and integer linear programming based equivalence verification methods, while keeping the error detecting capability.(3) The hierarchical verification methods based on polynomial symbolic algebra have been proposed. First, a generalized list based hierarichical representation for circuit designs is introduced. Based on this hierarchical representation and ultilizing the elimination and extension theorems from polynomial algebra, a new method is proposed to calculate the functionality of circuit designs, which breaks the original calculation into small sub-tasks to finish recursively. The computational efficiency can thus be improved efficienctly. Applying this new calculation method to design verification, hierarchical model checking and equivalence verification methods are realized. The experimental results show that, the hierarchical verification methods are much more efficient than the original verification methods. For our experimental circuits, efficiencies of the model checking and equivalence verification algorithms increase 23% and 17% respectively.更多还原