SystemVerilog断言手册 原书第四版 pdf下载

本书源于作者多年的实践经验、培训、与各论坛用户的交流互动，以及对设计流程、验证方法、语言演进的研究，是SVA流程和应用方面的权威参考。无论您是硬件设计师、验证工程师、软件与系统集成工程师，还是高等院校微电子、自动化、电子信息等相关专业的师生，本书都是您系统学习SystemVerilog断言设计的理想之选。

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

目录
第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

第1章验证方法中的断言
　　功能验证是典型设计周期中的主要瓶颈之一。为了解决这个问题，SystemVerilog得到了显著的增强，以支持断言和构建验证框架（如VMM、OVM和UVM等）所需的语言结构。IEEE1800-2017标准是SystemVerilog统一硬件设计、规范和验证语言的标准，而在IEEE1800-2023标准中，重点是保持SVA的稳定性，并对语言中的一些细节内容进行澄清，其中并没有引人新的功能。为此，我们可能会产生如下疑问：
　　？使用SystemVerilog断言（SVA）是一种好的验证方法吗？
　　？断言可以用于诸如VMM、OVM和UVM等验证架构中吗？
　　？在功能验证中，应给予SVA多大的重视？
　　？为什么要用两种不同的方式（如SystemVerilog和断言）描述同一件事？
　　？SVA能否以透明的方式集成到RTL设计中？
　　本章的重点就是解答以上这些问题。这里我们假设读者具有一定的SystemVerilog和RTL设计基础。本章将会对断言做一个简要的介绍，并对其中一些基本概念进行解释，以方便后续学习。其他章节将主要讨论语言应用的更多细节，同时提供更多的指南和示例。
　　1.1设计验证方法学
　　方法学被定义为“某一学科或从事研究工作的人所使用的一系列实践、程序和规则”。SVA语言是SystemVerilog不可或缺的一部分，支持基于断言的验证（ABV）方法，SVA的开发旨在向系统工程师、设计工程师和验证工程师提供一种方法，以一种清晰而简洁的方式描述有关设计需求和属性的复杂时序（即跨越多个时钟周期）行为。
　　为什么说断言很重要呢？从图1.1中可以看出，绝大多数的设计功能缺陷是对于设计需求的错误理解和设计错误导致的，断言有助于澄清这些需求并检测设计中的错误。
　　SVA也支持功能覆盖率，从而可以确定某些属性或者事件序列是否随着时间推移发生了，进而也为测试用例的效率提供了衡量标准。由于断言在语法上与SystemVerilog统一，用户可以将断言定义在巳经定义的设计单兀（如module和checker）中，然后再将设计单元绑定到对应的待测设计（DUT）或者SV接口，或者直接将断言嵌人RTL设计和其他验证代码（如测试平台模块）中。这些方法允许工具可以从上下文代码中推断出大量所需的信息。例如，工具可以检测RTL代码的实际行为与预期行为之间的不匹配，这些预期行为由断言和形式化验证中使用的约束指定。
　　SVA的另一个有用的特性是它与测试平台的交互性，通过向测试平台传递有关错误、序列结束点、满足时序条件的事件和覆盖率等信息，将断言与设计和验证语言统一了起来n。基于断言的验证正在改变传统设计流程，因为这种方法有助于形式化的描述设计意图和期望的操作。基于断言的验证还指导了验证的任务，加快了验证速度，这是因为断言在白盒级别提供了反馈，并且简化了测试平台的设计，将更多“验证”的任务转移到了断言上，而不是用户自定义的记分板和状态机（FSM）模型上。SVA使验证环境具有反应，也就是说基于断言的结果（成功或者失败），可以产生不同的操作。另外，使用SVA的形式化验证在不需要仿真的情况下又增加了另一个级别的验证。SVA也可以用于硬件加速器，因为它们可以作为RTL设计的一部分被综合，并且被划分到对应的仿真硬件中。在仿真过程中，如果设计有逻辑错误，那么综合后的断言将会触发停止/跟踪寄存器，以停止仿真并直接指向产生失败的原因。断言也可以在硅片中被综合，并在验证过程中通过JTAG边界扫描记录和标记功能错误。
　　1.2项目使用哪种语言/方法？
　　在决定设计/验证语言时，有几个因素需要考虑，因为它们将决定*终选择使用的方法和工具。
　　1.设计类型：控制密集型或处理密集型
　　带有FSM的控制密集型设计*好使用SystemVerilog或VHDL之类的语言实现。处理密集型设计（如滤波类设计或图像处理器等）*好使用C/C++进行设计和验证。使用C/C++的流程短期内不会取代Verilog/SV，因为目前某些IP的连接仍*适合使用RTL完成。尽管如此，一些供应商的IP巳经开始采用C++开发，并且使用高层次综合（HLS）的方式转换为Verilog和VHDL模型（以及SystemC）。经历过这种流程的工程师发现，使用行为级C/C++进行仿真的速度比使用SV快14000倍，开发周期也缩短了。目前第三方IP仍主要采用RTL进行开发，并且RTL将会与新出现的更快方法并存很长时间。
　　2.工程师的知识基础和管理的灵活性
　　如果设计团队只对VHDL比较熟悉，然后要切换到基于SystemVerilog的UVM上，那么这样的设计成本反倒会更高，这主要是因为此时需要进行培训、学习*线适应以及工具的购买（如果没有可用的工具）等。*终选择哪种语言，取决于项目进度安排和管理层对采用SystemVerilog的灵活度考量。
　　3.验证方法学
　　验证风格也将决定支持该风格的*佳语言。UVM或者类似于基于事务级和覆盖率的随机约束测试，*好使用SystemVerilog来处理。另外，基于断言的仿真验证和形式化验证可以使用像SVA或者PSL这样的语言，这些语言巳集成在VHDL和SystemVerilog中。
　　根据我（本？科恩）的经验，现在可以很自信地归纳以下几点：
　　（1）SystemVerilog是一种成熟且广受认可的语言，自2001年作为Verilog的扩展引人以来得到了广泛的应用。SystemVerilog在设计和验证方面比VHDL功能更强大，并且提供的资源更丰富。除了提供像关联数组、队列、类等这样的高级结构之外，SystemVerilog还实现了随机的可再现性，从而保证了随机的稳定性。这里需要注意，VHDL在这个方向上也取得了一定的进展。VHDL标准IEEE1076-2008[4]于2009年1月发布。开源VHDL验证方法TM（OSVVMtm）是VHDL对SystemVerilog的UVM的回应2）。
　　（2）对于控制密集型设计，使用SystemVerilog更好。
　　（3）编写断言对细化和阐明规范、定义RTL特定需求和接口需求非常重要。SVA比PSL更受欢迎，因为它更强大，并且可以得到IEEE1800标准和工具供应商的更好支持。
　　（4）如果在项目中可以使用形式化验证，那么将会为数字设计的验证过程提供许多好处（参见第7章）。
　　（5）UVM或类似UVM的验证方法，结合了随机约束测试、覆盖率和断言等特性，是一种高效的验证方法，可以定义测试向量，验证这些向量并检测错误。
　　（6）对于软件集成或处理密集型设计，许多人选择了C/C++路线，也取得了巨大的成功。
　　1.2.1什么是属性？什么是断言？
　　使用断言的概念并不新鲜。多年来，验证模块使用FSM和记分板等代码来验证设计的功能，这些代码（通常在监视器中实例化）只不过是标记和识别DUT中功能错误的断言。SVA是一种专门的语言和符号，极大地促进了这些断言的定义，从而消除了构建复杂的FSM和特定的类似RTL代码的需要，其简洁性也使得断言的编写和审查速度更快，从而阐明和验证设计要求及其实现。SVA包括了四层定义（详见附录B以获取更深人的定义）：
　　（1）布尔表达式：一种逻辑的组合表达式，该表达式在某一时刻评估为真或为假。例如：
　　（2）序列：一个按时钟周期线性顺序排列的布尔表达式的有限列表。在列表中，一个复杂的序列可能有并行的分支，所有的分支在指定的周期同时开始。一般情况下，序列会按照一定格式描述的表达式在一定的时间点去匹配布尔表达式。例如：
　　@（posedge clk）req##1 ack##1 write//##1表示1个时钟周期
　　（3）属性：逻辑关系和时序关系的集合，在这些从属关系（如序列、布尔表达式和其他一些属性）之间包含一些特殊的操作符。属性也可以用来描述覆盖率目标或关于设计环境的假设，甚至可以临时将分析重点限制在一组特定的场景上。属性可以声明在property中，因此，允许这些属性实例化和重用。属性也可以在断言语句中内嵌定义，这些断言将会强制工具执行。例如，根据声明的断言验证DUT：
　　$rose（req）|=>ack##1 wr;//如果有新的req，则在下一个周期检查ack是否有
　　效，然后在下一个周期检查wr是否为高
　　（4）指令：将属性实例化，并且定义如果属性成功或者失败应该采取的操作。属性本身并不会被工具执行去验证或者覆盖设计要求（如仿真或者形式化
　　验证）。为了检查设计行为的正确性、功能覆盖率、设计属性、关于设计性能的一些假设等，SystemVerilog提供了以下断言语句（也称为指令）：assert、assertproperty、cover、coverproperty、coversequence、assume、assumeproperty。
　　？断言：“断言”的定义通常取决于其上下文。在一般性讨论或者表述时，它通常指的是构成SVA的assert、assume和cover等这类语法结构；而在比较详细的文档中，它仅指特定的assert命令。assert是一种语句，要求给定属性在每次尝试时都成立。它也可以作为验证工具的一种语句，用于验证待测设计所关心的属性是否成立。需要注意的是，可以使用property声明来命名属性，然后可以使用命名的属性构建断言。断言可以定义标签，这样有助于工具进行断言追踪。立即断言需要使用assert命令，但不依赖于时钟事件；而并发断言则依赖于时钟事件，并且需要使用assertproperty语句。例如：
　　ap_req_ack_wr:assert property（@（posedge clk）$rose（req）|=>ack ##1 wr）;
　　在每个时钟事件（posedgeclk）发生时，如果req有一个从0到1的变化，然后在下一个周期，变量ack为1，紧接着的下一个周期变量wr为真，则断言真成功。
　　？假设：带有假设的约束通常用在输人信号上，从而可以约束需要考虑的行为集。假设通常用于形式化验证，但是对于文档和仿真也很有用处，例如，当有约束违例发生时，也会标记出来。约束可以表示实际的需求，例如，复位需要多少个时钟周期和输人的合法数值等。形式化验证工具可以使用约束来限制搜索空间。随机激励产生器可以使用约束产生更加智能的随机向量。在第7章中，我们将讨论形式化验证并详细阐述约束的相关内容。假设使用关键字assume或者assumepropery语句声明。下面是一个关于约束的示例：
　　//当ready为假时，request永远不会发生m pRequestReady:assumeproperty（@（posedge clk）not（request && ! ready））;
　　？限制：restrict用于限制测试场景以收敛形式验证的证明过程。而assume则用于定义合法的输人状态。restrict的使用可以提高分析的性能，并且通常是实现验证完备性所必须的。
　　？功能覆盖：功能覆盖是一种确保序列或属性至少发生一次的技术，因此它是对发生的属性与需求的检查。它使用关键字cover、cover sequence或者cover property语句实现，这与assert或assert property语句不同