组合电路等价验证预处理算法研究

论文摘要

随着大型集成电路设计和SOC芯片设计的不断进步,电路的规模,硬件的复杂度不断增大。今天,70%的设计时间是花费在验证错综复杂的系统上,传统的验证方法已经不能完全满足现今的要求,而形式验证则变得越来越重要,现在2种使用最广泛的形式验证技术相等性检查和模块检查成为研究的突破方向。本文研究工作是针对可满足问题(SAT)在组合电路验证和测试中的应用展开的。本文提出了一种能提高基于SAT的组合相等性检测,研究出一个低损耗的预处理器,可以静态地引入全局信号关系到原先的需要验证的Miter电路CNF公式,来减低SAT语句的复杂性,有效快速的建立蕴涵图,产生大量的直接,非直接和扩展回溯蕴含,加入到Miter电路的CNF公式中,来减少分析的时间。本文主要的价值之处在于:(1)通过全局信号关系引入恰当的语句,快速建立蕴含图,并且转换蕴含表达式为二进制子句。(2)利用加入的子句来约束SAT解决器的搜索空间,提供各个变量之间的关系,来增强布尔约束传递,大幅减少SAT公式的复杂性。

论文目录

• 摘要
• Abstract
• 第一章 引言
• 1.1 集成电路设计与制造技术的发展
• 1.2 形式化验证的介绍
• 1.3 可满足性问题研究和合取范式（CNF）预处理的研究情况
• 1.4 论文的组织结构
• 1.5 本文对于Miter电路简化预处理的方法和实现
• 第二章 可满足问题（SAT）在形式验证中的应用
• 2.1 逻辑电路转换为CNF表示
• 2.2 利用SAT进行电路的等价验证
• 2.3 利用SAT进行电路故障检测
• 2.4 SAT在其他形式验证中的应用
• 2.5 小结
• 第三章 可满足问题解决器及其算法
• 3.1 可满足问题的算法
• 3.2 BDD算法
• 3.3 DPLL算法
• 3.4 Zchaff解决器
• 3.4.1 BCP过程的数据结构
• 3.4.2 冲突分析和学习过程
• 3.4.3 变量的选择策略
• 3.4.4 新加入子句的删除策略和定时重启策略
• 3.5 小结
• 第四章 静态蕴含及其处理方法
• 4.1 静态蕴含
• 4.1.1 直接蕴含
• 4.1.2 间接蕴含
• 4.1.3 扩展回溯蕴含
• 4.2 可满足性问题的静态蕴含的应用
• 4.2.1 增强布尔约束传递
• 4.2.2 鉴定相等或者相反文字
• 4.2.3 常数节点的鉴定
• 4.2.4 扩展回溯蕴含的意义
• 4.3 CNF公式中生成静态蕴含表达式
• 4.3.1 CNF公式中直接蕴含的处理
• 4.3.2 CNF公式中间接蕴含的处理
• 4.3.3 CNF公式中扩展回溯蕴含的处理
• 4.4 小结
• 第五章 预处理器的算法和实现
• 5.1 目标
• 5.2 预处理器算法步骤
• 5.3 预处理器的数据结构
• 5.4 预处理器的主要程序结构
• 5.5 Miter电路处理后的实验数据
• 5.6 小结
• 第六章 总结和后续发展.
• 6.1 本文工作总结
• 6.2 本文工作展望
• 参考文献
• 致谢