基于吴方法的高层次模型检验方法研究

论文摘要

随着数字IC设计规模的增大和功能复杂性的提高,设计验证成为IC设计流程中越来越重要的方面。传统的模拟验证方法无法满足复杂IC设计带来的巨大的验证需求。基于此,形式验证方法作为模拟验证的一种重要补充,日益受到学术界的关注。模型检验作为一种重要的形式验证技术,由于自动化程度高,验证能力强,在工业界得到了广泛应用。现有的模型检验技术大多基于传统的位级方法,例如BDD或SAT,它们主要针对低层次门级电路和以控制流为主的电路的验证。然而,目前芯片的设计特点是要求强大的信号处理、数据通信能力、图像、多媒体处理和运算能力,算术运算模块和数据通路在电路中占有很大比例,使用BDD以及SAT难以对这样的电路进行建模。这也使得现有的模型检验技术无法胜任以数据流为主的高层次设计的验证。本文提出一种新颖的模型检验方法来解决高层次设计验证问题。本文从表示模型和验证算法两个方面进行研究。在表示模型方面,提出使用多项式等式来描述电路部件的功能和高层次时态逻辑公式。在验证算法方面,将吴方法机器定理证明的思想应用于高层次模型检验的方法框架。首先将电路按照时间帧展开,得到高层次设计的多项式集合表示;进而定义了高层次时态逻辑的定界语义,通过将描述性质的时态逻辑公式在给定的时间界限内展开,得到另一组多项式集合。以描述设计的多项式集合为假设,描述性质的多项式集合为结论,高层次模型检验问题被转化为一个假设和结论均具有多项式形式的定理证明问题。最后应用吴方法求解该定理证明问题。为了验证本文所提方法的正确性和有效性,随后进行了实验。从实验结果来看,本文所提的方法达到了预期的效果。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 课题背景及目的意义
• 1.2 论文的主要研究内容
• 1.3 论文的组织结构
• 第2章 形式验证方法
• 2.1 形式验证基于的数学方法
• 2.1.1 正则图形表示方法
• 2.1.1.1 BDD
• 2.1.1.2 WLDD
• 2.1.1.3 TED
• 2.1.2 代数方法
• 2.1.2.1 SAT
• 2.1.2.2 LP
• 2.1.2.3 PSA
• 2.2 形式验证的基本方法
• 2.2.1 等价验证
• 2.2.2 模型检验
• 2.2.3 定理证明
• 2.3 本章小结
• 第3章 模型检验理论与技术
• 3.1 模型检验理论基础
• 3.1.1 Kripke结构
• 3.1.2 时态逻辑
• 3.1.2.1 LTL
• 3.1.2.2 CTL
• 3.2 模型检验技术
• 3.2.1 CTL符号模型检验
• 3.2.1.1 不动点理论
• 3.2.1.2 符号模型检验
• 3.2.2 LTL定界模型检验
• 3.2.2.1 时态逻辑的定界语义
• 3.2.2.2 定界模型检验到SAT问题的转化
• 3.3 本章小结
• 第4章 吴方法介绍
• 4.1 吴方法的数学概念与原理
• 4.2 基于吴方法的几何定理机器证明
• 4.3 本章小结
• 第5章 基于吴方法的高层次模型检验方法
• 5.1 高层次模型检验的挑战
• 5.2 应用吴方法进行高层次模型检验
• 5.2.1 高层次设计的多项式建模
• 5.2.2 性质描述
• 5.2.3 基于吴方法的高层次模型检验
• 5.2.3.1 电路展开
• 5.2.3.2 从待验证性质的前件产生多项式等式集合
• 5.2.3.3 从待验证性质的后件产生多项式等式集合
• 5.2.3.4 应用吴方法求解定理证明问题
• 5.2.3.5 验证示例
• 5.2.4 变元定序
• 5.2.5 实验结果
• 5.3 本章小结
• 结论
• 参考文献
• 攻读硕士学位期间发表的论文和取得的科研成果
• 致谢