3 Introduction to systemverilog assertions
为了利用形式验证（FV）的力量来证明设计的正确性，首先必须有一种表达您的设计是否正确的方式。最流行的方法是通过property来实现，使用SystemVerilog Assertions（SVA）语言来进行规定。虽然行业和学术界有许多规范方法，比如属性规范语言（PSL）和开放验证库（OVL）断言库，但在过去的十年里，SVA已经有效地成为了指定寄存器传输级（RTL）属性的行业标准。因此，在详细探讨FV技术之前，需要从学习SVA语言开始。
3.1 BASIC ASSERTION CONCEPTS
3.1.1 A SIMPLE ARBITER EXAMPLE
一个arbiter的设计如下：
这是一个有四个请求代理的仲裁器，每个代理都可以使用 req 信号的一个比特位请求一个共享资源。gnt 信号指示当前获得使用资源授权的agent。还有一个 opcode 输入，允许某些命令覆盖仲裁器的正常行为，例如强制特定代理获取优先权，或在一段时间内切断对资源的所有访问。还有一个错误输出，表示已发送错误的 opcode 或非法的 opcode 序列。下面是实现此设计的顶层SystemVerilog（SV）模块的接口代码。
3.1.2 WHAT ARE ASSERTIONS?
在最基本的层面上，断言是关于对设计的陈述，期望它始终为真。对于仲裁器来说，一个简单的例子可能是当没有请求时，不能授权给agent。
check_grant: assert property (!(gnt[0] && !req[0])) else $error(“Grant without request for agent 0!”);
实际上断言可以比上面的简单布尔表达式更复杂，涉及逻辑蕴含和关于值随时间变化的可能性的陈述。
在对模型进行仿真时，当您的仿真器检测到代码中的任何SVA断言不为真时，通常会标志错误。在上面的例子中，如果在仿真中看到 gnt[0] == 1 和 req[0] == 0，将显示消息“agent0没有请求却获得授权！”。
当运行形式属性验证（FPV）工具时，断言被视为证明目标：该工具的目标是数学上证明您的RTL模型永远不会违反该断言。在深入技术细节之前，我们应该了解另外两种属性类型：假设(assumptions)和覆盖点(cover points)。
3.1.3 WHAT ARE ASSUMPTIONS?
assumption与assertion类似，但与指定测试设备的行为不同，它们通常指定用于约束验证环境的条件。通常，这些条件是由输入或其他环境因素导致的外部保证为真的条件。例如，期望的仲裁器只会在其操作码输入处收到合法的非NOP操作码。
在仿真中，与断言一样，假设会被以完全相同的方式处理：仿真器会检查当前仿真值是否违反了指定的条件，如果是，则标记为违反，并在不违反时输出消息。但请记住，概念上的含义仍然有些不同于断言失败：失败的假设通常意味着测试环境、测试平台代码或相邻的设计模块中存在问题，而失败的断言通常表示被测试设计中存在问题。在上面的好操作码例子中，这将表示测试平台错误地将非法的操作码驱动到设计中。
在形式验证（FV）中，假设和断言之间存在一个重要的区别。顾名思义，假设是工具认为是真实的东西。假设被视为公理，并用来证明断言的真实性。没有假设，FV工具会从允许任何可能的值到达它们正在分析的模型的输入开始；假设是用户引导这些值朝着可接受的行为方向的主要方法。在大多数情况下，一个好的假设集是为了消除对不现实行为的考虑并正确证明设计上的断言的要求。
Assumption例子：假设形式化验证一个FIFO，那么FIFO的空满信号必定不能同时为真。如果事务输入不做任何assumption，那么形式验证工具会考虑空、满同时为真的场景，这样会出现虚假的等效失败。
3.1.4 WHAT ARE COVER POINTS?
SVA覆盖点的规定方式与断言和假设相似，但意义上有些不同。虽然断言或假设被期望始终为真，但覆盖点只有在某些情况下才为真：它指定了我们希望确保进行测试的某种有趣条件。例如，在我们的仲裁器中，我们可能希望确保我们正在测试所有代理一次性请求资源的可能具有挑战性的情况：
cover_all_at_once: cover property (req[0]&&req[1]&&req[2]&&req[3]);
在模拟中，大多数用户会集体检查覆盖点：当一个覆盖点被命中时，工具或脚本会将信息保存到数据库中，最后用户可以在运行完测试套件中的所有模拟测试后检查总体覆盖率。通常，希望确保每个覆盖点至少被命中一次；如果没有，这意味着测试中存在潜在的漏洞。
对于性能验证（FV）来说，覆盖点也扮演着重要的角色。虽然FV在理论上覆盖了系统的所有可能行为，但要记住可以指定假设或其他输入要求来限制考虑的可能流量。这导致了过度约束的危险：可能会不小心指定排除系统的有趣流量类别的规定。因此，确保FV环境能够达到所有覆盖点是FV中的关键步骤。
3.1.5 SVA ASSERTION LANGUAGE BASICS
SVA断言语言可以被看作是多层逐渐增加复杂度的结构。
-
布尔表达式(Booleans)是标准的SystemVerilog布尔表达式。一个布尔表达式可以是一个逻辑变量，也可以是像上面的覆盖点示例中的公式:
req [0] && req [1] && req [2] && req [3]
-
序列(sequences)是关于布尔值（或其他序列）随时间发生的语句。它们依赖于明确定义的时钟事件来定义时间的流逝。例如，以下序列表示在两个时钟周期中的请求后紧跟着授权:
req[0] ##2 gnt[0]
-
属性(Properties)使用额外的运算符将序列结合起来，以显示蕴含和类似概念，以表达在设计中预期保持的某些行为。例如，一个属性可能表明，如果我们接收到一个请求，然后两个周期后接收到授权，那么这意味着在下一个周期授权将会取消：
req[0] ##2 gnt[0] |-> ##1 !gnt[0]
-
断言(Assertion)语句是使用 assert、assume 或者 cover 关键字之一的语句，它可以将一个SVA属性作为一个断言、假设或者覆盖点进行检查。除非在某种断言语句中使用，否则属性没有任何效果。例如，导致上述属性被检查的断言语句可以是：
gnt_falls: assert property(req[0] ##2 gnt[0] |-> ##1 !gnt[0]);
还有一个关键概念需要介绍，即时断言和并发断言：
-
Immediate assertion：即时断言语句是简单的断言语句，每当在过程代码中访问时都会进行检查。它们只允许布尔参数，没有时钟或复位机制，并且不支持许多高级属性运算符。因此，它们无法检查需要对时间流逝有意识的条件。在 SVA 中，即时断言通过不带关键字 property 的断言来指示，如下所示.
imm1: assert (!(gnt[0] && !req[0]))
-
Concurrent assertion: 并发断言语句始终相对于一个或多个时钟进行评估，并且可以描述跨越时间的行为，并且允许许多支持关于时间间隔的逻辑蕴含的高级陈述运算符。因此，它们比即时断言语句更加通用。在 SVA 中，通过在断言中包含关键字 property 来指示并发断言，如下所示.
conc1: assert property (!(gnt[0] && !req[0]))
虽然并发断言 conc1 看起来与即时断言 imm1 相似，但它们的评估方式有一些重要的区别。即时断言在过程代码中被访问时会进行评估，而并发断言只在明确定义的时钟边沿处进行评估。
原创 Junxiao Zhang 芯片验证笔记
