论文题目: 逻辑电路的等价性检验方法研究
论文类型: 博士论文
论文专业: 计算机系统结构
作者: 李光辉
导师: 李晓维
关键词: 集成电路,形式验证,等价性检验,错误诊断,布尔推理
文献来源: 中国科学院研究生院（计算技术研究所）
发表年度: 2005
论文摘要: 随着集成电路设计的规模变得越来越大、功能越来越复杂,功能验证已经成为设计流程的主要瓶颈。据统计,设计验证的时间已占到整个设计周期的一半以上。基于模拟的功能验证方法非常费时,难以达到100%的功能覆盖率。形式验证方法使用严格的数学推理来证明设计满足规范的部分或全部属性,引起学术界和产业界的广泛关注。等价性检验是一种形式验证方法,用来验证一个设计的不同描述形式之间的功能等价性。本文的工作涵盖逻辑电路等价性检验的几个关键问题:如何提高增量等价性检验算法的效率;如何验证包含黑盒的电路设计;如何有效地结合布尔推理中的不同引擎以提高布尔推理算法的效率;如何提高设计错误诊断的效率。通过系统深入的理论分析和扎实的实验研究,取得了如下创新性成果:1.提出了一种基于增量可满足性的等价性检验方法。利用两个电路内部的结构相似性,将整个电路的验证分解成一些较小的任务,增量地完成。与同类方法相比,具有三个新的特点:(1)有选择地消除一些容易影响性能的候选等价信号对,减小可满足性程序的调用频度。(2)采用等价结点置换方法消除误判,并且增加相应的表示等价关系的合取范式公式,有效缩小可满足性程序的搜索空间。(3)使用增量可满足性算法,大幅度节省计算资源。通过对ISCAS’85电路的验证实验研究表明,对各基准电路,该方法产生的候选等价结点数比同类方法要少1个数量级,算法速度比同类方法平均要快3倍至1个数量级。2.提出了一种针对包含黑盒电路的设计验证方法。将模拟与形式化的布尔比较相结合,使用并行逻辑模拟来检测黑盒外部可能的设计错误,通过基于布尔可满足性(SAT)的布尔比较增强模拟算法。与基于二叉判决图(BDD)的方法相比,该方法具有更强的处理能力,有效降低了算法的空间复杂度。该方法已成功地应用于提高设计错误诊断的效率。通过ISCAS’85电路的实验研究表明,在具有与同类方法相当的错误检测能力的情况下,该方法对于各实验电路平均要快1至2个数量级,而且错误诊断的准确性更高。3.提出了有效结合多引擎的启发式策略。通过计算相关电路的宽度,在进行布尔推理之前,确定合适的布尔推理引擎,如基于BDD的引擎,或者基于SAT的引擎等,从而避免传统推理过程中的不同引擎切换过程,提高了算法的效率。通过对ISCAS’85电路的测试产生实验结果表明,基于电路宽度策略算法的速度比基于BDD大小估计策略的算法要快,而且所产生的BDD最大结点数要少得多。
论文目录:
摘要
Abstract
第一章 引言
1.1 研究背景及意义
1.2 研究现状
1.2.1 等价性检验方法的研究概况
1.2.2 验证包含黑盒的电路设计的方法
1.2.3 设计错误诊断方法
1.3 本文的工作
1.4 论文的组织结构
第二章 集成电路设计验证综述
2.1 基于模拟的设计验证方法
2.1.1 模拟验证方法
2.1.2 模拟验证的覆盖率评估
2.1.3 模拟验证方法的局限性
2.2 半形式化方法
2.2.1 覆盖率驱动的验证方法
2.2.2 符号模拟
2.3 形式化方法
2.3.1 等价性检验
2.3.1.1 组合电路等价性检验方法
2.3.1.2 误判问题的消除
2.3.1.3 时序电路的等价性检验方法
2.3.1.4 寄存器的一致性
2.3.2 模型检验
2.3.2.1 系统属性的表示
2.3.2.2 符号模型检验
2.3.2.3 有界模型检验
2.3.3 定理证明
2.4 集成电路的设计错误诊断
2.4.1 设计错误诊断方法
2.4.1.1 基于模拟的错误诊断方法
2.4.1.2 错误诊断的符号方法
2.4.2 提高错误诊断准确性的方法
2.4.3 含黑盒的设计验证与错误诊断方法
2.5 SOC的设计验证方法学
2.5.1 系统级验证
2.5.2 硬件RTL验证与软件验证
2.5.3 网表的验证与物理验证
2.5.4 层次化设计验证方法
2.6 加入可测性逻辑后的设计验证
2.6.1 形式验证中的ATPG引擎
2.6.2 加入可测性逻辑的设计验证方法
2.7 本章小结
第三章 布尔函数与基于电路的布尔推理
3.1 布尔函数
3.1.1 布尔函数的运算
3.1.2 硬件行为的模拟
3.2 二叉判决图
3.2.1 有序二叉判决图
3.2.2 有序二叉判决图的运算
3.2.3 有序二叉判决图的变量排序
3.2.4 BDD在形式化验证中的应用
3.2.4.1 组合电路的验证
3.2.4.2 有限状态机的可达性分析
3.3 布尔可满足性
3.3.1 布尔可满足性问题
3.3.2 布尔可满足性问题的算法
3.3.3 SAT在基于电路的布尔推理中的应用
3.3.3.1 基于SAT的测试产生方法
3.3.3.2 SAT在等价性检验中的应用
3.3.3.3 基于SAT的有界模型检验方法
3.4 静态逻辑蕴涵
3.4.1 静态逻辑蕴涵的基本概念
3.4.2 静态逻辑蕴涵的算法
3.4.3 静态逻辑蕴涵的应用
3.4.3.1 用静态逻辑蕴涵增强基于SAT的等价性检验方法
3.4.3.2 基于静态学习的验证方法
3.5 本章小结
第四章 基于电路宽度的布尔推理方法
4.1 问题的提出
4.2 电路宽度与电路复杂性
4.2.1 电路宽度
4.2.2 电路宽度与BDD大小的关系
4.2.3 电路可满足性问题的复杂性
4.3 基于电路宽度的启发式策略
4.3.1 基于BDD大小估计的启发式策略
4.3.2 基于电路宽度的启发式策略
4.4 基于电路宽度的启发式策略在ATPG中的应用
4.5 实验结果及其分析
4.6 本章小结
第五章 基于可满足性的增量等价性检验方法
5.1 引言
5.2 SAT在等价性检验中的应用
5.2.1 使用局部BCP消除误判
5.2.2 内部等价性的利用
5.3 基于可满足性的增量等价性检验方法
5.3.1 候选等价结点的确定
5.3.2 内部等价结点以及电路等价性的推导
5.4 实验结果及其分析
5.4.1 实验数据
5.4.2 实验结果分析
5.5 本章小结
第六章 验证包含黑盒的电路设计的形式化方法
6.1 集成电路设计中的黑盒问题
6.2 验证包含黑盒的电路设计的常用方法
6.2.1 基于BDD的方法
6.2.1.1 特征函数
6.2.1.2 验证包含黑盒的实现
6.2.2 基于SAT的方法
6.3 结合逻辑模拟与布尔可满足性的验证方法
6.3.1 基于量化的布尔可满足性验证方法
6.3.2 逻辑模拟与布尔可满足性算法的结合
6.4 算法的改进
6.5 实验结果及其分析
6.5.1 含有未知约束的布尔比较
6.5.2 含有黑盒的设计验证实验
6.5.3 未知约束的变化对布尔比较性能的影响
6.6 本章小结
第七章 设计错误诊断的形式化方法
7.1 引言
7.2 错误诊断方法的相关研究
7.2.1 基于故障模拟的诊断方法
7.2.3 基于SAT的诊断方法
7.2.3.1 基本记号
7.2.3.2 诊断算法
7.2.3.3 基于区域模型的错误诊断算法
7.3 结合逻辑模拟与布尔可满足性的错误诊断方法
7.3.1 算法的基本思想
7.3.2 错误诊断方法
7.4 实验结果及其分析
7.4.1 提高错误诊断算法效率的实验
7.4.2 错误区域大小对算法性能的影响
7.5 本章小结
第八章 结束语
8.1 本文的主要贡献
8.1.1 基于电路宽度的布尔推理方法
8.1.2 基于可满足性的增量等价性检验方法
8.1.3 验证包含黑盒的电路设计的方法
8.1.4 设计错误诊断方法
8.2 存在的问题与将来的工作
参考文献
发表文章目录
致谢
作者简历
发布时间: 2006-12-27
参考文献
- [1].三值量子可逆逻辑电路合成及三值量子算法研究[D]. 樊富有.电子科技大学2015
相关论文
- [1].基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[D]. 郑飞君.浙江大学2008
- [2].超大规模集成电路形式验证的方法研究[D]. 卢永江.浙江大学2005
- [3].可满足性问题算法研究以及在时序电路等价验证中的应用[D]. 丁敏.复旦大学2005
- [4].集成电路寄存器传输级故障模型与测试生成研究[D]. 杨修涛.中国科学院研究生院（计算技术研究所）2006
- [5].数字电路的故障测试模式生成方法研究[D]. 刘歆.华中科技大学2004
- [6].集成电路功耗估计及低功耗设计[D]. 徐勇军.中国科学院研究生院（计算技术研究所）2006
- [7].模拟验证中的激励产生与覆盖评估[D]. 鲁巍.中国科学院研究生院（计算技术研究所）2006
- [8].模型检验及其布尔可满足问题的研究[D]. 邵明.中国科学院研究生院（计算技术研究所）2005
- [9].数字电路测试压缩方法研究[D]. 韩银和.中国科学院研究生院（计算技术研究所）2005
- [10].集成电路的逻辑等价性验证研究[D]. 杨军.浙江大学2007