学位论文 > 优秀研究生学位论文题录展示
基于有限环上多项式的数字电路形式验证方法
作 者: 李东海
导 师: 马光胜
学 校: 哈尔滨工程大学
专 业: 计算机应用技术
关键词: 形式验证 等价性检验 定界模型检验 有限环上多项式 Gr(o ¨)bner基 定点数据通路
分类号: TN79
类 型: 博士论文
年 份: 2008年
下 载: 72次
引 用: 0次
阅 读: 论文下载
内容摘要
随着集成电路的规模变得越来越大、功能越来越复杂,功能验证已经成为设计流程的主要瓶颈。据统计,设计验证的时间已占到整个设计周期的一半以上。传统的基于模拟的验证方法不但需要花费大量的时间,而且不能保证完全的验证覆盖率,己经不能满足现时集成电路设计的要求。形式验证利用数学的方法隐式遍历所有可能的情况,能保证完全的验证覆盖率,所需要的验证时间也大幅减少,是克服验证瓶颈的可行途径。本文以有限环上多项式为基础模型,围绕算术密集型设计(例如数字信号处理(DSP)电路)的等价性检验和定界模型检验,进行了深入研究,取得了如下创新性成果:(1)针对实现多项式运算的定点数据通路的逻辑门级与寄存器传输级(RTL)之间的等价性检验,提出一种将定点数据通路的位级描述抽象为字级描述的方法。首先采用算术转换描述定点数据通路的逻辑门级功能,采用多项式函数描述定点数据通路的RTL功能,然后采用牛顿插值方法迭代地将算术转换抽象为多项式函数,以实现定点数据通路的逻辑门级模型与RTL模型之间的等价性检验。实验结果表明,该方法的速度与已有方法相比对乘法器的验证平均要快1至2倍,对一些实现多项式运算的定点数据通路的验证平均要快1个数量级。(2)针对定点数据通路的设计规范与RTL实现或优化后的RTL实现之间的等价性检验,构建vanishing多项式环的理想的极小强Gr(o|¨)bner基,并在此基础上提出一种高效的等价性检验算法。通过使用多项式函数建模定点数据通路的设计规范和RTL实现,将等价性检验问题转化为判断一个多项式函数是否为vanishing多项式的问题,进而采用vanishing多项式环的理想的极小强Gr(o|¨)bner基来有效地解决该问题。理论分析表明该算法的时间复杂度的上界比已有方法的时间复杂度的上界小。实验结果表明,对一些实现多项式运算的定点数据通路的等价性检验,该方法比已有方法平均要快2倍。(3)针对DSP电路的高层次设计验证的定界模型检验,提出一种基于有限环上多项式理想的Gr(o|¨)bner基的定界模型检验方法。通过使用有限环上多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并采用有限环上多项式理想的Gr(o|¨)bner基有效地解决该定理证明问题。实验结果表明,与基于布尔可满足性(SAT)和基于线性规划的RTL SAT的定界模型检验方法相比,该方法对一些DSP电路的验证平均要快1倍到1个数量级。
|
全文目录
摘要 5-7 Abstract 7-11 第1章 绪论 11-19 1.1 课题的背景及意义 11-15 1.2 研究现状 15-17 1.3 本文的工作 17-18 1.4 论文的组织结构 18-19 第2章 集成电路的形式验证综述 19-47 2.1 形式验证的数学基础 19-36 2.1.1 基于正则的判决图的形式验证 19-30 2.1.2 基于 SAT的形式验证 30-36 2.2 形式验证方法 36-46 2.2.1 等价性检验 36-39 2.2.2 模型检验 39-46 2.2.3 定理证明 46 2.3 本章小结 46-47 第3章 算术转换到多项式函数的抽象 47-65 3.1 引言 47-48 3.2 算术转换和多项式函数 48-52 3.2.1 算术转换 48-50 3.2.2 多项式函数 50-52 3.3 AT到多项式的抽象 52-61 3.3.1 对于一元多项式的抽象 52-58 3.3.2 对于多元多项式的抽象 58-61 3.4 实验结果 61-64 3.5 本章小结 64-65 第4章 基于vanishing多项式的等价性检验方法 65-78 4.1 引言 65-66 4.2 vanishing多项式环的理想 66-68 4.3 定点数据通路的等价性检验 68-75 4.4 实验结果 75-77 4.5 本章小结 77-78 第5章 基于有限环上多项式的定界模型检验方法 78-98 5.1 引言 78-80 5.2 有限环上多项式理想的Gr(o|¨)bner基 80-84 5.3 电路设计的多项式表示 84-87 5.3.1 算术运算部件 84-85 5.3.2 布尔逻辑 85 5.3.3 多路选择器 85 5.3.4 寄存器 85-86 5.3.5 其他运算 86-87 5.4 性质描述 87 5.5 基于有限环上多项式理想的Gr(o|¨)bner基的定界模型检验 87-94 5.5.1 电路展开 88-89 5.5.2 从待验证性质的前件产生有限环上多项式等式集合 89 5.5.3 从待验证性质的后件产生有限环上多项式等式集合 89-90 5.5.4 采用有限环上多项式理想的Gr(o|¨)bner基解决定理证明问题 90-92 5.5.5 求解反例 92-94 5.6 实验结果 94-96 5.7 本章小结 96-98 结论 98-100 参考文献 100-113 攻读博士学位期间发表的论文和取得的科研成果 113-115 致谢 115
|
相似论文
- 抑制糖皮质激素受体(GR)表达建立肾阳虚小鼠模型,R-332
- 7050A1/Gr复合材料时效强化行为及内耗研究,TB33
- Gr-1~+CD11b~+髓样前体细胞在小鼠哮喘相关炎症中作用的初步研究,R562.25
- 基于EOS芯片MAC模块的EDA验证,TN402
- GR公司绩效管理体系设计研究,F272
- 红外线加热式热疲劳试验台的研究与开发,TH871.3
- 应用于集成电路形式化验证的SAT算法研究,TN402
- 基于BDD的逻辑电路验证,TN791
- 一些算子在组合数学中的应用,O177
- 金属氧化物催化臭氧氧化酸性红B和酸性大红GR,X703
- 基于ARM9车载GPS与GPRS定位系统的地图匹配算法研究,P228.4
- Lin-Bose问题及Gr(?)bner基性质的研究,O151.21
- 多维多项式矩阵实现问题的研究,O174.14
- 高原兔肝脏火器伤后机体应激性变化的研究,R826.5
- Gr(?)bner基方法与吴方法之比较及其应用,O153
- 海南岛葫芦科蔬菜根结线虫种类鉴定及防治研究,S436.3
- 基于Color Petri Nets的HMIPv6协议形式化验证研究,TN929.5
- 量子群和超量子群的Gr(?)bner-Shirshov基,O152.5
- G_2型量子群的Gr(?)bner-Shirshov基,O152.5
- 3带正交小波的若干性质及其参数化,O174.2
- Gr+Al_2O_3/Al复合材料的组织与摩擦磨损性能,TB331
中图分类: > 工业技术 > 无线电电子学、电信技术 > 基本电子电路 > 数字电路
© 2012 www.xueweilunwen.com
|