1.16“ended”结构

        到目前为止,定义的序列都只是用了简单的连接( concatenation)的机制。换句话说,就是将多个序列以序列的起始点作为同步点,来组合成时间上连续的检查。SVA还提供了另种使用序列的结束点作为同步点的连接机制。这种机制通过给序列名字追加上关键词“ ended”来表示。例如,s. ended表示序列的结束点。关键词“ ended”保存了一个布尔值,值的真假取决于序列是否在特定的时钟边沿匹配检验。这个 s.ended的布尔值只有在相同时钟周期有效。
        序列sl5a和s15b是两个需要多个时钟周期来完成的简单序列,属性pl5a检查序列s15a和序列s15b满足两者间隔一个时钟周期的延迟分别匹配检验。属性p15b检査相同的协议,但是使用了关键词“ ended”。在这种情况下,两个序列在结束点同步。由于使用了结束点,两个序列间加上了两个时钟周期的延迟,来保证断言检验的协议与pl5a相同。

sequence s15a ;
	@(posedge clk) a ##1 b;
endsequence

sequence s15b;
	@(posedge clk) c ##1 d;
endsequence

property p15a;
	s15a |-> s15b;
endproperty

property p15b;
	s15a.ended |-> ##2 s15b.ended;
endproperty

a15a: assert property(p15a);
a15b: assert property(p15b);

        图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为假。上述例子中,我们用了两种不同的方法来实现统一个检验。
        第一种方法基于序列的起始点来同步序列。第二种方法基于序列的结束点来同步序列。