11.5SVA检验器的时序窗口
到目前为止,带延迟的例子使用的都是固定的正延迟。在下面几个例子中,我们将讨论几种不同的描述延迟的方法属性p12检查布尔表达式“a&&b”在任何给定的时钟上升沿为真。如果表达式为真,那么在接下去的1-~3周期内,信号“c”应该至少在一个时钟周期为高。SA允许使用时序窗口来匹配后续算子。时序窗口表达式左手边的值必须小于右手边的值。左手边的值可以是0。如果它是0,表示后续算子必须在先行算子成功的那个时钟边沿开始计算。
property p12;
@(posedge clk) (a && b ) |-> ##[1:3] c;
endproperty
a12: assert property(p12);图1-15显示了属性p12在模拟中的响应。每声明一个时序窗口,就会在每个时钟沿上触发多个线程来检查所有可能的成功。p12实际上以下面三个线程展开。
(a && b ) |-> ##1 c 或
(a && b ) |-> ##2 c 或
(a && b ) |-> ##3 c 属性有三个机会成功。所有三个线程具有相同的起始点,但是一旦第一个成功的线程将使整个属性成功。应当注意,在任何时钟上升沿只能有一个有效的开始,但是可以有多个有效的结束。这是因为每个有效的起始可以有三个机会成功。
表1-8总结了属性计算过程中所有相关信号的采样值。在任何给定的时钟上升沿,如果信号“a”和信号“b”不全为高,那么属性得到一个空成功。另一方面,如果信号“a”和信号“b都为高,那么属性就有了一个有效的开始。如果信号“c”在之后的1~-3个时钟周期内都没被检测到高电平,属性失败。
注意,属性在时钟周期2和3都有有效的开始。这两个有效的开始同时在时钟周期4成功。时钟周期2开始的检查在两个时钟周期后检测到信号“c”为高。而时钟周期3开始的检查在一个时钟周期后检测到信号“c”为高。这两个都是有效情况,因此它们都成功了。在时钟周期12同样有一个有效的开始。属性在时钟周期13,14和15都检测信号“c”是否为高。由于信号“c”在这所有三个可能的时钟周期始终为低,检测失败。
1.15.1重叠的时序窗口
属性p13与属性p12相似。两者最大的区别是p13的后续算子在先行算子成功的同一个时钟沿开始计算。
property p13;
@(posedge clk) (a && b ) -> ##[0:2] c;
endproperty
a13: assert property(p13); 图1-16显示了p13在模拟中的响应。与属性p12最大的区别在于一个成功的开始发生在时钟周期12。这个成功是因为检查发生了重叠。信号“c”的值在先行算子成功的同一个时钟沿被检测为高。
1.15.2无限的时序窗口
在时序窗口的窗口上限可以用符号“$”定义,这表明时序没有上限。这叫作“可能性”( eventuality)运算符。检验器不停地检查表达式是否成功直到模拟结束。因为会对模拟的性能产生巨大的负面影响,所以这不是编写SVA的一个高效的方式。最好总是使用有限的时序窗口上限。属性p14在任何给定的时钟上升沿检查信号“a”是否为高。如果为高,那么信号“b”从下一个时钟周期往后最终将为高,而信号“c”在信号“b”为高的时钟周期开始往后最终将为高。
property p14;
@(posedge clk) a |-> ##[1:$] b ##[0:$] c;
endproperty
a14: assert property(p14); 图1-17显示了属性p14在模拟中的响应。表1-9总结了断言a14和相关信号的采样值。值得注意的是,真正的成功可能在任意个时钟周期后结束。如果一个有效的开始发生,而信号“b”或信号“c”在模拟结束前始终不为高,这些检查被报告为“未完成检验”( incomplete check)。因为信号“b”和信号“c”可以重叠地满足检验,整个检查有可能在一个时钟周期内结束。时钟周期17显示了这样一种情况,当信号“a”在时钟周期17被检测为高,且信号“b”和信号“c”在时钟周期18都被检测为高。
