基于多项式模型的高层次形式化验证
| 第1章 绪论 | 第1-24页 |
| ·EDA的发展阶段 | 第11-12页 |
| ·课题研究的意义 | 第12-15页 |
| ·验证和确认 | 第15-18页 |
| ·验证方法 | 第18-19页 |
| ·模拟验证 | 第18页 |
| ·形式化验证 | 第18-19页 |
| ·形式化验证的现状 | 第19-22页 |
| ·本文主要工作 | 第22-24页 |
| 第2章 形式化验证概述 | 第24-34页 |
| ·模型验证 | 第24-25页 |
| ·定理证明器 | 第25-26页 |
| ·形式化综合 | 第26-27页 |
| ·等价性验证 | 第27-33页 |
| ·WGLs模型 | 第29-31页 |
| ·基于WGLs的等价性验证 | 第31-33页 |
| ·本章小结 | 第33-34页 |
| 第3章 基于WGLS的字级描述的形式化验证 | 第34-43页 |
| ·字级函数的WGLs表示 | 第35-37页 |
| ·HDL操作符的WGLs描述 | 第37-41页 |
| ·研究实例 | 第41-42页 |
| ·本章小结 | 第42-43页 |
| 第4章 高层次形式化验证模型LWGLS | 第43-50页 |
| ·LWGLs模型 | 第44-47页 |
| ·函数分解 | 第44-45页 |
| ·LWGLs模型 | 第45-47页 |
| ·加法和乘法操作的组合规则 | 第47-48页 |
| ·RTL电路的验证 | 第48-49页 |
| ·本章小结 | 第49-50页 |
| 第5章 泰勒展开图算法的改进 | 第50-59页 |
| ·泰勒展开图 | 第50-52页 |
| ·基础定义 | 第50-51页 |
| ·布尔函数的表示 | 第51-52页 |
| ·TEDs的基本算法 | 第52-54页 |
| ·加法 | 第52-53页 |
| ·乘法 | 第53-54页 |
| ·TEDs基本操作的算法 | 第54-57页 |
| ·Maple符号系统 | 第54-55页 |
| ·改进算法 | 第55-57页 |
| ·实例分析 | 第57-58页 |
| ·加法实例 | 第57页 |
| ·乘法实例 | 第57-58页 |
| ·本章小结 | 第58-59页 |
| 第6章 时序泰勒展开图 | 第59-69页 |
| ·基础知识 | 第60-62页 |
| ·泰勒展开图 | 第60-61页 |
| ·时序布尔函数 | 第61-62页 |
| ·时序泰勒展开图 | 第62-65页 |
| ·TBFs函数的TBTEDs图 | 第65-67页 |
| ·实验分析 | 第67-68页 |
| ·本章小结 | 第68-69页 |
| 结论 | 第69-71页 |
| 参考文献 | 第71-74页 |
| 攻读硕士学位期间发表的论文和取得的科研成果 | 第74-75页 |
| 致谢 | 第75页 |
