全面的功能验证：完整的工业流程

　　《全面的功能验证：完整的工业流程》分为5个部分。第1部分的内容是功能验证概述，包括概念背景、验证计划、验证策略和一些基本练习。第1部分还介绍了验证周期的概念和层次化验证的概念，以及在实践中怎样将巨型设计分解为可验证的单元。第2部分和第3部分关注两个最主要的功能验证方法：基于模拟的验证方法和形式验证方法。第4部分把注意力集中在验证周期的后期阶段，包括回归测试和“逃逸”错误分析，以及一些高级的验证技术。第5部分，是一些验证实例研究的集合，进一步强调了验证周期和验证过程中的相关概念。《全面的功能验证：完整的工业流程》既可作为科研院所、高等工科院校计算机、电子、微电子等专业的教材或教学参考书，也可作为集成电路验证领域的工程师的技术指南或工具书。

　　威立（Bruce Wile）是IBM杰出工程师。他是IBM系统与技术组ASIC首席工程师，在这个岗位上，他领导开发了当前和下一代的服务器芯片组。自从1985年从宾夕法尼亚州立大学毕业并开始职业生涯，Wile先生在功能验证领域工作了18年。他曾先后担任许多芯片和系统的验证工程师，包括开始的IBMS／390ES／9000系列缓存和存储控制器单元，进而是处理器、I／O设备以及整个系统。在验证生涯中，他还担任着验证组领导和管理岗位。2000年，Wile先生被任命为IBM服务器芯片验证组长，负责整个IBM服务器全线产品的验证技术开发和执。……

译者序
　　对本书的评论
　　原书序
　　前言
　　第1部分 验证简介
　　第1章 芯片设计的验证5
　　1.1 功能验证简介5
　　1.2 验证面临的挑战9
　　1.2.1 状态空间爆炸的挑战9
　　1.2.2 查找不正确行为的挑战10
　　1.3 验证的任务和目标12
　　1.4 验证的开销15
　　1.4.1 工程开销和对独立验证团队的需求16
　　1.4.2 设计自动化工具17
　　1.4.3 时间17
　　1.5 本书范畴以外的验证领域18
　　1.6 验证周期：一个结构化的流程18
　　1.6.1 功能规范20
　　1.6.2 建立验证计划20
　　1.6.3 开发环境20
　　1.6.4 调试硬件描述语言和环境21
　　1.6.5 回归测试21
　　1.6.6 硬件制造22
　　1.6.7 调试流片后的硬件（系统测试）22
　　1.6.8 “逃逸”错误分析22
　　1.6.9 常见的中断验证周期的情况23
　　1.7 本章小结23
　　1.8 习题24
　　
　　第2章 验证流程26
　　2.1 验证层次26
　　2.1.1 验证等级26
　　2.1.2 怎样选择验证等级30
　　2.2 验证策略34
　　2.2.1 驱动原理34
　　2.2.2 检查策略37
　　2.2.3 检查黑盒设计41
　　2.2.4 验证策略汇总44
　　2.2.5 通用的模拟验证环境46
　　2.2.6 验证方法学的进展46
　　2.3 本章小结51
　　2.4 习题52
　　
　　第3章 基于模拟的验证基础55
　　3.1 基本验证环境：测试平台55
　　3.1.1 激励模块56
　　3.1.2 监视器60
　　3.1.3 检查器62
　　3.1.4 记分板62
　　3.1.5 待验证设计64
　　3.2 观察点：黑盒、白盒和灰盒验证65
　　3.2.1 黑盒65
　　3.2.2 白盒65
　　3.2.3 灰盒66
　　3.3 基于断言的验证概述67
　　3.3.1 断言的重要性68
　　3.3.2 断言表达设计意图69
　　3.3.3 断言的分类69
　　3.4 测试平台和测试策略71
　　3.4.1 确定性的测试平台72
　　3.4.2 自检查的测试平台73
　　3.5 本章小结76
　　3.6 习题76
　　
　　第4章 验证计划78
　　4.1 功能规范78
　　4.2 验证计划的演进79
　　4.3 验证计划的内容80
　　4.3.1 验证层次的描述81
　　4.3.2 必需的工具81
　　4.3.3 风险和依赖82
　　4.3.4 待验证的功能83
　　4.3.5 细节测试及方法：环境84
　　4.3.6 覆盖率要求88
　　4.3.7 测试用例场景：矩阵88
　　4.3.8 资源需求89
　　4.3.9 进度细节90
　　4.4 验证实例：Calc191
　　4.4.1 设计描述91
　　4.4.2 为Calc1建立验证计划94
　　4.4.3 Calc1设计的确定性验证99
　　4.5 本章小结102
　　4.6 习题103
　　
　　第2部分 基于模拟的验证
　　第5章 硬件描述语言和模拟引擎107
　　5.1 硬件描述语言108
　　5.1.1 硬件描述语言建模层次108
　　5.1.2 硬件描述语言在验证方面的应用115
　　5.2 模拟引擎介绍119
　　5.2.1 速度与精度120
　　5.2.2 选择正确的方法121
　　5.3 事件驱动模拟122
　　5.3.1 层次化模型网络122
　　5.3.2 随时间变化进行的模型评估124
　　5.3.3 模型评估中的事件驱动控制125
　　5.3.4 实现一个事件驱动的模拟引擎框架129
　　5.4 改善模拟吞吐量134
　　5.5 基于周期的模拟137
　　5.5.1 同步设计138
　　5.5.2 基于周期的模拟算法139
　　5.5.3 对基本的基于周期的模拟引擎进行扩展141
　　5.6 波形观察器144
　　5.7 本章小结147
　　5.8 习题148
　　
　　第6章 创建环境149
　　6.1 测试平台描述工具149
　　6.1.1 采用硬件描述语言作为测试平台描述工具150
　　6.1.2 C/C++库155
　　6.1.3 高级验证语言172
　　6.1.4 其它测试平台描述工具180
　　6.2 验证覆盖率181
　　6.2.1 概述182
　　6.2.2 功能验证覆盖率与制造过程中的测试覆盖率183
　　6.2.3 结构覆盖率184
　　6.2.4 功能覆盖率186
　　6.2.5 大量覆盖率数据的采集和管理189
　　6.2.6 正确的覆盖率分析策略190
　　6.3 本章小结191
　　6.4 习题191
　　
　　第7章 基于模拟的测试激励生成策略193
　　7.1 Calc2概述193
　　7.1.1 Calc2验证计划196
　　7.1.2 Calc2及其测试激励生成策略201
　　7.2 测试激励生成策略201
　　7.2.1 测试激励生成的类型201
　　7.2.2 激励部件的通用算法205
　　7.2.3 在Calc2中应用4种类型的测试激励生成方法206
　　7.2.4 为随机测试用例选取种子219
　　7.2.5 随机环境中的约束求解策略221
　　7.2.6 随机环境中的覆盖率技术224
　　7.2.7 促进“稀有”事件的发生226
　　7.2.8 “死锁”和“活锁”激励的生成228
　　7.3 本章小结231
　　7.4 习题231
　　
　　第8章 基于模拟的验证中的结果检查策略232
　　8.1 结果检查的类型232
　　8.1.1 运行时实时检查与测试用例结束检查233
　　8.1.2 预生成测试用例与实时生成测试用例238
　　8.1.3 在Calc2中应用结果检查策略238
　　8.2 调试247
　　8.2.1 调试过程248
　　8.2.2 不同类型的测试平台对调试的影响258
　　8.3 本章小结259
　　8.4 习题260
　　
　　第9章 广义的功能验证261
　　9.1 系统的复位和启动262
　　9.1.1 复位线初始化262
　　9.1.2 扫描初始化265
　　9.1.3 可测性和内建自测试267
　　9.2 错误和降级模式的处理270
　　9.2.1 错误检测机制的验证271
　　9.2.2 自修复硬件的验证273
　　9.3 对辅助的硬件调试机制进行验证279
　　9.4 低功耗模式的验证282
　　9.4.1 通过关闭功能单元节省功耗283
　　9.4.2 通过周期降级节省功耗284
　　9.5 本章小结285
　　9.6 习题285
　　
　　第10章 重用策略与系统模拟287
　　10.1 重用策略287
　　10.1.1 重用准则289
　　10.1.2 水平重用295
　　10.1.3 垂直重用296
　　10.1.4 在Calc2中应用重用策略297
　　10.1.5 断言重用299
　　10.2 系统模拟302
　　10.2.1 系统测试平台302
　　10.2.2 单元的连接和交互303
　　10.2.3 可重用IP世界的验证挑战306
　　10.3 通用逻辑模拟外的其它方法307
　　10.3.1 加速308
　　10.3.2 硬件仿真313
　　10.3.3 硬件/软件协同验证313
　　10.3.4 协同仿真315
　　10.4 本章小结317
　　10.5 习题318
　　
　　第3部分 形式验证
　　第11章 形式验证简介323
　　11.1 基础知识324
　　11.1.1 设计的正确性及规范324
　　11.1.2 计算复杂性325
　　11.1.3 模拟线性扩展的神话327
　　11.1.4 形式验证中的数学证明方法328
　　11.2 形式化的布尔等价性检查329
　　11.2.1 等价性检查在大规模集成电路设计流程中的作用330
　　11.2.2 等价性检查工具的主要组成元素331
　　11.2.3 时序和组合布尔等价性检查332
　　11.2.4 组合电路等价性检查的核心算法334
　　11.2.5 现代等价性检查工具的蓝图342
　　11.3 功能形式验证——性质检查344
　　11.3.1 性质检查与时序等价性检查345
　　11.3.2 形式化方法完全验证设计的神话346
　　11.3.3 一个设计实例的性质348
　　11.3.4 形式验证中待验证设计的驱动351
　　11.3.5 状态空间遍历和时序逻辑353
　　11.3.6 功能形式验证工具的流程357
　　11.4 本章小结357
　　11.5 习题358
　　
　　第12章 形式验证的使用359
　　12.1 采用硬件描述语言库描述性质规范359
　　12.1.1 开放验证库360
　　12.1.2 采用开放验证库描述性质365
　　12.2 性质描述语言PSL368
　　12.2.1 概述369
　　12.2.2 PSL的布尔层370
　　12.2.3 PSL的时序层372
　　12.2.4 PSL的验证层375
　　12.2.5 PSL的建模层377
　　12.2.6 应用PSL描述性质378
　　12.2.7 高级PSL话题的讨论及注意事项379
　　12.3 使用形式验证进行性质检查384
　　12.3.1 模拟和形式验证之间的性质复用384
　　12.3.2 模型编译385
　　12.3.3 形式功能验证算法386
　　12.3.4 状态空间爆炸问题的解决方法388
　　12.3.5 半形式验证391
　　12.3.6 提供形式和半形式验证工具的EDA供应商392
　　12.4 本章小结392
　　12.5 习题393
　　
　　第4部分 全面的验证
　　第13章 完成验证周期397
　　13.1 回归测试398
　　13.1.1 验证流程中的回归测试398
　　13.1.2 回归测试的质量399
　　13.1.3 回归测试的效率400
　　13.2 问题跟踪403
　　13.3 流片前的准备406
　　13.3.1 度量标准406
　　13.3.2 完成准则410
　　13.4 “逃逸”错误分析412
　　13.4.1 个体错误分析412
　　13.4.2 “逃逸”错误举例418
　　13.4.3 “逃逸”错误分析的趋势422
　　13.5 本章小结423
　　13.6 习题424
　　
　　第14章 高级验证技术425
　　14.1 节省验证周期——引导验证的过程426
　　14.1.1 分离上电复位验证和主线验证426
　　14.1.2 引导待验证设计进入高“潜误”状态427
　　14.1.3 调整待验证设计的配置以激发资源冲突的状态430
　　14.2 高层建模概念430
　　14.2.1 高层模型的应用430
　　14.2.2 高层建模的类型433
　　14.3 覆盖率驱动的测试生成436
　　14.4 本章小结439
　　14.5 习题439
　　
　　第5部分 验证实例研究
　　第15章 验证实例443
　　15.1 一个行删除的“逃逸”错误实例443
　　15.1.1 背景介绍443
　　15.1.2 验证环境444
　　15.1.3 “逃逸”错误445
　　15.2 分支历史表446
　　15.2.1 背景介绍446
　　15.2.2 分支历史表的目标及逻辑设计447
　　15.2.3 分支历史表的验证450
　　15.2.4 结果458
　　15.3 网络处理器458
　　15.3.1 系统简介458
　　15.3.2 验证工作460
　　15.3.3 结果468
　　15.4 本章小结468
　　附录验证术语表471
　　参考文献482