第1章 设计验证的缘由 1
1.1什么是设计验证 1
1.2验证的基本原理 2
1.3验证方法学 5
1.4基于模拟的验证与形式验证的比较 9
1.5形式验证的局限性 10
1.6 Verilog语言调度和执行语义简介 11
1.7本章小结 14
第2章 编写验证的代码 15
2.1功能正确性 16
2.2时序正确性 24
2.3模拟的性能 28
2.4可移植性与可维护性 34
2.5可综合性、可调试性与通用工具兼容性 37
2.6基于周期的模拟 39
2.7硬件模拟/仿真 41
2.8 2状态与4状态模拟 43
2.9 linter程序的设计与使用 44
2.10本章小结 44
2.11习题 45
第3章 模拟器体系结构与操作 48
3.1编译器 48
3.2模拟器 52
3.3模拟器的分类与比较 72
3.4模拟器的操作与应用 75
3.5增量式编译 83
3.6模拟器控制台 84
3.7本章小结 85
3.8习题 85
第4章 测试基准组成与设计 90
4.1测试基准的分类与测试环境 90
4.2初始化机制 93
4.3时钟生成与同步 97
4.4激励生成 103
4.5响应评估 108
4.6验证实用程序 123
4.7测试基准至系统设计接口 131
4.8常见的实际技术与方法 132
4.9本章小结 138
4.10习题 138
第5章 测试构想、断言与覆盖 142
5.1分层验证 143
5.2测试规划 145
5.3伪随机测试生成程序 152
5.4断言 155
5.5 SystemVerilog断言 167
5.6验证覆盖 174
5.7本章小结 187
5.8习题 188
第6章 调试进程与验证周期 193
6.1故障捕获、范围压缩与错误跟踪 193
6.2模拟数据转储 199
6.3潜在故障原因的隔离 202
6.4系统设计更新与维护：修改控制 213
6.5回归、发布机制与流片标准 215
6.6本章小结 216
6.7习题 217
第7章 形式验证初步 224
7.1集合与运算 224
7.2关系、划分、偏序集与格 225
7.3布尔函数与表示 231
7.4布尔函数运算符 238
7.5有限状态自动机与语言 241
7.6本章小结 255
7.7习题 256
第8章 判定图、等价检验与符号模拟 259
8.1二叉判定图 260
8.2判定图的变异 274
8.3基于判定图的等价检验 283
8.4布尔可满足性 287
8.5符号模拟 295
8.6本章小结 304
8.7习题 305
第9章 模型检验与符号计算 309
9.1性质、规范与逻辑 309
9.2性质检验 321
9.3符号计算与模型检验 328
9.4符号CTL模型检验 340
9.5计算改进 346
9.6模型检验工具的使用 350
9.7本章小结 351
9.8习题 351
参考文献 355
缩写词汇表 376