文摘
英文文摘
论文说明:图表目录
声明
第1章 绪论
1.1 引言
1.2 ASIP应用背景
1.3 ASIP设计
1.4 ASIP验证的研究动机与目标
1.5 验证方法概述
1.5.1 基于仿真的验证方法
1.5.2 基于形式化方法的验证
1.5.3 验证方法小结
1.6 体系结构描述方法
1.6.1 体系结构描述语言
1.6.2 Petri网
1.6.3 小结
1.7 本文的主要工作
1.8 论文组织
笫2章 ASIP体系结构描述
2.1 引言
2.2 已有工作
2.3 ASIP体系结构
2.4 HDPN
2.4.1 Petri网原理
2.4.2 HDPN
2.5 基于HDPN的ASIP设计
2.6 描述实例
2.7 小结
第3章 静态属性验证
3.1 引言
3.2 静态属性
3.2.1 结构有效性
3.2.2 接口一致性
3.2.3 行为确定性
3.2.4 活性
3.2.5 公平性
3.2.6 语义映射
3.2.7 时间约束
3.3 小结
第4章 动态属性验证
4.1 引言
4.2 已有工作
4.3 模型描述和属性描述方法
4.3.1 NuSMV
4.3.2 属性描述方法
4.4 模型提取方法
4.4.1 分层检测方法
4.4.2 局部模型检测方法
4.5 实例
4.6 小结
第5章 从HDPN到NuSMV描述的转换
5.1 引言
5.2 HDPN和NuSMV的比较
5.3 HDPN到NuSMV描述的转换
5.3.1 全局模型的转换
5.3.2 局部模型的转换
5.4 实例分析
5.5 小结
第6章 流水线处理器验证
6.1 引言
6.2 DLX流水线的验证
6.2.1 已有工作
6.2.2 流水线结构
6.2.3 流水线模型
6.2.4 流水线的基本属性
6.2.5 流水线验证
6.2.6 小结
6.3 带旁路的流水线验证
6.3.1 已有工作
6.3.2 旁路流水线
6.3.3 流水线模型
6.3.4 属性定义
6.3.5 实例分析
6.4 小结
第7章 乱序执行处理器验证
7.1 引言
7.2 已有工作
7.3 基于Tomasulo算法的处理器设计验证
7.3.1 Tomasulo算法
7.3.2 基于Tomulo算法处理器的模型提取
7.3.3 属性提取
7.4 支持猜测执行和Tomasulo算法的处理器设计验证
7.4.1 支持猜测执行和Tomasulo算法的处理器体系结构
7.4.2 模型提取
7.4.3 属性提取
7.4.4 处理器验证
7.5 存储器访问操作的建模和验证
7.6 小结
第8章 结束语
8.1 研究工作总结
8.2 进一步研究工作的展望
参考文献
在读期间发表的学术论文与取得的研究成果
致谢