第1章 绪论 1
1.1 设计验证简介 1
1.2 设计验证中的关键问题 4
1.2.1 量化评估 4
1.2.2 激励生成 5
1.2.3 形式化验证 7
1.3 章节组织结构 8
参考文献 10
第2章 寄存器传输级行为描述抽象方法 12
2.1 硬件描述语言概述 12
2.1.1 硬件描述语言的产生与发展 12
2.1.2 硬件描述语言的描述特点 13
2.2 RTL行为描述的进程分析 19
2.2.1 语法与语义限制 19
2.2.2 组合进程 21
2.2.3 时钟进程 23
2.2.4 异步进程 25
2.3 寄存器传输级行为描述抽象 26
2.3.1 行为描述中的进程 26
2.3.2 过程性语句 26
2.3.3 语句的语义行为 31
2.3.4 语句的执行条件 35
2.3.5 进程的相互关系 36
2.3.6 电路模型 38
2.3.7 行为模拟方式 40
2.4 本章总结 41
参考文献 42
第3章 基于可观测性的覆盖率评估方法 43
3.1 设计验证中的可观测性 43
3.1.1 研究设计验证中的可观测性的意义 44
3.1.2 设计验证中的可观测性相关研究 46
3.2 可观测性的DFUDO模型 48
3.2.1 工作基础 48
3.2.2 动态参数化引用-定值链 49
3.2.3 HDL设计中信号可观测性的DFUDO模型 53
3.3 基于DFUDO模型的语句覆盖率评估方法 55
3.3.1 基于DFUDO模型的语句覆盖率（OSC）的定义 55
3.3.2 覆盖率评估算法 56
3.3.3 实验及分析 57
3.4 基于DFUDO模型的分支覆盖率评估方法 63
3.4.1 基于DFUDO模型的分支覆盖率（OBC）的定义 63
3.4.2 优化的覆盖率评估算法 65
3.4.3 实验及分析 66
3.5 两种基于DFUDO模型的代码覆盖率评估方法的比较 71
3.5.1 OSC与OBC的共性 71
3.5.2 OSC与OBC的差异比较 72
3.6 可观测性的COC模型 74
3.6.1 增强型进程控制树与数据流向图 74
3.6.2 控制-观测链 76
3.6.3 基于COC模型的可观测性的定义 78
3.7 基于COC模型的语句覆盖率评估方法 78
3.7.1 实现框架 78
3.7.2 电路的行为模拟 79
3.7.3 可观测性分析过程 80
3.7.4 基于COC模型的语句覆盖率的计算 81
3.7.5 实验及分析 82
3.8 本章总结 84
参考文献 86
第4章 缺项-设计错误模型 88
4.1 设计错误模型介绍 88
4.2 实际芯片的设计验证 90
4.2.1 设计简介 90
4.2.2 接口逻辑的设计验证 91
4.2.3 处理器逻辑的设计验证 93
4.3 缺项-设计错误模型 94
4.3.1 设计错误数据的分析 94
4.3.2 缺项错误模型 96
4.3.3 缺项错误模型的测试方法 99
4.3.4 实验及分析 100
4.4 设计错误的注入 104
4.4.1 软件的变异测试系统Mothra 104
4.4.2 基于Mothra的硬件设计变异测试系统 107
4.4.3 独立的硬件设计错误注入系统ErrorInjector 108
4.5 本章总结 114
参考文献 115
第5章 基于错误传播概率的量化分析方法 118
5.1 在量化评估方法中考虑错误效果的意义 118
5.2 RTL操作的错误屏蔽概率分析 119
5.2.1 一元操作的EMP分析 119
5.2.2 二元操作的EMP分析 123
5.2.3 常见字操作的错误屏蔽概率 130
5.3 基于错误屏蔽概率的静态可观测性量化分析方法 131
5.3.1 研究静态可观测性分析方法的动机 131
5.3.2 HDL设计中内部信号的静态可观测性分析方法 132
5.3.3 根据低观测根源选择内部观测点的方法 135
5.3.4 实验及分析 137
5.4 本章总结 139
参考文献 139
第6章 模拟验证的激励生成概述 141
6.1 简介 141
6.2 遗传算法用于激励生成 142
6.2.1 遗传算法的起源和发展 142
6.2.2 遗传算法的基本结构 142
6.2.3 遗传算法的技术要点 143
6.2.4 基于模拟的激励生成与遗传算法 146
6.2.5 ARTIST系统 147
6.3 确定性激励生成 148
6.3.1 基于故障模型的测试生成 148
6.3.2 基于错误模型的激励生成 150
6.4 本章总结 151
参考文献 152
第7章 基于传输故障模型的寄存器传输级激励生成 154
7.1 行为倾向驱动引擎 154
7.1.1 电路行为的表征与展现 154
7.1.2 函数或映射的属性 155
7.1.3 抽象的行为值与RTL变量的行为 160
7.1.4 行为倾向 164
7.1.5 驱动引擎 168
7.2 传输故障模型 174
7.2.1 电路故障的层次化抽象模型 175
7.2.2 传输故障的定义与组织 176
7.2.3 传输故障与逻辑故障的对应关系 177
7.3 无回溯激励生成及算法实现 178
7.3.1 无回溯激励生成 178
7.3.2 基于行为倾向驱动引擎构造无回溯测试生成算法 184
7.3.3 简单实例分析 188
7.3.4 算法特征小结 191
7.4 实验及分析 192
7.4.1 拟定的实验方案 192
7.4.2 系统实现方式 193
7.4.3 实验结果比较分析 194
7.5 本章总结 198
参考文献 198
第8章 基于行为阶段聚类的寄存器传输级激励生成 200
8.1 寄存器传输级行为描述与有限状态机 200
8.1.1 有关RTL行为描述的若干定义 200
8.1.2 有限状态机 202
8.1.3 小结 205
8.2 电路的行为阶段 206
8.2.1 阶段变量 206
8.2.2 行为阶段转换函数 209
8.2.3 小结 211
8.3 行为阶段的聚类 212
8.3.1 对电路状态聚类的动机 212
8.3.2 基于RTL行为描述的状态聚类：行为阶段聚类 214
8.3.3 小结 224
8.4 基于聚类的激励生成 224
8.4.1 故障模型 224
8.4.2 基于聚类的测试生成算法 226
8.4.3 基于聚类的ATG系统ATCLUB 228
8.5 实验及分析 236
8.6 本章总结 239
参考文献 240
第9章 覆盖率驱动的寄存器传输级激励生成 242
9.1 基于混合遗传算法的激励生成 242
9.1.1 遗传算法的改进方法 242
9.1.2 RTL模型和系统实现框架 243
9.1.3 遗传算法设计 245
9.1.4 实验及分析 251
9.2 可观测性语句覆盖率驱动的激励生成 253
9.2.1 无回溯的激励生成方案 253
9.2.2 以基于可观测性的语句覆盖率为驱动的激励生成过程 254
9.2.3 停止判断机制 256
9.2.4 选择阈值 257
9.2.5 实验及分析 257
9.3 本章总结 259
参考文献 260
第10章 布尔函数与基于电路的布尔推理 261
10.1 布尔函数 261
10.1.1 布尔函数的运算 261
10.1.2 硬件行为的模拟 262
10.2 二叉判决图 263
10.2.1 有序二叉判决图 263
10.2.2 有序二叉判决图的运算 265
10.2.3 有序二叉判决图的变量排序 266
10.2.4 BDD在形式化验证中的应用 267
10.3 布尔可满足性 270
10.3.1 布尔可满足性问题 270
10.3.2 布尔可满足性问题的算法 272
10.3.3 SAT在基于电路的布尔推理中的应用 273
10.4 静态逻辑蕴涵 278
10.4.1 静态逻辑蕴涵的基本概念 278
10.4.2 静态逻辑蕴涵的算法 279
10.4.3 静态逻辑蕴涵的应用 281
10.5 本章总结 283
参考文献 284
第11章 基于可满足性的增量等价性检验方法 287
11.1 等价性检验介绍 287
11.1.1 研究背景及意义 287
11.1.2 等价性检验综述 290
11.2 基于可满足性的增量等价性检验方法 299
11.2.1 SAT在等价性检验中的应用 300
11.2.2 基于可满足性的增量等价性检验方法 301
11.2.3 实验及分析 305
11.3 本章总结 308
参考文献 308
第12章 验证包含黑盒的电路设计的形式化方法 311
12.1 集成电路设计中的黑盒问题 311
12.2 验证包含黑盒的电路设计的常用方法 312
12.2.1 基于BDD的方法 312
12.2.2 基于SAT的方法 314
12.3 结合逻辑模拟与布尔可满足性的验证方法 315
12.3.1 基于量化的布尔可满足性验证方法 315
12.3.2 逻辑模拟与布尔可满足性算法的结合 317
12.3.3 算法的改进 319
12.3.4 实验及分析 320
12.4 包含黑盒的电路设计验证方法在逻辑错误诊断中的应用 323
12.4.1 错误诊断方法的相关研究 324
12.4.2 结合逻辑模拟与布尔可满足性的错误诊断方法 331
12.4.3 实验及分析 334
12.5 本章总结 336
参考文献 336
第13章 极小布尔不可满足问题 339
13.1 引言 339
13.2 识别MU式的算法 340
13.3 提取MU子式的近似算法 344
13.3.1 自适应核搜索算法 344
13.3.2 利用蕴涵图的近似提取算法 347
13.3.3 利用蕴涵图提取MU子式的算法误差模拟实验 350
13.3.4 AMUSE方法 351
13.4 提取MU子式的精确算法 355
13.4.1 利用线性规划的提取算法 355
13.4.2 遍历子句的算法及预先局部赋值优化策略 358
13.4.3 实验及分析 360
13.5 本章总结 362
参考文献 362
第14章 模型检验在电路设计验证中的应用研究 364
14.1 模型检验简介 364
14.1.1 有限状态转移模型 364
14.1.2 时态逻辑 366
14.1.3 模型检验 370
14.1.4 满足时态逻辑公式状态集合的不动点表征 372
14.2 符号模型检验中转移关系的分组策略 373
14.2.1 布尔函数的支撑变量 373
14.2.2 二叉判决图的结点与支撑向量 374
14.2.3 基于支撑向量海明距离的转移关系分组策略 375
14.2.4 实验及分析 376
14.3 结合ATG和SAT的无界模型检验前像计算方法 377
14.3.1 系统前像计算方法及动机 378
14.3.2 ATG过程减少状态变量上的赋值 379
14.3.3 实验及分析 380
14.4 基于SAT的电路属性检验 382
14.4.1 RTL设计到CNF的转化 383
14.4.2 针对电路的SAT求解器优化 384
14.4.3 多时帧搜索策略 389
14.4.4 实验及分析 390
14.5 本章总结 392
参考文献 392
第15章 总结与展望 395
15.1 总结 395
15.2 展望 397
参考文献 401
索引 402