| 第一章 绪论 | 第1-26页 |
| 1．1 研究背景及选题意义 | 第11-12页 |
| 1．2 数字系统设计自动化概述 | 第12-18页 |
| 1．2．1 设计领域和层次 | 第12-14页 |
| 1．2．2 系统级综合 | 第14-15页 |
| 1．2．3 高级综合 | 第15-16页 |
| 1．2．4 RTL综合 | 第16-17页 |
| 1．2．5 逻辑级综合 | 第17-18页 |
| 1．2．6 工艺映射 | 第18页 |
| 1．3 控制器综合 | 第18-22页 |
| 1．3．1 有限状态机分解 | 第20-21页 |
| 1．3．2 状态化简 | 第21页 |
| 1．3．3 状态分配 | 第21-22页 |
| 1．4 测试 | 第22-23页 |
| 1．5 验证 | 第23-24页 |
| 1．6 本文完成的主要工作 | 第24-25页 |
| 1．7 小结 | 第25-26页 |
| 第二章 验证技术综述及控制器综合验证策略的确定 | 第26-39页 |
| 2．1 引言 | 第26-27页 |
| 2．2 验证方法概述 | 第27-34页 |
| 2．2．1 验证的基本概念 | 第27-28页 |
| 2．2．2 模拟验证 | 第28-30页 |
| 2．2．2．1 基本原理 | 第29页 |
| 2．2．2．2 步骤 | 第29页 |
| 2．2．2．3 方法 | 第29-30页 |
| 2．2．2．4 特点 | 第30页 |
| 2．2．3 符号模拟 | 第30-31页 |
| 2．2．4 形式验证 | 第31-34页 |
| 2．2．4．1 含义 | 第31-32页 |
| 2．2．4．2 任务 | 第32页 |
| 2．2．4．3 基本过程 | 第32页 |
| 2．2．4．4 目前的主要方法 | 第32-34页 |
| 2．3 符号模型检验 | 第34-36页 |
| 2．4 控制器综合验证策略的确定 | 第36-37页 |
| 2．4．1 适合控制器综合的验证方法的确定 | 第36-37页 |
| 2．4．2 基于STG图同构求解的控制器综合结果验证的基本思想 | 第37页 |
| 2．4．3 基于STG图同构求解的控制器综合结果验证方法的特点 | 第37页 |
| 2．5 小结 | 第37-39页 |
| 第三章 逆向分析技术的研究 | 第39-47页 |
| 3．1 引言 | 第39页 |
| 3．2 逻辑函数 | 第39-40页 |
| 3．3 控制器的行为描述 | 第40-43页 |
| 3．3．1 有限状态机 | 第41-43页 |
| 3．3．2 状态转换图 | 第43页 |
| 3．4 控制器的结构实现 | 第43-44页 |
| 3．5 逆向分析算法 | 第44-46页 |
| 3．5．1 基本思想 | 第44-45页 |
| 3．5．2 逆向分析算法 | 第45-46页 |
| 3．6 算法分析 | 第46页 |
| 3．6．1 算法推论 | 第46页 |
| 3．6．2 时间复杂性 | 第46页 |
| 3．7 小结 | 第46-47页 |
| 第四章 控制器综合结果的验证 | 第47-55页 |
| 4．1 引言 | 第47页 |
| 4．2 等价和最小化 | 第47-49页 |
| 4．2．1 状态等价 | 第47-48页 |
| 4．2．2 完全确定有限状态机的最小化 | 第48-49页 |
| 4．3 等价性验证 | 第49-53页 |
| 4．3．1 图同构问题的描述 | 第50-51页 |
| 4．3．1．1 图的同构 | 第50-51页 |
| 4．3．1．2 图同构求解的一般方法 | 第51页 |
| 4．3．2 等价性证明同构问题的描述 | 第51-53页 |
| 4．3．2．1 算法思想 | 第51页 |
| 4．3．2．2 等价性验证算法 | 第51-53页 |
| 4．4 算法正确性 | 第53-54页 |
| 4．5 算法复杂性讨论 | 第54页 |
| 4．6 小结 | 第54-55页 |
| 第五章 结束语 | 第55-57页 |
| 5．1 总结 | 第55页 |
| 5．2 将来的工作 | 第55-57页 |
| 参考文献 | 第57-63页 |
| 致谢 | 第63页 |