基于多项式符号代数的数字电路形式验证方法研究

《基于多项式符号代数的数字电路形式验证方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、哈尔滨工程大学博士学位论文基于多项式符号代数的数字电路形式验证方法研究姓名：杨志申请学位级别：博士专业：计算机应用技术指导教师：马光胜20090601基于多项式符号代数的数字电路形式验证方法研究摘要随着数字集成电路设计规模的增大和功能复杂性的提高，功能验证已经成为设计流程中的瓶颈。传统的模拟验证方法无法满足现时复杂集成电路设计带来的巨大的验证需求。形式验证技术，例如模型检验和等价验证，因此发展成为模拟验证方法的一种重要补充，正日益受到学术界的关注。现有的形式验证技术大多基于传统的位级方法，例如BDD或布尔SAT，它们主要针对低层次门级电路和以控制流为主的电路的验证，难以胜任以数据

2、流为主的高层次复杂电路设计的验证。作为一种新近提出的电路表示和计算方法，多项式符号代数能够克服BDD和布尔SAT方法的某些不足。本文深入研究了多项式符号代数方法在数字电路形式验证中的应用，取得了如下创新性成果：(1)提出了基于多项式符号代数的模型检验方法。首先，扩展了传统的Kripkc结构的概念，得到了所谓状态转换系统的新概念。用该状态转换系统代替传统的Kripke结构来抽象高层次设计中的控制逻辑，并统一用多项式方法描述高层次设计中的数据通路和控制逻辑，从而有效地避免了数据域和控制域之间频繁的约束传播和回溯操作。进而，给出了一个高层次设计模型检验的方法框架。在该方法框架之下，原有

3、的模型检验问题被转化为一个假设和结论均具有多项式形式的一阶逻辑定理证明问题，一个基于多项式符号计算的判定过程被用来有效地解决该定理证明问题。针对典型高层次设计的实验结果表明，与现有的基于非线性求解器的高层次模型检验方法相比，该方法在保证验证准确性的情况下，平均要快1到5倍。(2)提出了基于多项式符号代数的等价验证方法。该方法直接在高层次建模数据通路设计，给出了高层次数据通路的多项式集合表示的一般形式及构造方法。由于避免了将高层次数据通路设计展开为门级网表，对于同样的验证问题，该方法涉及的信号变量的数目和约束表达式的数目要比基于BDD和布尔SAT的等价验证方法少得多。进而，从多项式

4、集合公共零点的角度定义了高层次数据通路的功能等价性，并给出了一个基于多项式符号计算的有效的代数求解算法。针对高层次基准数据通路的实验结果表明，与现有的基于*BMD和整数线性规划的高层次等价验证方法相比，该方法在保证错误诊断能力的情况哈尔滨丁程大学博士学位论文下，平均要快1倍到1个数量级。(3)提出了基于多项式符号代数的层次化验证方法。首先，引入了一种基于广义表数据结构的层次化电路表示模型。基于此种层次化表示，并应用多项式代数中的消元定理和扩张定理，得到了一种层次化的电路功能计算方法。该方法将原本规模较大的计算问题划分为一些小的计算问题，并以一种逐层递归的方式完成原有计算，从而有效

5、地提高了计算效率。进而，将这种新的电路功能计算方法用于设计验证，实现了层次化的模型检验和等价验证算法。实验结果表明，采用层次化策略能够有效地提高原有模型检验和等价验证算法的验证效率。就本文的实验电路而言，模型检验算法的效率平均提高了23％，等价验证算法的效率平均提高了17％。关键词：形式验证；模型检验；等价验证；层次化；多项式符号代数基于多项式符号代数的数字电路形式验证方法研究AbstractAsthesizeandfunctionalcomplexityofintegratedcircuitsincrease，functionalverificationhasbeenthema

6、inbottleneckofthedesignflow．Traditionalsimulationbasedverificationmethodscannotmeetwiththetremendousverificationdemandoftoday'scomplexintegratedcircuitdesigns．Becauseofthis，formalverificationtechniques，suchasmodelcheckingandequivalenceverification，receivemoreandmoreattentionfromacademiccircle

7、asanimportantassistant．Existingformalverificationtechniquesalemostlybasedonbit·levelmethods，suchasBDDandBooleanSAT,whicharegenerallygearedtowardsverificationoflow—·levelcontrol··dominatedcircuits，andarehardtosatisfytheverificationrequirements