SVA学习_sva嵌套的蕴含

---

一、断言

断言是设计属性的描述：

1. 如果一个设计属性在仿真中不像我们期望那样表现，那么这个断言失败
2. 如果一个不期望出现的设计属性在仿真中发生，那么这个断言失败
   断言分为即时断言和并发断言

1. 即时断言

即时断言特点：
  （1）即时断言与时序无关
  （2）必须放在过程块中
  （3）只能用于动态模拟(仿真)
如：

always_comb
	begin
	   a_ia: assert(a&b);
	end
1
2
3
4

注：always_comb为sv语法，可自动嵌入敏感列表

2. 并发断言

并发断言特点：
  （1）并发断言与时序相关
  （2）可以放在过程块、模块(module)、接口(interface)或者一个程序(program)中
  （3）可以在静态(形式的)验证和动态模拟(仿真)工具中使用
如：

a_ib:assert property(@(posedge clk) not(a&b));
1

3. 即时断言和并发断言的区别

并发断言有关键词“property”
即时断言无关键词“property”

二、SVA块

1. 序列(sequence)

基本语法：

sequence name_of_sequence;
	    <test expression>; (即：逻辑事件的组合)
endsequence
1
2
3

注：sequence可以参数化，如：

sequence para_exs(para1,para2);
	para1 || para2;
endsequence
1
2
3

property para_exp;（即：时钟上升沿，a或b有一个信号为高即断言成功）
	@(posedge clk) para_exs(a,b);
endproperty
1
2
3

2. 属性(property)

基本语法：

property name_of_property;
	<test expression>;(即：逻辑事件的组合)
	//or
    //<name_of_sequence>;(即：引用序列)
endproperty
1
2
3
4
5

3. 断言(assert)

基本语法：

name_of_assertion:assert property(name_of_property);//并发断言
1

4.两段式断言/三段式断言

（1）三段式断言

sequence name_of_sequence;
	<test expression>; (逻辑事件的组合)
endsequence

property name_of_property;
	<complex sequence expressions>;
endproperty
	
name_of_assertion:assert property(name_of_property);//并发断言
1
2
3
4
5
6
7
8
9

（2）两段式断言

property name_of_property;
	<test expression>;
endproperty

name_of_assertion:assert property(name_of_property);//并发断言
1
2
3
4
5

注：1.两段式的断言结构应用更多
  2.同一个断言相关的属性(property)和断言(assert)只能有一个时钟定义

三、SVA内嵌函数

1.$rose(boolean expression or name of signal)：当信号/逻辑表达式由低变高时返回真

注：rose采样的是电平变化，而非上升沿，见下图。clk2时，信号a被采样为低电平；clk3时，信号a被采样为高电平。在clk3处，信号a被认为由低变高，$rose(a)为真。

2.$fell(boolean expression or name of signal)：当信号/逻辑表达式由高变低时返回真

注：fell采样的是电平变化，而非下降沿，见下图。clk2时，信号b被采样为高电平；clk3时，信号b被采样为低电平。在clk3处，信号b被认为由高变低，$fell(b)为真。

3. $stable(boolean expression or name of signal)：当表达式不发生变化时返回真
4. $onehot(expression)：检验表达式满足"one-hot"，即：表达式只有一位为高
5. $onehot0(expression)：检验表达式满足"zero one-hot"，即：表达式只有一位为高或者没有任何位为高
6. $isunknow(expression)：检验表达式的任何位是否是X或者Z
7. $countones(expression)：计算向量中为高的位的数量

四、断言的执行块

SystemVerilog语言中每当一个断言检查失败，仿真器在默认情况下都会打印一条错误信息，对成功的断言不会打印任何东西。因此如果设计者想要自定义断言成功或失败之后的信息，可以通过断言的执行块进行。
执行块语法

assertion_name:assert property(name_of_property)
  <success message>;
else
  <fail message>;
1
2
3
4

五、蕴含(implication)

蕴含的主要作用为：检测起始点无效时忽略这次检查。蕴含等效于一个if-then结构。蕴含的左边叫做“先行算子”，右边叫做“后续算子”。先行算子是约束条件，先行算子成功时，后续算子才会被计算。蕴含结构只能被用在属性定义中，不能在序列中使用。蕴含分为：交叠蕴含(overlapped implication)和非交叠蕴含(non-overlapped implication)。

1. SVA检测器的时序窗口

（1）SVA中，时钟周期延迟用“##”表示。如：##2表示延迟2个时钟周期
（2）##[1:3]表示时间窗口，延迟1~3个时钟周期。时间窗口下限可以为0，如果为0则表示不延迟，在同一个时钟周期发生
（3）时序窗口的上限可以为“$”，表示时序没有上限。这叫做“可能性”(eventuality)运算符，如：

property even_exp;
	@(posedge clk) a |-> ##[1:$] b ## [1:$] c;
endproperty
even_exa:assert property(even_exp);
1
2
3
4

属性even_exp在时钟上升沿检查信号a是否为高，如果为高，下个时钟上升沿检查信号b是否为高，如果是高则再下一个时钟周期检查信号c是否为高（没有时序上限，一直检查直到c为高之后断言成功），如果b在a为高后的下个时钟不为高，则需要等待b为高之后($,没有时序上限一直检查)再检查c是否为高。

2. 交叠蕴含(|->)

如果先行算子匹配成功，在同一个时钟周期计算后续算子表达式。用符号“|->”表示。如：

property over_imp_exp;
    @(posedge clk) a |-> b;
endproperty
over_imp:assert property(over_imp_exp);
1
2
3
4

属性over_imp_exp在时钟上升沿检查信号“a”是否为高，如果是高，信号“b”在同一个时钟边沿也为高，则断言成功，否则失败。

3. 非交叠蕴含(|=>)

如果先行算子匹配成功，那么在下一个时钟周期计算后续算子表达式。用符号“|=>”表示。如：

property over_nonimp_exp;
    @(posedge clk) a |=> b;
endproperty
over_nonimp:assert property(over_imp_exp);
1
2
3
4

属性over_nonimp_exp在时钟上升沿检查信号“a”是否为高，如果是高，信号“b”在下一个时钟边沿也为高，则断言成功，否则失败。

4. 后续算子带固定延迟

property ex;
    @(posedge clk) a |-> ##2 b;
endproperty
ex_a:assert property(ex);
1
2
3
4

注:交叠蕴含表达式：a |-> ##1 b
  非交叠蕴含表达式：a |=> b
所检验的属性相同

5.使用序列做先行算子/后续算子

sequence slla;
    @(posedge clk) (a && b) ##1 c;
endsequence

sequence sllb;
    @(posedge clk) ##2 !d;
endsequence

property p11;
    slla |-> sllb;
endproperty

a11:assert property(p11);
1
2
3
4
5
6
7
8
9
10
11
12
13

属性p11检查，在时钟上升沿，如果a和b均为高，那么一个周期后c为高，两个时钟周期后，d为低，则断言成功，否则断言失败。

6. 嵌套的蕴含

嵌套的蕴含，即在一个表达式中多次使用蕴含，如：