| 第一章 绪论 | 第1-30页 |
| 1．1 快速发展的微电子技术 | 第20-21页 |
| 1．2 集成电路设计与功能验证 | 第21-22页 |
| 1．3 集成电路功能验证面临的挑战 | 第22-25页 |
| 1．3．1 模拟激励生成 | 第23-24页 |
| 1．3．2 模拟验证结果检验 | 第24页 |
| 1．3．3 模拟验证效果分析 | 第24-25页 |
| 1．3．4 模拟验证环境建模 | 第25页 |
| 1．4 工程学指导下的集成电路功能验证 | 第25-27页 |
| 1．5 本文的课题来源 | 第27页 |
| 1．6 本文的主要研究内容 | 第27-30页 |
| 第二章 功能验证方法及研究进展综述 | 第30-50页 |
| 2．1 引言 | 第30页 |
| 2．2 验证方法概述 | 第30-36页 |
| 2．2．1 验证的分类方法 | 第31页 |
| 2．2．2 基于模拟的验证方法 | 第31-35页 |
| 2．2．2．1 基于事件的模拟 | 第33页 |
| 2．2．2．2 基于周期的模拟 | 第33页 |
| 2．2．2．3 确定性模拟方法 | 第33-34页 |
| 2．2．2．4 随机模拟方法 | 第34页 |
| 2．2．2．5 软硬件协同验证方法 | 第34页 |
| 2．2．2．6 硬件加速 | 第34页 |
| 2．2．2．7 硬件仿真 | 第34页 |
| 2．2．2．8 快速原型验证 | 第34-35页 |
| 2．2．2．9 模拟/混合验证方法 | 第35页 |
| 2．2．2．10 基于事务的模拟方法 | 第35页 |
| 2．2．3 形式化验证方法 | 第35-36页 |
| 2．2．3．1 定理证明 | 第35-36页 |
| 2．2．3．2 模型检验 | 第36页 |
| 2．2．3．3 等价性检验 | 第36页 |
| 2．3 功能验证方法的研究进展 | 第36-49页 |
| 2．3．1 功能验证新技术 | 第37-45页 |
| 2．3．1．1 半形式化验证方法研究进展 | 第37-38页 |
| 2．3．1．2 基于覆盖率反馈的模拟激励生成方法研究进展 | 第38-39页 |
| 2．3．1．3 模拟验证结果检查方法研究的进展 | 第39-41页 |
| 2．3．1．4 覆盖率度量方法的研究进展 | 第41-44页 |
| 2．3．1．5 模拟验证方法的其它进展 | 第44-45页 |
| 2．3．2 功能验证方法学的新进展 | 第45-49页 |
| 2．3．2．1 基于功能虚拟原型的统一验证方法学 | 第45-47页 |
| 2．3．2．2 DFV验证方法学 | 第47页 |
| 2．3．2．3 基于规范的验证方法学 | 第47-48页 |
| 2．3．2．4 基于断言的验证方法学 | 第48-49页 |
| 2．3．2．5 其它验证方法学 | 第49页 |
| 2．4 结束语 | 第49-50页 |
| 第三章 基于功能信息的验证工程学研究 | 第50-84页 |
| 3．1 引言 | 第50-51页 |
| 3．2 验证方法的发展方向原则 | 第51-58页 |
| 3．2．1 抽象化原则 | 第51-53页 |
| 3．2．2 形式化原则 | 第53-58页 |
| 3．2．2．1 从功能验证的目的根源考虑 | 第53-55页 |
| 3．2．2．2 从验证技术方法的角度考虑 | 第55-58页 |
| 3．3 基于功能信息的验证工程学的理论基础 | 第58-69页 |
| 3．3．1 工程学思想的重要性 | 第59-62页 |
| 3．3．1．1 软件危机和软件工程的借鉴 | 第59-60页 |
| 3．3．1．2 集成电路的功能验证需要工程学思想 | 第60-62页 |
| 3．3．2 功能信息的意义 | 第62-69页 |
| 3．3．2．1 功能信息的作用分析 | 第62-66页 |
| 3．3．2．2 功能信息的实例应用 | 第66-69页 |
| 3．3．3 结论 | 第69页 |
| 3．4 基于功能信息的验证工程学 | 第69-83页 |
| 3．4．1 功能信息的定义 | 第69-70页 |
| 3．4．2 验证工程学的基本内容 | 第70-71页 |
| 3．4．3 基于功能信息的验证工程学的过程模型 | 第71-81页 |
| 3．4．3．1 设计实现——功能信息的生成 | 第73-75页 |
| 3．4．3．2 功能验证——功能信息的应用 | 第75-77页 |
| 3．4．3．2．1 SoC功能验证中的功能信息引入流程 | 第76页 |
| 3．4．3．2．2 IP模块功能验证的功能信息引入流程 | 第76-77页 |
| 3．4．3．3 理论支持——形式化和标准化方法 | 第77-80页 |
| 3．4．3．3．1 形式化理论研究 | 第78页 |
| 3．4．3．3．2 标准制定 | 第78-80页 |
| 3．4．3．4 技术方法支持——基于功能信息的验证技术 | 第80-81页 |
| 3．4．4 基于功能信息验证工程学的过渡演化模型 | 第81-83页 |
| 3．4．4．1 基于功能信息的验证工程学的演化模型 | 第81-82页 |
| 3．4．4．2 个体机构引入基于功能信息的验证工程学的方法 | 第82-83页 |
| 3．5 结束语 | 第83-84页 |
| 第四章 基于指令模板的测试程序自动生成方法研究 | 第84-132页 |
| 4．1 引言 | 第84-87页 |
| 4．1．1 基于指令模板的验证激励自动生成方法概述 | 第85-87页 |
| 4．2 指令模板的规范化设计方法研究 | 第87-109页 |
| 4．2．1 指令模板的分层描述方法研究 | 第88-99页 |
| 4．2．1．1 格式层描述 | 第89-91页 |
| 4．2．1．1．1 基于指令编码的结构解析 | 第89-90页 |
| 4．2．1．1．2 格式层模板描述 | 第90-91页 |
| 4．2．1．2 指令模板内容层 | 第91-95页 |
| 4．2．1．2．1 指令模板的单元内容约定 | 第91-92页 |
| 4．2．1．2．2 指令模板单元内容描述 | 第92-95页 |
| 4．2．1．3 模板约束层 | 第95-99页 |
| 4 2 1．3．1“互联”(linkage)的描述 | 第95-97页 |
| 4．2．1．3．2 “约束”(constraint)的描述 | 第97-99页 |
| 4．2．2 模板综合方法研究 | 第99-105页 |
| 4．2．2．1 数据结构的建立 | 第99-101页 |
| 4．2．2．2 模板综合算法 | 第101-105页 |
| 4．2．2．2．1 单元链接建立算法 | 第102-103页 |
| 4．2．2．2．2 参数传播算法 | 第103-104页 |
| 4．2．2．2．3 约束链接的建立算法 | 第104-105页 |
| 4．2．3 基于分层模板的指令生成的基本方法 | 第105-107页 |
| 4．2．4 指令模板检验方法 | 第107-109页 |
| 4．2．4．1 静态检查方法 | 第107-108页 |
| 4．2．4．2 动态验证方法 | 第108-109页 |
| 4．3 基于指令模板的测试程序生成方法 | 第109-123页 |
| 4．3．1 指令生成过程的遍历 | 第109页 |
| 4．3．2 指令生成过程的异常控制方法研究 | 第109-118页 |
| 4．3．2．1 已有相关研究方法参考 | 第110-111页 |
| 4．3．2．2 分支交叉方法 | 第111-118页 |
| 4．3．2．2．1 采用分支交叉方法的测试程序结构 | 第111-112页 |
| 4．3．2．2．2 分支交叉跳转条件的分析 | 第112-114页 |
| 4．3．2．2．3 分支交叉跳转条件的设定 | 第114-116页 |
| 4．3．2．2．4 包含分支交叉控制的测试程序生成 | 第116-118页 |
| 4．3．3 测试程序优化 | 第118-123页 |
| 4．3．3．1 相关研究工作 | 第118-119页 |
| 4．3．3．2 基于自私基因算法优化模板访问过程 | 第119-123页 |
| 4．3．3．2．1 自私基因算法简介 | 第119-120页 |
| 4．3．3．2．2 优化过程 | 第120-123页 |
| 4．4 基于模板的指令生成系统(TIGS) | 第123-124页 |
| 4．5 验证实例 | 第124-129页 |
| 4．5．1 MIPS处理器指令系统介绍 | 第124-127页 |
| 4．5．2 MIPS I指令模板描述 | 第127-128页 |
| 4．5．2．1 格式层描述 | 第127-128页 |
| 4．5．2．2 MIPS I指令模板内容层描述 | 第128页 |
| 4．5．2．3 MIPS I指令模板约束层描述 | 第128页 |
| 4．5．3 基于 TIGS的实例运行及结果讨论 | 第128-129页 |
| 4．6 结束语 | 第129-132页 |
| 第五章 基于断言的监视器模块自动生成方法研究 | 第132-152页 |
| 5．1 引言 | 第132-133页 |
| 5．2 相关研究介绍 | 第133-134页 |
| 5．3 基于断言的设计属性描述 | 第134-141页 |
| 5．3．1 用时态逻辑语言描述设计属性 | 第134-137页 |
| 5．3．2 基于简单断言的属性描述方法 | 第137页 |
| 5．3．3 属性规范语言 | 第137-140页 |
| 5．3．3．1 属性规范语言的组织结构 | 第138-139页 |
| 5．3．3．2 属性规范语言的词法结构 | 第139-140页 |
| 5．3．4 基于 Stanford简单断言和 PSL属性语言的监视器断言子集定义 | 第140-141页 |
| 5．4 监视器模块生成方法 | 第141-150页 |
| 5．4．1 将监视器属性描述转换为事件序列 | 第142-144页 |
| 5．4．2 基于事件序列的监视器模块生成 | 第144-149页 |
| 5．4．2．1 采用同步延迟的事件序列识别方法 | 第145-146页 |
| 5．4．2．2 基于有限状态机(FSM)的事件序列识别方法 | 第146-149页 |
| 5．4．2．3 反馈方式的确定 | 第149页 |
| 5．4．3 自动生成方法实现 | 第149-150页 |
| 5．5 总结与分析 | 第150-152页 |
| 第六章 验证环境建模技术研究 | 第152-176页 |
| 6．1 引言 | 第152-153页 |
| 6．2 PLL行为模型实现 | 第153-155页 |
| 6．3 倍频电路验证模型的数字实现技术研究 | 第155-175页 |
| 6．3．1 相关研究介绍 | 第155-156页 |
| 6．3．2 ADPLL的设计方法 | 第156-164页 |
| 6．3．2．1 数字鉴相器模块设计 | 第156-158页 |
| 6．3．2．2 数字环路滤波模块设计 | 第158-159页 |
| 6．3．2．3 数控振荡器模块设计 | 第159页 |
| 6．3．2．4 分频器模块设计 | 第159-164页 |
| 6．3．2．4．1 可配置非幂方分频器的分频原理 | 第159-160页 |
| 6．3．2．4．2 可配置非幂方分频器的分频算法 | 第160-161页 |
| 6．3．2．4．3 可配置非幂方分频器的Verilog-HDL实现 | 第161-163页 |
| 6．3．2．4．4 可配置非幂方分频器的配置方法 | 第163-164页 |
| 6．3．2．4．5 与传统设计方法的性能比较 | 第164页 |
| 6．3．3 用于倍频验证模型的ADPLL参数分析 | 第164-167页 |
| 6．3．3．1 ADPLL参数举例分析一 | 第165页 |
| 6．3．3．2 ADPLL参数举例分析二 | 第165-167页 |
| 6．3．4 一种新的倍频电路验证建模方法 | 第167-175页 |
| 6．3．4．1 时钟倍频基本原理分析 | 第167-168页 |
| 6．3．4．2 周期分割的倍频验证模型设计 | 第168-170页 |
| 6．3．4．2．1 系统结构设计 | 第168-169页 |
| 6．3．4．2．2 误差补偿方法 | 第169-170页 |
| 6．3．4．3 引入ADPLL思想完善倍频验证模型 | 第170-171页 |
| 6．3．4．4 倍频电路验证模型的HDL编码实现 | 第171-174页 |
| 6．3．4．5 误差分析及参数分析 | 第174-175页 |
| 6．4 结束语 | 第175-176页 |
| 第七章 总结与展望 | 第176-178页 |
| 7．1 总结 | 第176-177页 |
| 7．2 展望 | 第177-178页 |
| 参考文献 | 第178-184页 |
| 攻读博士学位期间发表的论文 | 第184页 |
