基于PSA的集成电路形式验证方法研究
| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第1章 绪论 | 第11-19页 |
| ·课题的背景及意义 | 第11-14页 |
| ·研究现状 | 第14-16页 |
| ·本文的工作 | 第16-18页 |
| ·论文的组织结构 | 第18-19页 |
| 第2章 数字电路的形式验证综述 | 第19-45页 |
| ·形式验证的数学基础 | 第19-34页 |
| ·基于正则的判决图的形式验证 | 第19-29页 |
| ·代数方法 | 第29-34页 |
| ·形式验证方法 | 第34-44页 |
| ·等价性检验 | 第34-37页 |
| ·模型检验 | 第37-43页 |
| ·定理证明 | 第43-44页 |
| ·本章小结 | 第44-45页 |
| 第3章 基于关系模型结合定理证明的定界模型检验 | 第45-71页 |
| ·引言 | 第45-46页 |
| ·验证框架 | 第46-47页 |
| ·性质表示 | 第47-53页 |
| ·带有测试的 Kleene 代数 | 第47-48页 |
| ·高级语言概念 | 第48-49页 |
| ·HLL 的关系模型 | 第49-51页 |
| ·一个例子 | 第51-53页 |
| ·系统建模 | 第53-58页 |
| ·控制逻辑建模 | 第53-55页 |
| ·数字电路部件建模 | 第55-58页 |
| ·基于定理证明的模型检验 | 第58-65页 |
| ·数字电路时序展开 | 第58-60页 |
| ·定理证明方法 | 第60-62页 |
| ·验证示例 | 第62-65页 |
| ·实验结果与分析 | 第65-68页 |
| ·本章小结 | 第68-71页 |
| 第4章 基于多项式理想良性基的等价性验证 | 第71-87页 |
| ·引言 | 第71-73页 |
| ·拟解决的主要问题 | 第73-74页 |
| ·数据通路的建模 | 第74-76页 |
| ·等价性验证总体思路 | 第76-77页 |
| ·等价性验证方法 | 第77-83页 |
| ·代数角度功能等价定义 | 第77-78页 |
| ·等价问题求解 | 第78-80页 |
| ·验证框架 | 第80-83页 |
| ·验证示例 | 第83-84页 |
| ·实验结果及分析 | 第84-86页 |
| ·本章小结 | 第86-87页 |
| 第5章 基于 PSA 的模块化验证方法 | 第87-106页 |
| ·引言 | 第87-88页 |
| ·数字电路的模块化模型 | 第88-89页 |
| ·数字电路功能计算 | 第89-94页 |
| ·一个例子 | 第94-97页 |
| ·模块化的验证方法 | 第97-102页 |
| ·模型检验算法 | 第97-98页 |
| ·等价性验证算法 | 第98-102页 |
| ·实验结果及分析 | 第102-105页 |
| ·模型检验实验 | 第102-103页 |
| ·等价性验证实验 | 第103-105页 |
| ·本章小结 | 第105-106页 |
| 结论 | 第106-108页 |
| 参考文献 | 第108-120页 |
| 攻读博士学位期间发表的论文和取得的科研成果 | 第120-121页 |
| 致谢 | 第121-122页 |
| 个人简历 | 第122页 |
