SVA-GRAMMAR

SVA的位置

在.v文件中

module ABC();
	rtl代码
	SVA断言
end mudule

断言的格式

断言1

assert property(事件1)
	$display("......",$time);
else
	$display(".......",$time);

断言2

assert property(事件2)
	$display("......",$time);
else
	$display(".......",$time);

含义：断定”事件1”和“事件2”会发生，如果发生了，记作pass，否则记作fail

事件1和事件2的两种书写格式

序列块

sequence name;//常用于组合逻辑断言
	...
endsequence

属性块

property name;//常用于有时间观念的断言，可用于调用sequence
	...;
endproperty

调用sequence或者property
```
assert property(name)
```

带参数的property,sequrnce

assert property(p1(a,b))//调用的property带参数

sequence s1;//被主sequence调用的sequence带参数
	s2(a,b);
endsequence

property内部定义局部变量

property p1;
	int cnt;
	......
endproperty

注：断言的一般格式

通常基于时序逻辑，组合逻辑少见
一般规则time+event，如时钟上升沿+发生某事或者信号下降+发生某事

语法

语法1：信号（事件）之间的组合逻辑关系

常见的有：&&，||，！，^
firstmatch(a||b)：从左到右检查第一个匹配的序列，如果a和b都匹配，优先选择a作为匹配结果
a?b:c：a事件成功后，触发b，a不成功则触发c

语法2：在“时序逻辑”中判断独立的一根信号的行为

@(posedge clk) A事件；//当clk上升沿时，如果发生A事件，断言将会报警（即断言失败）

//边沿触发内置函数：
$rose(a);//信号上升，即如果信号a从0变为1，$rose(a)返回值为1，否则为0
$fell(a);//信号下降，即信号a从1变为0时，$fell(a) 的返回值为1，否则为0
$stable(a);//信号值不变,即如果信号a在当前时钟周期和上一个时钟周期的值相同，$stable(a)的返回值为1，否则为0

语法3：在“时序逻辑”中判断多个事件/信号的行为关系

intersect(a,b)//断定a和b两个事件同时发生且同时结束

a within b//断定b事件的发生的时间段里包含a事件发生的时间段

a ##2 b//断定a事件发生后2个单位时间内b事件一定会发生

a ##[1;3]//断定a事件发生后1~3个单位时间内b事件一定会发生

a ##[3:$]//断定a事件发生后3个周期内b事件一定会发生

c throughout(a##2 b)//断定a事件成到b事件成立的过程中,c事件一直成立

@ (posedge clk) a|->b//断定clk上升沿后，a事件“开始发生”，同时，b事件发生

@ (posedge clk) a end|->b//断定clk上升沿后，a事件执行了一段实践结束后，同时，b事件发生

@ (posedge clk) a-=>b//断定clk上升沿后，a事件开始发生，下一个时钟沿后，b事件开始发生

@ (posedge clk) a-=>##2b//断定clk上升沿后，a事件开始发生，下三个时钟沿后，b事件开始发生

@（posedge clk) $past(a,2)== 1`b1//断定a信号在2个时钟周期“以前”，电平值都是1

@ (posedge clk) a[*3]//断定@(posedge clk)a在连续3个时钟周期内都成立
@ (posedge clk) a[*1：3]//断定posedge clk)a在连续1~3个时钟周期内都成立
@ (posedge clk) a[->3]//断定@(posedge clk)a可以在非连续的3个时钟周期内成立

举例子：

property ABC;
	int tmp;
	@(posedge clk) ($rose(a),tmp=b)|->##4(c==(tmp*tmp+1)) ##3 d[*3];
endproperty

以上property说明：clk上升沿时，首先断定a信号由低变高，此时把b信号的值赋给tmp变量，在4个时钟周期后，断定信号c的值是4个周期前b^2+1，在延迟3个时钟周期，b信号会在接下来的3个时钟周期内都为真，再过三个周期，b信号会再来……

如果以上都成立默认为断言成功。或者从一开始信号a没有上升沿，断言也成功

语法4：多时钟域联合断言

(posedge clk1) a|-> ##1 @(posedge clk2) b

当clk1上升沿时，事件a发生（高电平），紧接着如果过来第二个时钟后面的clk2的上升沿，则b发生。##1在跨时钟时，不表示一个时钟周期，只表示等待最近的一个跨时钟事件，所以此时不能写成##2

但是可以写成：

@(posedge clk1) a|=> @ (posedge clk2) b

语法5：总线的断言函数

总线是很多跟bit线，共同表示一个数，SVA提供了多bit状态一起判断的函数

$onehot(BUS)//BUS中有且仅有1位为高，其他为低
$onehot0(BUS)//BUS中有不超过1位为高，也可以全为低
$isunknown(BUS)//BUS中存在高阻态或未知态
countones(BUS)==n//BUS中有且仅有n bits为高，其他为低

语法6：屏蔽不定态

当信号被断言时，如果信号是未复位的不定态，无论如何断言，都会报告”断言失败“。为了不报告此类问题，可以屏蔽断言。

比如，@(posedge clk) (q==$past(d)),当未复位的时候会报错，可以将其屏蔽：

@(posedge clk) disable iff(!rst_n) (q==$past(d))

语法7：断言覆盖率检测

name: cover poperty(func_name)

在modelsim中开启断言编译和显示功能

编译verilog代码时，按照system verilog进行编译
```
vlog -sv anc.v
```
仿真命令，加一个-assertdebug
```
vsim -assertdebug =novopt testbench
```
使用打开断言窗口的命令来查看断言成功与否
```
view assertions
```

经验

断言中可以有function和task
断言可以规定同时发生的事情：a&&b或者a##0 b

断言要用变量

##4 var=signal//错误写法，没有对rtl信号的任何断言
##4(废话,var=signal)//正确的

断言风格：要表示
```
if a1
{
	if a2
	then b
}
```
因该用a1&&a2|->b或者a1##3 a2|->b来表示
若要表示“当clk上升沿到来的时候，b<=a。要将上述逻辑写成断言，应该使用

@(posedge clk)(a==a,tmp==a)|=>(b==tmp)

因为时钟沿到来的时候，b还没有得到a的值，保存的是时钟沿到来之前的值

在SVA中实现类似for功能的唯一方法：

##4 (废话，cnt=0,arr[cnt]=DateIn,cnt++)//初始化
##1 （read=read,arr[cnt]=DataIn,cnt++)[*3]//循环3次

使用了|->，就不能再用&&事件的组合逻辑了，比如：
```
property ept_p;
    @(posedge rd_clk) ((rd_num==0)|->rd_ept)
    &&(rd_ept|->(rd_num==0));
endproperty
```
解决方法是只能使用两个断言，没有别的方案