请高手指点SVA ended construct的问题

yjh

有哪位兄才知道SVA ended construct：
sequence s15a; @(posedge clk) a ##1 b; endsequence
sequence s15b; @(posedge clk) c ##1 d; endsequence
property p15a; @(posedge clk) s15a |=> s15b; endproperty
property p15b; @(posedge clk) s15a.ended |-> ##2 s15b.ended; endproperty
a15a: assert property(p15a);
a15b: assert property(p15b);
这里的ended的具体作用是什么？有人知道么？
有和没有这个ended有什么区别呢？

lissee_lissee

语法书上有

xmandxm

最近在看SVA相关的，貌似《A Practical Guide for SystemVerilog Assertions》上面的例子吧。加不加ended，影响的只是synchronization的点，加了ended是以该sequence的ending point做为参考同步点。拿s15a来说，在clk的第N个上升沿，a=1,且N+1个上升沿，b=1，那么该sequence为true，进而去判断s15b。如果不加ended，s15a的synchronization是以sequence的起始点a=1，即第N个clk上升沿为参考，加了ended是以该sequence的终点即b=1，即N+1个clk上升沿为参考。
可能不对，望大神指点。

alien920804

回复 3# xmandxm
我最近也是在看《A Practical Guide for SystemVerilog Assertions》，也是对楼主所提的问题疑惑不解，看了你的解释，感觉说得挺对的。不过我还有一个疑问想要请教你。对于page57对应ended给出的那段代码给出的波形中，对于a15a的波形，是不是应该是s15a success之后的一个时钟有效沿s15b也success，a15a才会success。因为它是这么描述的：property p15a; @(posedge clk) s15a |=> s15b; endproperty

但我看书上的波形仿佛不是这么回事。求解答~