SVA介绍----SVA的时序窗口

1. 非固定的时序窗口

//检查a&&b成功后，那么在接下来的1～3个时钟周期内，信号c应该至少在一个时钟周期为高电平
property p12;
	@(posedge clk)  (a&b) |-> ##[1:3] c;
	//类似于以下代码：
	// (a&&b) -> ##1 c 或
	// (a&&b) -> ##2 c 或
	// (a&&b) -> ##3 c
endproperty
a12: assert property(p12);

属性p12一共有三次机会成功，三个线程具有相同的起始点(a&&b成功)，但是一旦第一个成功的线程，会使得整个属性成功；

2. 重叠的时序窗口

//检查a&&b成功后，那么在接下来的0～2个时钟周期内，信号c应该至少在一个时钟周期为高电平
property p13;
	@(posedge clk)  (a&b) |-> ##[0:2] c;
	//类似于以下代码：
	// (a&&b) -> c 或
	// (a&&b) -> ##1 c 或
	// (a&&b) -> ##2 c
endproperty
a13: assert property(p13);

属性p13与p12类似，一共有三次机会成功，三个线程具有相同的起始点(a&&b成功)，但是一旦第一个成功的线程，会使得整个属性成功；但不同的是，如果 a&&b 成功的同一个时钟沿，信号c也是高电平，那么属性p13检查成功；

3. 无限的时序窗口

//检查a&&b成功后，那么在接下来的0～2个时钟周期内，信号c应该至少在一个时钟周期为高电平
property p14;
	@(posedge clk)  (a&b) |-> ##[1:$] c;
	//类似于以下代码：
	// (a&&b) -> c 或
	// (a&&b) -> ##1 c 或
	// (a&&b) -> ## n
endproperty
a14: assert property(p14);

线程具有相同的起始点(a&&b成功)，但是一旦第一个成功的线程，会使得整个属性成功；但不同的是，如果 a&&b 成功后，此后的任何一个时钟沿，只要信号c为高电平，属性p14成功。在时序窗口的上限可以使用符号"$",表示对时序的要求没有上限，这被称作可能性(eventuality)运算符。

4. ended结构

到目前为止，定义的序列都只是使用了简单的连接机制，即将多个序列以序列的起始点作为同步点，来组合形成时间上连续的检查。SVA也提供了使用序列的结束点进行检查的机制，这种机制需要在表示序列的名字上追加“ended”来表示。

//使用结束点检查机制
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);

属性p15a通过基于序列的起始点来同步序列，p15b通过序列的结束点来同步序列；(但是两个属性具有相同的检查机制) (如果a为低电平，那么p15a/p15b都是空成功) 举例：

1. 激活时间：

在时钟上升沿0/1，a/b信号分别为高电平； 在时钟0 (信号a检测为高)，p15a被激活； 在时钟1 (信号b检测为高)，p15b被激活；

2. 成功时间：

p15a被激活后(时钟0)，一个时钟周期后(时钟1)，b为高电平,再经过一个时钟周期后(时钟2)，c为高电平，再经过一个时钟周期后(时钟3)，d为高电平，此时p15检查通过； p15b被激活后(时钟1)，一个时钟周期后(时钟2)，c为高电平,再经过一个时钟周期后(时钟3)，d为高电平，此时p15检查通过；