第0章 基于断言的验证 1
第1章 SVA介绍 5
1.1 什么是断言 5
1.2 为什么使用SystemVerilog断言（SVA） 6
1.3 SystemVerilog的调度 8
1.4 SVA术语 9
1.4.1 并发断言 9
1.4.2 即时断言 10
1.5 建立SVA块 11
1.6 一个简单的序列 12
1.7 边沿定义的序列 13
1.8 逻辑关系的序列 15
1.9 序列表达式 15
1.10 时序关系的序列 16
1.11 SVA中的时钟定义 18
1.12 禁止属性 19
1.13 一个简单的执行块 21
1.14 蕴含操作符 21
1.14.1 交叠蕴含 22
1.14.2 非交叠蕴含 23
1.14.3 后续算子带固定延迟的蕴含 24
1.14.4 使用序列作为先行算子的蕴含 25
1.15 SVA检验器的时序窗口 27
1.15.1 重叠的时序窗口 29
1.15.2 无限的时序窗口 30
1.16 “ended”结构 32
1.17 使用参数的SVA检验器 35
1.18 使用选择运算符的SVA检验器 36
1.19 使用true表达式的SVA检验器 38
1.20 “＄past”构造 39
1.21 重复运算符 42
1.21.1 连续重复运算符［＊］ 43
1.21.2 用于序列的连续重复运算符［＊］ 44
1.21.3 用于带延迟窗口的序列的连续重复运算符［＊］ 46
1.21.4 连续运算符［＊］和可能性运算符 47
1.21.5 跟随重复运算符［-＞］ 48
1.21.6 非连续重复运算符［＝］ 50
1.22 “and”构造 51
1.23 “intersect”构造 54
1.24 “or”构造 56
1.25 “first_match”构造 58
1.26 “throughout”构造 60
1.27 “within”构造 61
1.28 内建的系统函数 63
1.29 “disable iff”构造 65
1.30 使用“intersect”控制序列的长度 66
1.31 在属性中使用形参 68
1.32 嵌套的蕴含 70
1.33 在蕴含中使用if/else 71
1.34 SVA中的多时钟定义 73
1.35 “matched”构造 75
1.36 “expect”构造 76
1.37 使用局部变量的SVA 77
1.38 在序列匹配时调用子程序 79
1.39 将SVA与设计连接 81
1.40 SVA与功能覆盖 83
第2章 SVA模拟方法论 85
2.1 一个被验证的实例系统 85
2.1.1 主控设备 86
2.1.2 中间设备 88
2.1.3 目标设备 90
2.2 块级验证 91
2.2.2 仲裁器的验证 92
2.2.1 SVA在设计块中的应用 92
2.2.3 模拟中针对仲裁器的SVA检验 94
2.2.4 主控设备的验证 96
2.2.5 模拟中针对主控设备的SVA检验 98
2.2.6 胶合（Glue）的验证 100
2.2.7 模拟中针对胶合逻辑（glue logic）的SVA检验 102
2.2.8 目标设备的验证 104
2.2.9 模拟中针对目标设备的SVA检验 106
2.3 系统级验证 108
2.4 功能覆盖 114
2.4.1 实例系统的覆盖率计划 115
2.4.2 功能覆盖小结 124
2.5 用于创建事务日志的SVA 124
2.6 用于FPGA原型测试的SVA 127
2.7 SVA模拟方法的小结 131
第3章 SVA在有限状态机中的应用 133
3.1 设计例子——FSM1 134
3.1.1 FSM1的功能描述 134
3.1.2 FSM1的SVA检验器 139
3.2 设计实例——FSM2 143
3.2.1 FSM2的功能描述 144
3.2.2 FSM2的SVA检验器 148
3.2.3 有时序窗口协议的FSM2 155
3.3 在FSM中应用SVA的小结 159
第4章 SVA用于数据集约型（DATA iNTENSIVE）的设计 161
4.1 简单乘法器的检验 161
4.2 设计实例——算术单元 163
4.2.1 WHT算术 163
4.2.2 WHT硬件的实现 164
4.2.3 WHT模块的SVA检验器 165
4.3 设计实例——JPEG的数据通路设计 168
4.3.1 三模块的深入探讨 169
4.3.2 用于JPEG设计的SVA检验器 172
4.3.3 JPEG模型的数据检验 176
4.4 数据集约型设计的小结 182
第5章 SVA储存器 183
5.1 存储控制系统实例 183
5.1.1 CPU-AHB接口操作 183
5.1.2 存储控制器的操作 186
5.2 SDRAM的验证 189
5.3 SRAM/FLASH的验证 208
5.4 DDR-SDRAM的验证 215
5.5 存储器SVA的小结 217
第6章 SVA协议接口 219
6.1 PCI简介 220
6.1.1 一个PCI读出事务的实例 222
6.1.2 PCI写入事务实例 223
6.2 PCI系统实例 224
6.3 情形1——主控DUT设备 225
6.4 情形2——目标DUT设备 243
6.5 情形3——系统级断言 259
6.6 用于标准协议的SVA小结 263
第7章 对检验器的检验 265
7.1 断言验证 266
7.2 双信号SVA Assertion Test 268
7.2.1 双信号的逻辑关系 268
7.2.2 电平敏感逻辑关系激励的产生 269
7.2.3 边沿敏感逻辑关系激励的产生 272
7.2.4 双信号的时序关系 275
7.2.5 时序关系激励的产生 276
7.2.6 双信号的重复关系 286
7.2.7 双信号ATB环境 290
7.3 一个PCI检验器的ATB实例 301
7.4 检验器检验小结 305