满足性算法在形式化验证中的应用研究及实现

论文摘要

随着超大规模集成电路复杂度的增加和规模的逐渐变大，验证电路的功能等价已经变得越来越重要。传统上，功能验证主要是通过模拟和测试技术实现。这些方法随着设计复杂度的增加，将很难保证能找到所有的死角错误。然而，形式化验证能够在数学上证明具体实现和规范之间的一致性，而不会错过或忽略任何搜索空间。已受到人们的广泛钟爱。由于验证问题的特殊性很多问题都可以转化为布尔满足性问题来解决，这使得布尔满足性问题在形式化验证领域占据着重要的地位。传统的基于BDD技术解决这一问题方法极大的受限于BDD的瓶颈问题——空间爆炸问题，难以解决规模比较大的问题。而基于DPLL（Davis-Putnam,Logemann and Loveland）深度搜索规则的SAT算法能够很好地避免这一问题，并且通过添加一些合理的启发式规则和学习机制能够快速的解决一些大规模问题。这就使得设计高效的SAT算法成了相当有价值的研究方向，而且业界在这个方面也不断地推成出新颖的SAT验证程序（例如当前比较有影响力的SAT程序包主要包括GRASP[6]，SATO[7]，BERKMIN[8]，ZCHAFF[9]等）进行不断地效率比试。本文主要从模型检验、符号模拟以及等价性验证三方面论述了布尔满足性算法在形式化验证领域的主要应用及相应算法的实现。首先，介绍了基于DPLL规则SAT算法的基本框架及关键技术，以及当前比较流行的基于SAT的有限模型验证和符号模拟技术。需要突出的是本文详细地讲述了基于DPLL深度搜索规则的启发式学习判定程序ChiveriSolver的实现过程以及提出了一些新颖的变量选择策略以及子句学习策略。在介绍基于SAT的等价性验证基础上，介绍了如何通过使用ChiveriSolver并利用增量式策略解决大规模组合电路的验证算法IncrCEC（Incremental Combinational Equivalence Checking）。在此算法中，通过对组合电路进行门级逻辑锥的划分，解决了使用纯SAT算法解决等价性问题时丢失电路共享结构信息的问题。最后，通过实验将ChiveriSolver与zchaff效率进行了对比，发现ChiveriSolver和zchaff在解决不同的问题上各有优势，ChiveriSolver完全可以和zchaff比美，并在对于变量单枝出现比较多的合取范式实例验证效率取得了很大的改进。并将ChiveriSolver应用于IncrCEC进行了组合等价性增量式验证，从实验结果可以看出基于增量式策略解决大规模的组合电路验证时，效率可观。

论文目录

• 摘要
• ABSTRACT
• 目录
• 第一章 绪论
• 1.1 引言
• 1.2 论文结构
• 第二章 SAT问题
• 2.1 启发式SAT算法
• 2.2 冲突分析过程
• 2.3 公式转换为CNF
• 2.4 本章小结
• 第三章 有限模型检验
• 3.1 背景知识
• 3.2 符号化表示
• 3.3 拆解传递关系
• 3.4 本章小节
• 第四章 符号模拟
• 4.1 时序拆解
• 4.2 布尔向量的参数化
• 4.3 基于SAT的再参数化算法
• 4.3.1 背景知识
• 4.3.4 计算参数方程h（P）
• 4.3.5 再参数化算法描述
• 4.3.6 SAT算法的应用
• 4.4 本章小结
• 第五章 等价性验证
• 5.1 组合电路等价性检验
• 5.1.1 背景知识
• 5.1.2 组合电路验证实例
• 5.1.3 组合电路增量验证
• 5.2 时序电路等价性检验
• 5.3 本章小结
• 第六章 启发式CHIVEIUSOLVER的实现
• 6.1 总体结构
• 6.1.1 读取范式阶段
• 6.1.2 预处理阶段
• 6.1.3 求解过程
• 6.1.4 结果处理阶段
• 6.2 详细设计
• 6.2.1 算法涉及的数据结构
• 6.2.2 算法使用的辅助结构
• 6.2.3 算法涉及的主要方法
• 6.3 程序说明
• 6.3.1 程序功能
• 6.3.2 程序输入
• 6.3.3 程序输出
• 6.4 本章小结
• 第七章 实验结果及分析
• 7.1 ChiveriSolver性能测试
• 7.2 增量式组合电路等价性验证
• 7.3 本章小节
• 第八章 结论及展望
• 参考文献
• 致谢