数字集成电路设计验证：量化评估、激励生成、形式化验证
出版时间：2010年版
内容简介
《数字集成电路设计验证：量化评估、激励生成、形式化验证》内容涉及数字集成电路设计验证的三个主要方面：量化评估、激励生成和形式化验证。主要包括寄存器传输级（RTL）电路建模、基于可观测性的覆盖率评估方法、设计错误模型；基于故障模型的激励生成、基于RTL行为模型的激励生成、覆盖率驱动的激励生成；基于可满足性的等价性检验、包含黑盒电路的形式化验证，以及不可满足问题。全书图文并茂，阐述了作者及其科研团队自主创新的研究成果和结论，对致力于数字集成电路设计验证方法研究的科研人员（尤其是在读研究生），具有较大的学术参考价值，也可用作集成电路专业的高等院校教师、研究生和高年级本科生的教学参考书。
目录
FOREWORD
前言
第1章 绪论
1.1 设计验证简介
1.2 设计验证中的关键问题
1.2.1 量化评估
1.2.2 激励生成
1.2.3 形式化验证
1.3 章节组织结构
参考文献
第2章 寄存器传输级行为描述抽象方法
2.1 硬件描述语言概述
2.1.1 硬件描述语言的产生与发展
2.1.2 硬件描述语言的描述特点
2.2 RTL行为描述的进程分析
2.2.1 语法与语义限制
2.2.2 组合进程
2.2.3 时钟进程
2.2.4 异步进程
2.3 寄存器传输级行为描述抽象
2.3.1 行为描述中的进程
2.3.2 过程性语句
2.3.3 语句的语义行为
2.3.4 语句的执行条件
2.3.5 进程的相互关系
2.3.6 电路模型
2.3.7 行为模拟方式
2.4 本章总结
参考文献
第3章 基于可观测性的覆盖率评估方法
3.1 设计验证中的可观测性
3.1.1 研究设计验证中的可观测性的意义
3.1.2 设计验证中的可观测性相关研究
3.2 可观测性的DFUDO模型
3.2.1 工作基础
3.2.2 动态参数化引用一定值链
3.2.3 HDL设计中信号可观测性的DFUD0模型
3.3 基于DFUD0模型的语句覆盖率评估方法
3.3.1 基于DFUDO模型的语句覆盖率（OSC）的定义
3.3.2 覆盖率评估算法
3.3.3 实验及分析
3.4 基于DFUDO模型的分支覆盖率评估方法
3.4.1 基于DFUDO模型的分支覆盖率（OBC）的定义
3.4.2 优化的覆盖率评估算法
3.4.3 实验及分析
3.5 两种基于DFUDO模型的代码覆盖率评估方法的比较
3.5.1 OSC与OBC的共性
3.5.2 OSC与OBC的差异比较
3.6 可观测性的COC模型
3.6.1 增强型进程控制树与数据流向图
3.6.2 控制－观测链
3.6.3 基于COC模型的可观测性的定义
3.7 基于COC模型的语句覆盖率评估方法
3.7.1 实现框架
3.7.2 电路的行为模拟
3.7.3 可观测性分析过程
3.7.4 基于COC模型的语句覆盖率的计算
3.7.5 实验及分析
3.8 本章总结
参考文献
第4章 缺项－设计错误模型
4.1 设计错误模型介绍
4.2 实际芯片的设计验证
4.2.1 设计简介
4.2.2 接口逻辑的设计验证
4.2.3 处理器逻辑的设计验证
4.3 缺项－设计错误模型
4.3.1 设计错误数据的分析
4.3.2 缺项错误模型
4.3.3 缺项错误模型的测试方法
4.3.4 实验及分析
4.4 设计错误的注入
4.4.1 软件的变异测试系统Mothra
4.4.2 基于Mothra的硬件设计变异测试系统
4.4.3 独立的硬件设计错误注入系统ErrorInjector
4.5 本章总结
参考文献
第5章 基于错误传播概率的量化分析方法
5.1 在量化评估方法中考虑错误效果的意义
5.2 RTL操作的错误屏蔽概率分析
5.2.1 一元操作的EMP分析
5.2.2 二元操作的EMP分析
5.2.3 常见字操作的错误屏蔽概率
5.3 基于错误屏蔽概率的静态可观测性量化分析方法
5.3.1 研究静态可观测性分析方法的动机
5.3.2 HDL设计中内部信号的静态可观测性分析方法
5.3.3 根据低观测根源选择内部观测点的方法
5.3.4 实验及分析
5.4 本章总结
参考文献
第6章 模拟验证的激励生成概述
6.1 简介
6.2 遗传算法用于激励生成
6.2.1 遗传算法的起源和发展
6.2.2 遗传算法的基本结构
6.2.3 遗传算法的技术要点
6.2.4 基于模拟的激励生成与遗传算法
6.2.5 ARTIST系统
6.3 确定性激励生成
6.3.1 基于故障模型的测试生成
6.3.2 基于错误模型的激励生成
6.4 本章总结
参考文献
第7章 基于传输故障模型的寄存器传输级激励生成
7.1 行为倾向驱动引擎
7.1.1 电路行为的表征与展现
7.1.2 函数或映射的属性
7.1.3 抽象的行为值与RTL变量的行为
7.1.4 行为倾向
7.1.5 驱动引擎
7.2 传输故障模型
7.2.1 电路故障的层次化抽象模型
7.2.2 传输故障的定义与组织
7.2.3 传输故障与逻辑故障的对应关系
7.3 无回溯激励生成及算法实现
7.3.1 无回溯激励生成
7.3.2 基于行为倾向驱动引擎构造无回溯测试生成算法
7.3.3 简单实例分析
7.3.4 算法特征小结
7.4 实验及分析
7.4.1 拟定的实验方案
7.4.2 系统实现方式
7.4.3 实验结果比较分析
7.5 本章总结
参考文献
……
第8章 基于行为阶段聚类的寄存器传输级激励生成
第9章 覆盖率驱动的寄存器传输级激励生成
第10章 布尔函数与基于电路的布尔推理
第11章 基于可满足性的增量等价性检验方法
第12章 验证包含黑盒的电路设计的形式化方法
第13章 极小布尔不可满足问题
第14章 模型检验在电路设计验证中的应用研究
第15章 总结与展望
索引