毛主席说过：没有调查就没有发言权。

《SVA介绍——学习SVA语法》系列第二讲

本文还是延续上一篇的风格，语言内容尽可能简单明了，有问题大家相互讨论，共同进步。需要电子书的朋友可以给我发邮件。tommi.wei@qq.com

1.16 "ended"结构

到 目 前 为 止 ， 定 义 的 序 列 都 只 是 用 了 简 单 的 连 接(concatenation)的机制。换句话说，就是将多个序列以序列的起始点作为同步点，来组合成时间上连续的检查。 SVA 还提供了另一
种使用序列的结束点作为同步点的连接机制。这种机制通过给序列名字追加上关键词“ended”来表示。例如， s.ended 表示序列的结束点。关键词“ ended”保存了一个布尔值，值的真假取决于序
列是否在特定的时钟边沿匹配检验。这个 s.ended 的布尔值只有在相同时钟周期有效。

序列 s15a 和 s15b 是两个需要多个时钟周期来完成的简单序列，属性 p15a 检查序列 s15a 和序列 s15b 满足两者间隔一个时钟周期的延迟分别匹配检验。属性 p15b 检查相同的协议，但是使用了关键词“ ended”。在这种情况下，两个序列在结束点同步。由于使用了结束点，两个序列间加上了两个时钟周期的延迟，来保证断言检验的协议与 p15a 相同。
 

图 1-18 显示了属性 p15a 和 p15b 在模拟中的响应。 表 1-10 总结了断言 a15a 和 a15b 的状态。断言 a15a 的第一个真正的成功发生在时钟周期 2。当信号“ a”被检测为高，检验在时钟周期 2 被
激活。当信号“ d” 在时钟周期 5 检测为高时， 检验完成。 断言 a15b的第一次真正成功出现在在时钟周期 3。 在时钟周期 3， 当序列 s15a成功，即信号“ b”被检测为高时检验被激活。接着在时钟周期 5当序列 s15b 成功，或者说信号“ d”被检测为高时，检验完成。
 

 断言 a15a 的第一次失败发生在时钟周期 5。当信号“ a”在给定的时钟上升沿为高，且一个时钟周期以后(时钟周期 6)信号“ b”紧接着为高时，检测到一个有效的起始点。这样就会检查后续算子，因为信号“ c”在下一个时钟周期不为高，检验失败于时钟周期 7。
相应地，断言 a15b 的第一个失败出现在时钟周期 6。当序列s15a 在时钟周期 6 成功结束时，检测到一个有效的起始点。接着检验后续算子在时钟周期 8 是否得到一个有效的结束点。因为信
号“ c”在时钟周期 7 不像期望的那样为高，序列的结束点的值为假，导致检验在时钟周期 8 为假。

 1.17 使用参数的 SVA 检验器

SVA 允许像 Verilog 那样在检验器中使用参数(parameter)。这为创建可重用的属性提供了很大的灵活性。比如，两个信号间的延迟信息可以在检验器中用参数表示，那么这种检验器就可以在设计只有时序关系不同的情况中重用。 例子 1.2 显示了一个带延迟默认值参数的检验器。如果这个检验器在设计中被调用，它使用一个时钟周期作为延迟默认值。如果在实例化时重设检验器中延迟参数值，那么同一个检验器就可以被重用。在例子 1.2 中，模块“ top”有两个“ generic_chk”的实例。实例i1 将延迟参数改写为 2 个时钟周期，而实例 i2 使用默认的 1 个时钟周期。

例 1.2 使用参数的 SVA 检验器的例子

1.18 使用选择运算符的SVA检查器

SVA 允许在序列和属性中使用逻辑运算符。属性 p17 检查如果信号“ c”为高，那么信号“ d”的值与信号“ a”的相等。如果信号“ c”不为高，那么信号“ d”的值与信号“ b”的相等。这是一个组合的检验，在每个时钟上升沿被执行。
 

1.19 使用 true 表达式的 SVA 检验器

使用 true 表达式，可以在时间上延长 SVA 检验器。这代表一种忽略的状态，它使得序列延长了一个时钟周期。这可以用来实现同时监视多个属性且需要同时成功的复杂协议。

序列 s18a 检查一个简单的条件。序列 s18a_ext 检查相同的条件，但是序列的成功被往后移了一个时钟周期。当这个序列被用在一个属性的现行算子时，它会造成一些差异。两个序列的结束
点不同，因此开始检查后续算子的时钟周期也不一样。

属性 p18 检查先行算子中的 s18a.end，如果成功，两个时钟周期后，检查 s18b.end 是否成功。属性 p18_ext 检查 s18a_ext 在先行算子中是否成功。这个成功与 s18a.ended 的成功相同，但是早了一个时钟周期。因此属性 p18_ext 的后续算子需要在一个时钟周期而不是像 p18 中定义的两个时钟周期后成功。属性 p18 和 p18_ext检查相同的情况，但是他们在先行算子中的成功点却不同。

1.20 "$past"构造

SVA 提供了一个内嵌的系统任务“ $past”，它可以得到信号在几个时钟周期之前的值。在默认情况下，它提供信号在前一个时钟周期的值。结构的基本语法如下。

$past (signal_name， number of clock cycles)
 

这个任务能够有效地验证设计到达当前时钟周期的状态所采用的通路是正确的。属性 p19 检验的是在给定的时钟上升沿，如果表达式(c&&d)为真，那么两个周期前，表达式(a&&b)为真。

 1.20.1 带时钟门控的$past 构造

$past 构造可以由一个门控信号(gating singal)控制。比如，在一个给定的时钟沿，只有当门控信号的值为真时才检查后续算子的状况。使用门控信号的$past 构造的基本语法如下：
$past (signal_name， number of clock cycles， gatingsignal)

属性 p20 与属性 p19 相似。但是只有当门控信号“ e”在任意给定的时钟上升沿有效时检验才被激活。

1.21 重复运算符

如果信号“ start”在任何给定的时钟上升沿跳变为高，接着从下一个时钟周期起，信号“ a”保持三个连续时钟周期为高，然后下一个时钟周期，信号“ stop”为高。像上述描述的序列可以使用下面的 SVA 代码来检验。

@(posedge clk) $rose(start) |-> ##1 a ##1 a ##1 a ##1 stop

如果信号“ a”需要在很多个周期中保持高电平，编写这样一个检验器可能会非常冗长。而且这个例子要求信号“ a”连续地保持高电平。当我们只希望检查信号“ a”是否在被检测时保持为高，而不一定是三个连续的时钟周期的时候，协议就会变得复杂起来。换句话说，信号“ a”需要连续地或者间歇地重复自己三次。

SVA 语言提供三种不同的重复运算符：

1. 连续重复(consecutive repetition)；
2. 跟随重复(go to  repetition)；
3. 非连续重复(non-consecutive repetition)。
    

连续重复—— 允许用户表明信号或者序列将在指定数量的时钟周期内都连续地匹配。信号的每次匹配之间都有一个时钟周期的隐藏延迟。连续重复运算符的基本语法如下所示。

signal or sequence [*n]

“ n”是表达式应该匹配的次数。

比如， a[*3]可以被展开成下面的式子。

a ##1 a ##1 a

而序列(a##1b)[*3]可以展开为

(a ##1 b) ##1 (a ##1 b) ##1 (a ##1 b)
 

跟随重复—— 允许用户表明一个表达式将匹配达到指定的次数，而且不一定在连续的时钟周期上发生。这些匹配可以是间歇的。跟随重复的主要要求是被检验重复的表达式的最后一个匹配应该发生在整个序列匹配结束之前。跟随重复运算符的基本语法如下所示。

signal [->n]

参考下面的序列：

start ##1 a[->3] ##1 stop

这个序列需要信号“ a”的匹配(即信号“ a”的第三次，也就是最后一次重复的匹配)正好发生在“ stop”成功之前。换句话说，信号“ stop”在序列的最后一个时钟周期匹配，而且在前一个时钟周期，信号“ a”有一次匹配。

非连续重复—— 与跟随重复相似，除了它并不要求信号的最后一次重复匹配发生在整个序列匹配前的那个时钟周期。非连续重复运算符的基本语法如下所示。

signal [=n]

在跟随重复和非连续重复中只允许使用表达式，不能使用序列。

1.21.1 连续重复运算符[*]

属性 p21 检查在检验有效地开始两个时钟周期后，信号“ a”在连续的三个时钟周期为高，再过两个时钟周期，信号“ stop”为高。下一个时钟周期，信号“ stop”为低。
 

property p21;
        @(posedge clk) $rose(start) |->
        ##2 (a[*3]) ##2 stop ##1 !stop;
endproperty
a21： assert property(p21);

1.21.2 用于序列的连续重复运算符[*]

属性 p22 检查有效开始的两个时钟周期以后，序列(a ##2 b)重复三次，接着再过两个时钟周期，信号“ stop”为高。
 

 

 1.21.3 用于带延迟窗口的序列的连续重复运算符[*]

属性 p23 检查在有效开始的两个时钟周期后，序列(a ##[1：4] b)重复 3 次，接着再过两个时钟周期，信号“ stop”为高。实际上，这个序列有一个时序窗口，使得情况变得有些复杂。

property p23;
        @(posedge clk) $rose(start) |->
                ##2 ((a ##[1:4] b)[*3]) ##2 stop;
endproperty
a23： assert property(p23);
主序列(a ##[1： 4] b)[*3]可以被扩展成：
        ((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b)) ##1
        ((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b)) ##1
        ((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b))

1.21.4 连续运算符[*]和可能性运算符

属性 p23 指定了一个重复序列的时序窗口。同样的，重复的次数也可以是一个窗口。比如， a[*1： 5]表示信号“ a”从某个时钟周期开始重复 1~5 次。这个定义可以展开成下面的表达式。
 

 重复窗口的边界规则与延迟窗口的相同。左边的值必须小于右边的值。右边的值可以是符号“ $”，这表示没有重复次数的限制。
属性 p24 显示了一个带没有重复次数限制的有限的检查。它检验有效开始两个时钟周期后，信号“ a”将保持为高，直到信号“ stop”跳变为高。

 

1.21.5 跟随重复运算符[->]
 

属性 p25 检查如果在任何时钟上升沿有有效的开始，两个时钟周期后， 信号“ a”连续或者间断地出现 3 次为高， 接着信号“ stop”在下一个时钟周期为高。
 

 1.21.6 非连续重复运算符[=]

属性 p26 检查如果在任何时钟上升沿有有效的开始信号，两个时钟周期后，在一个有效的“ stop”信号前，信号“ a”连续或者间断地出现 3 次为高，然后一个时钟周期后“ stop”应该为低。p26 和 p25 做的是相同的检查， 唯一的不同是 p26 使用的是非连续(non-consecutive)重复运算符而不是跟随(go to)重复运算符。这表示在属性 p26 中，在信号“ stop”有效匹配的前一个时钟周期，信号“ a”不一定需要有有效的匹配。
 

1.22 "and"构造

二进制运算符“ and”可以用来逻辑地组合两个序列。当两个序列都成功时整个属性才成功。两个序列必须具有相同的起始点，但是可以有不同的结束点。检验的起始点是第一个序列的成功时的起始点，而检验的结束点是使得属性最终成功的另一个序列成功时的点。
序列 s27a 和 s27b 是两个独立的序列。 属性 p27 将两者用运算符“ and”组合起来。当两个序列都成功时，属性成功。

 

 

 1.23 “intersect”构造

“ intersect”运算符和“ and”运算符很相似，它有一个额外要求。两个序列必须在相同时刻开始且结束于同一时刻。换句话说，两个序列的长度必须相等。

1.24 ”or“构造

二进制运算符“ or”可以用来逻辑地组合两个序列。只要其中一个序列成功，整个属性就成功。

 

 持续更新......