论文题目: 超大规模集成电路形式验证的方法研究
论文类型: 博士论文
论文专业: 电路与系统
作者: 卢永江
导师: 严晓浪
关键词: 模拟验证,形式验证,等价性验证,二叉决策图,可满足性,割集,锁存器匹配,先假设后验证,符号回溯验证
文献来源: 浙江大学
发表年度: 2005
论文摘要: 随着集成电路的设计规模越来越大、复杂度越来越高,产品上市时间却越来越紧迫,集成电路的验证变得越来越困难。2003年度的国际半导体技术发展报告(International Technology Roadmap for Semi-conductor, ITRS2003)指出,验证已经成为集成电路设计流程中最大瓶颈。传统的模拟验证因其测试周期长、不能完全覆盖,已经不适合当前对集成电路的验证。形式验证作为传统基于模拟的验证方法的补充,日益引起人们的关注。它的特点是使用严格的数学推理来证明一个系统满足全部或部分规范。 本论文在较为全面、深入地研究和总结国内外形式验证技术研究成果的基础上,对组合电路及时序电路验证上分别进行算法研究、设计和实现,取得了较为理想的结果。主要内容包括: 组合电路验证是数字集成电路形式化设计验证的重用方面。论文给出了一种使用布尔可满足性SAT的新颖组合电路等价性验证技术。算法是在联接电路(Miter)中进行推理来简化验证问题,推理中使用了与/非图结构简化、二叉决策图BDD扩展、隐含学习多种方法,最后使用有效SAT解算器zChaff解决验证任务。该算法综合了BDD和SAT的优点,限制BDD构建大小避免了内存爆炸,推理简化减小了SAT搜索空间。 针对利用BDD验证常常出现内存爆炸这一问题,我们注意到在实际的设计流程中,对设计的电路修改优化只是涉及部分电路结构的变化,因此参考电路与实现电路之间存在大量的等价节(即结构相似性)。由于这一特点,本文提出一个高效的割集算法。该算法结合静态割集验证多对节点时的高效性,利用动态在割集验证一对节点时有效性,扬长补短,提高算法的鲁棒性。 时序电路验证比组合电路更复杂,尤其是状态变量多的电路。一种有效的方法是通过锁存器匹配,将部分时序电路验证转化为组合电路验证问题,降低验证的复杂度。本文提出了一种结合多种方法的新颖锁存器匹配算法。算法结合任意
论文目录:
第一章 绪论
§1.1 引言
§1.2 验证的基本概念
§1.3 验证方法综述
1.3.1 模拟验证方法
1.3.1.1 软件模拟
1.3.1.2 硬件仿真
1.3.1.3 测试
1.3.2 形式验证方法
1.3.2.1 模型检验
1.3.2.2 定理证明
1.3.2.3 等价性检查
§1.4 论文的研究重点以及章节安排
第二章 二叉决策图及其在电路验证中的应用
§2.1 引言
§2.2 二叉决策图
§2.3 有序二叉决策图
2.3.1 最简的的序二叉决策图
2.3.2 ROBDD运算小结
2.3.3 建立电路中节点逻辑函数的ROBDD表示
2.3.4 ROBDD的变量问题
§2.4 基于HARMONY多输出变量排序
2.4.1 单输出变量排序
2.4.2 Harmony启发式算法
2.4.3 其它变量合并
2.4.4 实验结果
第三章 可满足性方法与形式验证
§3.1 引言
§3.2 可满足性问题的有关定义和性质
§3.3 SAT求解程序
3.3.1 DPLL算法
3.3.2 分支策略
3.3.3 冲突分析
§3.3 可满足性的电路验证原理
§3.4 静态隐含加速等价性验证
3.4.1 静态隐含术语介绍
3.4.2 关联节点静态隐含
3.4.2.1 识别关联节点
3.4.2.2 关联节点静态隐含算法
3.4.3 提高隐含速度的策略
3.4.4 算法
3.4.5 实验结果
第四章 组合电路等价性验证方法研究
§4.1 引言
§4.2 组合电路中一些基本定义
§4.3 结合二叉判决图和布尔可满足性的等价性验证算法
4.3.1 基本定义和定理
4.3.2 验证算法
4.3.2.1 AIG结构简化
4.3.2.2 二叉判决图扩展
4.3.2.3 基于电路的解算器和基于CNF的解算器
4.3.3 实验结果
§4.4 一种有效的基于割集的等价性验证算法
4.4.1 基本定义和定理
4.4.2 算法描述
4.4.3 割集生成算法
4.4.3.1 动态割集生成
4.4.3.2 静态割集
4.4.4 依赖性处理
4.4.5 误判处理
4.4.6 实验结果及其分析
第五章 时序电路等价性验证方法研究
§5.1 引言
§5.2 一种有效的用于时序电路等价性验证的锁存器匹配算法
5.2.1 预备知识
5.2.2 算法描述
5.2.2.1 任意模拟技术
5.2.2.2 局部BDD
5.2.2.3 目标模拟
5.2.3 实验结果
§5.3 基于局部BDD的时序电路等价性验证
5.3.1 预备知识
5.3.2 相关研究
5.3.3 基于局部BDD的时序验证算法
5.3.3.1 算法流程
5.3.3.2 算法原理
5.3.3.3 其它加速策略
5.3.3.4 时序方法描述
5.3.4 实验结果
第六章 结论与展望
§6.1 论文的主要工作
§6.2 进一步的研究工作和设想
参考文献
攻读博士期间撰写的学术论文
致谢
发布时间: 2005-07-14
参考文献
- [1].基于有限环上多项式的数字电路形式验证方法[D]. 李东海.哈尔滨工程大学2008
- [2].基于多项式符号代数的数字电路形式验证方法研究[D]. 杨志.哈尔滨工程大学2009
- [3].VLSI设计中的形式验证方法研究[D]. 吴俊华.哈尔滨工程大学2009
- [4].基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[D]. 郑飞君.浙江大学2008
- [5].RTL到门级设计的等价性验证的研究[D]. 翁延玲.浙江大学2008
- [6].基于SAT的数字电路形式验证方法研究[D]. 王秀芹.哈尔滨工程大学2009
- [7].片上系统高层等价性检验关键技术研究[D]. 胡健.国防科学技术大学2016
- [8].基于PSA的集成电路形式验证方法研究[D]. 范德会.哈尔滨工程大学2012
相关论文
- [1].RTL到门级设计的等价性验证的研究[D]. 翁延玲.浙江大学2008
- [2].基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[D]. 郑飞君.浙江大学2008
- [3].VLSI设计中的形式验证方法研究[D]. 吴俊华.哈尔滨工程大学2009
- [4].基于SAT的数字电路形式验证方法研究[D]. 王秀芹.哈尔滨工程大学2009
- [5].超大规模集成电路若干布线算法研究[D]. 庄昌文.电子科技大学2001
- [6].深亚微米工艺条件下标准单元和存储器逻辑参数提取及建模技术研究[D]. 李训根.浙江大学2005
- [7].32位嵌入式CPU的超深亚微米物理实现与验证[D]. 张培勇.浙江大学2005
- [8].可满足性问题算法研究以及在时序电路等价验证中的应用[D]. 丁敏.复旦大学2005
- [9].逻辑电路的等价性检验方法研究[D]. 李光辉.中国科学院研究生院（计算技术研究所）2005
- [10].集成电路的逻辑等价性验证研究[D]. 杨军.浙江大学2007
标签：模拟验证论文; 形式验证论文; 等价性验证论文; 二叉决策图论文; 可满足性论文; 割集论文; 锁存器匹配论文; 先假设后验证论文; 符号回溯验证论文;