SVA简介

Systemverilog assertion(SVA)是systemverilog的一个子集，也叫断言。它是设计的属性的描述，主要用于验证设计的行为。

SVA主要包括立即断言（Immediate asseration）与并发断言（Concurrent asseration）。举例子如下：

并发断言：

并发断言基于时钟周期进行，可以放置于procedural block、module、interface及program中。在静态(形式）验证及动态仿真工具中均可以应用。

a_cc将在每个时钟上升沿进行断言检测，若a和b同时为高，则断言失败。

立即断言：

立即断言基于事件，必须放置在程序块中，只能用于动态仿真，没有时间的概念。立即断言与并发断言关键字区分在于“property”。简单的立即断言示例如下：

像Verilog的连续赋值块，当a或b变化时，a_ia会执行，当a和b都为高时断言成功，否则断言失败。我们在实际应用中，主要是用并发断言，立即断言用的不多。

SVA有三种形式的断言: assert 、assume、cover。注意这里不要和上面的立即断言和并发断言混淆了，这里说的三种形式主要是针对并发断言来的。

由于立即断言使用不多，因此我们下面介绍断言语法和结构主要是针对并发断言来描述的。

SVA断言结构主要由如下四个部分组成。

布尔表达式是构成SVA的最基本单元。其一般形式为标准的SystemVerilog的布尔表达式，它由信号及其逻辑关系运算符构成，用以表示某个逻辑事件的发生。

序列（sequence）的基本语法是：

sequence具有以下特性：

SVA也允许在属性property中使用if/else结构：

属性中可以使用形式参数以属性重用。SVA也允许时钟作为参数，延时时间也可以使用形式参数使得属性更加通用。

SVA提供禁止使能检测使能用于在某些情况下关断检测匹配，其原语为：

disable iff只能用于property中，条件为真时将不执行检测。

p34将在reset为高时关断检测。

throughout操作符用于保证某些条件在整个序列的验证过程中一直为真。

在整个sequence definition验证器件，expression表达式必须一直保持为真。即使验证序列匹配成功但表达式不为真，也会导致整个验证序列的验证失败。

p31要求在序列检查期间，start信号必须保持为低电平。

针对带有时序窗口的序列，同意起始点可能有多个匹配到的序列，fisrt_match用于确保只用第一次匹配成功的序列而丢弃其他匹配的序列，用于针对同一个校验具有多个匹配的情况。

对于p30来讲，对于每个起始点都有5中可能匹配的序列，first_match在得到一个成功匹配的点后，其他情况将不会再考虑匹配。

逻辑操作符or当序列中的其中一个验证成功后即匹配成功。

逻辑操作符and用于组合两个序列，当所有的序列都成功匹配后才通过检测。所有的序列在同一时间开始但可以在不同时间结束。

SVA允许使用选择运算符?:。如下例所示：

p17在上升沿检测c点评，为高时判定d是否等于a，为低时判定d是否等于b。

属性property也可以被定义为不希望发生，即若property中序列发生，则断言失败，可以使用关键词not进行声明。

上例中若在某时钟沿a为高点平，且两个时钟后b为高电平则断言失败，否则断言成功。

非交叠蕴含操作符符号为|=>。

非交叠蕴含操作符在先验部分验证匹配后，在下个时钟沿才进行后验部分的检查匹配。相对于蕴含操作符后验部分有一个时钟的滞后。如下例所示，在时钟边沿a为高电平则一个时钟后b也应为高电平。

交叠蕴含操作符符号为 |->。

交叠蕴含操作符中，若先验部分验证成功，则后验结果在同一时钟进行验证。如下例所示,若某时钟处a变为高电平，则同一时刻b也应为高电平。

原语：signal or sequence [*n] n-重复的次数

持续性重复允许指定事件或序列持续性匹配指定周期数，重复周期之间默认有一时钟周期的间隔。

(a##1b)[*3]等价于 a##1b##1a##1b##1a##1b

示例1. 信号的重复

start上升沿两个时钟周期后，a持续为高3个时钟周期，再经过两个时钟周期后，stop拉高1个时钟周期。

示例2. 带有延迟窗的重复

示例3. 带有不确定性的持续性重复

持续性重复可以指定秩序性重复的最小和最大次数，信号持续性重复次数在这个范围内都匹配正确。其重复次数上限可以设为$表示无穷。

a[*1:5]等价于：

不要求信号持续重复，可以是间断性的，但要求最后一次匹配必须在序列匹配的最后一个时钟周期。

要求a重复三次且必须最后一次出现紧接着stop信号。

示例：

p25要求a最后一次出现必须紧接着stop信号。

非持续性重复操作不要求信号连续重复，也不要求信号最后一次匹配必须在序列的最后一个时钟周期。

p26中序列要求检测到start上升沿后两个时钟周期后，a应重复2次，但不要求持续重复，随后再过一个时钟周期，stop拉高一个时钟周期。注意，start上升沿后两个时钟周期后不要求a立即为高，只需要确保再start上升沿于stop拉高之间有三个a高电平即可，跟随重复操作类似。

以下内建函数，都是对表达式进行操作，不能对序列进行操作。

$rose()函数就是我们常说的上升沿检测，匹配规则是信号的当拍值为1上拍数据为0。

$fell()函数和$rose函数刚好相反，是检测下降沿的。

$fell()函数和$rose函数的结合体，当拍采样值与上一拍不一致则匹配成功

$stable和$change刚好相反，信号当拍采样值与上一拍一样则匹配成功。

$past(exp1, num_ticks, exp2, clk)，这个函数比较复杂一般要跟之后的蕴含算子一起使用(事实上之前讲的东西之后基本上都要和蕴含算子配合使用)，这个函数的含义是：以clk为采样时钟，从当前时刻往前看，第num_ticks次exp2成立时exp的值，$past返回的是一个信号值。

任意时钟沿，表达式a都只有1bit为高；

任意时钟沿，表达式a都只有1bit为高或这均为低电平；

任意时钟沿，表达式a任意位是否有X态或者Z态，如果有则匹配，没有X态或Z态则报错；注意这个函数我们一般时~$isunkown(a)这样使用，在有X态或Z态时候我们希望报错出来；

返回表达式中高电平的bit数量。

在实际应用中，如果我们把SVA断言放到interface中，那么在EDA环境中，只要环境中例化了这个interface，那么SVA断言自然就绑定上interface的信号上了。

如果我们把SVA放到RTL文件中，也不用特别的绑定，如下所示：

如果我们把SVA独立放到一个module里面，那么我们需要用bind语法进行绑定。具体语法如下：

bind rtl实例名 断言模块名 断言实例名(signal1,signal2...);

具体bind语法可以参考网上的资料。