| 摘要 | 第1-5页 |
| ABSTRACT | 第5-7页 |
| 目录 | 第7-9页 |
| 图表索引 | 第9-10页 |
| 第1章 绪论 | 第10-28页 |
| ·研究背景及选题意义 | 第10-12页 |
| ·数字系统设计自动化概述 | 第12-21页 |
| ·数字电路设计领域和层次 | 第12-14页 |
| ·系统级综合(System-Level Synthesis) | 第14-15页 |
| ·高级综合(High-Level Synthesis) | 第15-17页 |
| ·RTL综合(Register-Transfer Level Synthesis) | 第17-18页 |
| ·逻辑综合(Logic-Level Synthesis) | 第18页 |
| ·工艺映射(Technology Mapping) | 第18-19页 |
| ·验证 | 第19-21页 |
| ·控制器综合的研究内容 | 第21-24页 |
| ·有限状态机分解 | 第22-23页 |
| ·状态化简 | 第23页 |
| ·状态分配 | 第23-24页 |
| ·形式验证综述 | 第24-27页 |
| ·论文的内容 | 第27-28页 |
| 第2章 控制器综合相关问题 | 第28-39页 |
| ·引言 | 第28页 |
| ·基本概念 | 第28-31页 |
| ·非完全确定有限状态时序机的状态化简 | 第31-34页 |
| ·状态化简研究进展 | 第31-32页 |
| ·定义和记号 | 第32-34页 |
| ·求解最小FSM的一般步骤 | 第34页 |
| ·状态分配 | 第34-38页 |
| ·状态分配研究进展 | 第34-35页 |
| ·经典的按权状态分配算法 | 第35-37页 |
| ·算法介绍 | 第37-38页 |
| ·本章小结 | 第38-39页 |
| 第3章 形式验证方法概述 | 第39-47页 |
| ·定理证明 | 第39-40页 |
| ·模型检验 | 第40-41页 |
| ·等价性检验方法 | 第41-43页 |
| ·形式验证在工业界的应用状况 | 第43-44页 |
| ·目前的研究热点 | 第44-45页 |
| ·半形式化验证 | 第44页 |
| ·模型检验和定理证明相结合 | 第44-45页 |
| ·SoC的验证问题 | 第45页 |
| ·将形式验证技术融入设计流程 | 第45页 |
| ·适合控制器综合的验证方法的确定 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 第4章 控制器综合正确性验证 | 第47-64页 |
| ·引言 | 第47-48页 |
| ·相关概念 | 第48-52页 |
| ·控制器综合结果验证的基本思想 | 第52-54页 |
| ·基本思想 | 第52-53页 |
| ·基本思想正确性证明 | 第53-54页 |
| ·逆向分析技术 | 第54-57页 |
| ·逆向分析基本原理 | 第54-55页 |
| ·逆向分析算法 | 第55-57页 |
| ·算法时间复杂度 | 第57页 |
| ·综合结果验证 | 第57-63页 |
| ·STG_org与STG_rd相容性验证算法 | 第57-59页 |
| ·改进的验证算法 | 第59-61页 |
| ·时间复杂度分析 | 第61页 |
| ·STG_rd与STG_ext相容性验证算法 | 第61-62页 |
| ·时间复杂度分析 | 第62-63页 |
| ·本章小结 | 第63-64页 |
| 第5章 相关数据结构设计 | 第64-68页 |
| ·控制器综合结果正确性验证步骤 | 第64页 |
| ·有限状态机的表示 | 第64-65页 |
| ·主要数据结构 | 第65-67页 |
| ·本章小结 | 第67-68页 |
| 第6章 总结与展望 | 第68-70页 |
| 参考文献 | 第70-74页 |
| 致谢 | 第74-75页 |
| 攻读学位期间发表的学术论文目录 | 第75页 |
