SYSTEMVERILOG 断言手册（原书第四版修订版）

本书聚焦RTL层面对ASIC和FPGA的建模与验证，旨在通过系统化的理论讲解、丰富的工程实例与工具验证案例，帮助读者掌握基于断言的验证方法，解决传统验证中需求模糊、设计意图难监控、验证完整性难衡量等核心痛点。
　　本书由SystemVerilog领域权威专家编写，先通过大量示例展示基础概念，然后专注于序列和属性的细节，接着通过更多示例探讨高级主题，随后讨论了在设计和验证周期的各个阶段（包括需求、设计和验证阶段）使用断言的过程，通过两个完整模型展示了形式化验证的应用，最后增加了SVA方面的论文，同时回答了用户在论坛中提出的问题。书中所呈现的编码和使用指南源自作者多年的设计与验证工作经验，以及对硬件描述语言、断言语言和框架库的使用与教学经验。

目录
第1章 验证方法中的断言 1
1.1 设计验证方法学 2
1.2 项目使用哪种语言/方法？ 3
1.3 为什么选择SVA？ 8
1.4 属性、断言和尝试的概述 12
1.5 基于断言的验证 21
第2章 理解序列 25
2.1 序列语法 26
2.2 序列操作符和内置函数 28
2.3 重复操作符 31
2.4 序列组合操作符 45
2.5 序列支持的方法 55
2.6 序列和属性中可用的形参类型 66
2.7 形参、序列和属性声明中的局部变量 76
第3章 理解属性 99
3.1 断言、属性、术语与语法 100
3.2 属性开头声明 105
3.3 属性标识符 106
3.4 形参及其用法 106
3.5 属性变量声明 109
3.6 属性语句的主体 109
3.7 时钟事件 109
3.8 禁用条件 113
3.9 属性表达式和操作符 118
3.10 应用场景 128
3.1 1 属性中的局部变量 150
练习题（答案参见附录A） 157
第4章 属性和序列高级主题 161
4.1 断言在SystemVerilog中的调度 162
4.2 基于断言的系统函数 164
4.3 时钟序列、属性和多时钟 186
4.4 接口中的属性 198
4.5 断言语句 199
4.6 立即断言 213
4.7 断言绑定至作用域或实例 219
4.8 静态/自动变量和断言 223
第5章 检查器 231
5.1 checker的优势 232
5.2 checker结构的语法 234
5.3 checker内容 235
5.4 检查器使用的模型 238
5.5 上下文推断 249
5.6 检查器变量 250
第6章 设计流程中的SVA 257
6.1 传统设计流程 258
6.2 采用SVA的设计流程 258
6.3 需求 260
6.4 架构规划 263
6.5 验证和测试计划 263
6.6 RTL设计 264
6.7 测试平台设计 264
6.8 功能覆盖率在验证中的重要性 265
6.9 案例研究——同步FIFO 269
6.10 仿真 285
第7章 基于断言的形式化验证 287
7.1 形式化属性验证 288
7.2 全局时钟块以及过去和将来采样值函数 290
7.3 案例研究——信号灯控制器的FV 299
第8章 SVA规范指南 309
8.1 命名规范指南 310
8.2 风格 314
8.3 模型使用指南 324
8.4 方法学指南 334
8.5 SVA与UVM的结合 341
第9章 断言验证 343
9.1 驱动端口 346
9.2 激励向量 351
9.3 测试平台构建方法 360
9.4 测试模块中简单的不受约束的随机测试向量 362
第10章 断言字典 373
10.1 在en信号上升跳变时总线递增 374
10.2 若COND1成立，则必须满足COND2 376
10.3 若COND1成立，则当下次COND2发生时必须满足COND3 376
10.4 若COND1成立，则在第N次COND2后必须满足COND3 377
10.5 若满足COND1且首次满足COND2，则保持COND3直至出现COND4为止 378
10.6 若满足COND1且首次满足COND2，则触发序列 379
10.7 在COND1和COND2之间，信号1必须保持有效 380
10.8 若COND1成立后出现1次COND2，则触发序列 381
10.9 若COND1成立，则在COND3成立前出现N次COND2（N为变量值） 382
10.10 若COND1成立，且在N个周期内出现y次COND2，则触发COND3 383
10.11 若COND1成立，则COND2必须保持直到COND3成立 384
10.12 若COND1成立，则COND2必须在COND3之前发生 385
10.13 若COND1后跟随COND2，且在COND2持续期间64个周期内未收到COND3，则触发错误（COND5）；如果64个周期内收到COND3，则触发COND4 386
10.14 若COND1发生，则COND2应在N个周期内完成，除非COND3 发生 387
10.15 内存数据完整性：从内存读取的数据应与最后一次写入的数据相同 389
10.16 队列的数据完整性：接口写入的数据必须正确传输至接收硬件 391
10.17 禁止对同一地址连续写入两次 393
10.18 连续两次写入地址0后，下一周期ready必须为1 394
10.19 假设复位信号在初始N个周期内保持低电平 395
10.20 若序列启动但未完成，则状态寄存器必须报错 396
10.21 PROPERTY1与PROPERTY2互斥性验证 397
10.22 禁止未读前重复写入同一地址 400
10.23 SignalA[odd_bits] |=> SignalB[odd_bits]，SignalA[even_bits] |=> SignalB[even_bits] 400
10.24 在断言中使用类变量 401
10.25 如何覆盖四值变量（0,1,X,Z） 401
10.26 线程唯一性问题——FIFO 案例 402
10.27 先行算子为真时排他性后续算子检查 405
10.28 建立时间和保持时间检查 406
10.29 时间检查 407
10.30 在两个脉冲之间，信号a必须为真（无固定时钟） 408
10.31 信号a在信号b出现10个高电平周期期间保持高电平 408
10.32 并行转串行 408
10.33 一个信号在另一个信号的两个非连续下降沿之后保持稳定 409
10.34 测量时钟周期 410
10.35 断言的顺序触发 411
10.36 用于跨时钟域数据路径的断言 412
10.37 总线序列 412
10.38 在时钟边沿（上升沿或下降沿）发生前禁用断言 413
10.39 这个属性有什么问题？ 413
10.40 信号在两个事件之间持续保持高电平至少N 个周期 414
附录 417
附录A 第3章练习题答案 418
附录B 专业术语 424
附录C 系统任务和系统函数（IEEE 2012第20章） 435
补充内容 439
补充内容1：使用Fork-join 模型理解SVA引擎 440
补充内容2：用户使用SVA的经验反思（第1部分） 454
补充内容3：用户使用SVA的经验反思（第2部分） 459
补充内容4：理解时间步内的断言处理 464
补充内容5：理解和使用立即断言 470
补充内容6：SVA包——动态的范围延迟和重复 474
补充内容7：辅助逻辑与always属性 480
补充内容8：基于UVM类环境的SVA 485
补充内容9： 使用断言代替FSM/逻辑实现记分板并进行验证 492
补充内容10：理解多时钟、triggered和matched 499
补充内容11：用户问答 510
补充内容12：SVA退化现象 528
补充内容13：intersect与throughout、until、until_with、within的区别与联系536