论文题目: 可满足性问题算法研究以及在时序电路等价验证中的应用
论文类型: 博士论文
论文专业: 微电子与固体电子学
作者: 丁敏
导师: 唐璞山
关键词: 可满足性问题,时序电路等价验证,形式验证
文献来源: 复旦大学
发表年度: 2005
论文摘要: 当今的VLSI芯片设计给验证带来巨大挑战。形式验证作为传统模拟验证的补充越来越受到重视。提高形式验证的验证规模和速度成为国际研究的热点。本文的研究工作针对这个趋势,可以分成两个部分: Ⅰ.可满足性算法的研究。本文的研究工作首先就从验证问题的基本理论问题—可满足性问题入手。选择目前可满足性问题中的主流算法—DPLL算法作为研究的主要对象。分析了DPLL算法流程中基本且重要的启发式优化策略。并在此基础上,针对高级推理过程,提出了具有动态删除策略的改进了的失败性文字检查(FLD)过程。具体贡献有:1)从对动态删除策略的定性分析和实验结果分析表明,本文提出的动态删除策略在大大降低原有FLD过程的计算时间同时,减小了实际的DPLL算法的搜索空间,因而提高了DPLL算法的总体运行速度;2)由于DPLL算法在当前可满足性问题中的垄断地位,任何优化策略都必须适合集成到该算法中。同其他的高级推理过程技术相比,经过本文改进后的FLD技术更适合结合到DPLL算法中。 Ⅱ.时序电路等价验证的研究。本文在对可满足性问题的研究基础上,着重研究将可满足性问题的算法作为验证引擎应用到时序电路等价验证中。本文先分析了传统的基于状态遍历算法及其优缺点,比较了两种主流引擎—BDD和SAT的优缺点,然后利用了模型检查中的基于数学归纳法思想,提出了单独使用可满足性算法作为引擎的基于时间帧展开的时序电路等价验证算法。该算法的特点有:1)由于我们的算法只使用到了可满足性算法引擎,因而和采用BDD引擎的算法不同,不存在内存增长过快的问题。并且本文在算法的构造和改进中提高了引擎在迭代使用时候的效率;2)我们的算法在结合了数学归纳法、不可满足子集提取和结构不动点计算这三种已有的技术基础后,更适合用于时序深度较深的逻辑层时序电路的等价验证。而且,在整合三种技术后,又提出了一些改进措施。从实验分析表明,这些改进措施在有效降低可满足性算法引擎的计算时间同时,也进一步减缓了内存的增长,优于单独使用数学归纳法的时序等价验证。
论文目录:
摘要
ABSTRACT
第一章 绪论
§1．1 集成电路发展及设计验证
§1．2 NP完全问题
§1．3 本文研究背景及出发点
§1．4 本文研究重点
§1．5 论文的组织结构
第二章 基础知识
§2．1 布尔代数
§2．2 集合与布尔函数
§2．3 二分决策图(BDD)
§2．4 逻辑范式、电路与可满足性问题(SAT)
第三章 可满足性问题算法的发展
§3．1 历史综述
§3．2 DPLL算法
§3．3 加速搜索过程的启发式策略
§3．3．1 布尔约束传递过程(BCP，Boolean Constraint Propagation)
§3．3．2 基于冲突的学习过程和非同步回溯
§3．3．3 决策变量选择策略
§3．3．4 学习子句的删除
§3．3．5 随机重新启动
§3．4 数据结构
§3．5 小结
第四章 高级推理过程—FLD算法研究
§4．1 高级推理过程简述
§4．2 FLD算法
§4．3 动态筛选策略
§4．4 结合FLD的DPLL算法流程
§4．5 实验结果与分析
§4．6 小结
第五章 不可满足子集提取
§5．1 不可满足子集
§5．2 基于DPLL算法的不可满足子集提取算法简述
第六章 时序电路等价验证综述
§6．1 时序电路模型及等价验证层次
§6．2 时序电路等价定义
§6．3 基于状态遍历的等价验证算法
§6．4 BDD引擎vs SAT引擎
§6．5 小结
第七章 基于时间帧展开的时序电路等价验证算法
§7．1 引言
§7．2 数学归纳法思想
§7．3 基于时间帧展开的等价验证算法
§7．4 实验结果与分析
§7．5 小结
第八章 总结和展望
§8．1 论文工作总结
§8．2 今后工作展望
参考文献
附录
§附录一：FDSAT程序部分伪代码
§附录二：FESD程序部分伪代码
致谢
发布时间: 2005-09-19
参考文献
- [1].时序电路测试产生中一些关键技术的研究[D]. 王仲.中国科学院研究生院（计算技术研究所）1999
- [2].时序电路测试生成算法研究[D]. 许川佩.西安电子科技大学2006
- [3].基于蚂蚁算法的时序电路测试生成研究[D]. 李智.电子科技大学2003
- [4].纳米集成电路软错误分析与缓解技术研究[D]. 孙岩.国防科学技术大学2010
- [5].低功耗逻辑电路设计及在RISC设计中的研究[D]. 韦健.浙江大学2001
- [6].并行ATPG算法理论与原型系统设计技术研究[D]. 刘蓬侠.国防科学技术大学2002
- [7].电路进化设计算法研究[D]. 梁后军.中国科学技术大学2009
- [8].数字集成电路测试生成算法研究[D]. 侯艳丽.哈尔滨工程大学2008
相关论文
- [1].基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[D]. 郑飞君.浙江大学2008
- [2].基于SAT的数字电路形式验证方法研究[D]. 王秀芹.哈尔滨工程大学2009
- [3].超大规模集成电路形式验证的方法研究[D]. 卢永江.浙江大学2005
- [4].可编程逻辑核版图自动生成方法研究[D]. 温宇杰.复旦大学2005
- [5].模型检验的反例解释[D]. 沈胜宇.国防科学技术大学2005
- [6].数字电路的故障测试模式生成方法研究[D]. 刘歆.华中科技大学2004
- [7].逻辑电路的等价性检验方法研究[D]. 李光辉.中国科学院研究生院（计算技术研究所）2005
- [8].模型检验及其布尔可满足问题的研究[D]. 邵明.中国科学院研究生院（计算技术研究所）2005
- [9].基于布尔可满足性的电路设计错误诊断[D]. 吴洋.复旦大学2006
- [10].集成电路的逻辑等价性验证研究[D]. 杨军.浙江大学2007
标签：可满足性问题论文; 时序电路等价验证论文; 形式验证论文;