请高手指点SVA ended construct的问题
时间:10-02
整理:3721RD
点击:
有哪位兄才知道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有什么区别呢?
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有什么区别呢?
语法书上有
最近在看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上升沿为参考。
可能不对,望大神指点。
我最近也是在看《A Practical Guide for SystemVerilog Assertions》,也是对小编所提的问题疑惑不解,看了你的解释,感觉说得挺对的。不过我还有一个疑问想要请教你。对于page57对应ended给出的那段代码给出的波形中,对于a15a的波形,是不是应该是s15a success之后的一个时钟有效沿s15b也success,a15a才会success。因为它是这么描述的:property p15a; @(posedge clk) s15a |=> s15b; endproperty
但我看书上的波形仿佛不是这么回事。求解答~