SystemVerilog Assertion(SVA)編寫經驗
1、断言的目的：
传统的验证方法是通过加激励，观察输出。这种方法对案例的依赖严重，案例设计不好，问题不便于暴露。而断言是伴随RTL代码的，不依赖测试案例，而是相对“静态”。例如：我们要测试一个串行数据读写单元，数据线只有一根，先传四位地址，再传数据。
（1）案例验证法：
- 写一个地址，再写一段数据，然后读取该地址，看输出的是不是刚才写的数据。
（2）断言法：
- 不需要专门设计地址和数据，当发起写时，在地址传输的时间里将地址存储到一个变量里，在数据传输的时间里将数据存储到一个变量里，观察RAM中该地址是否存在该数据就可以了。
（3）斷言的實質：
- 断言设计相当于在电脑上把RTL实现的功能再实现一遍。
2、断言中可以包含function和task。
而且function经常用于断言，因为有的处理很复杂，而断言又是“一句式”的，无法分成好几句进行表达，所以需要function替断言分担工作。
3、断言允许规定同时发生的事件
- 就是组合逻辑，你可以写成：a && b，也可以写成 a ##0 b，不能写 ##0.5，不支持小数
4、断言是用电脑模仿RTL的运行过程
当RTL功能复杂时，你必须用到变量。断言中支持C语言的int和数组声明，但在赋值时“不能”写成：##4 var = Signal，其中var是断言中的变量，和RTL无关，Signal是RTL中的一个信号。
本句是想在第4周期将Signal的值赋给var，以便在后面使用该值。但本句只有变量赋值，没有对RTL信号的任何断言，就会报错，解决方法是：##4 (“废话”，var = Signal)，一定要有断言的话我们就写“废话”，例如:data == data 等。
如果有多个变量要赋值也可以，##4 （废话，变量1赋值，变量2赋值...........）
5、关于断言的表达风格
- 语法介绍的 “a |-> b”，实际上是 “if a, then b”的逻辑，当a不发生，b也不会被判断，该断言自然成功。
- 但当我们的逻辑是
if a1 {
if a2 {
then b
}
}该如何用断言表达？？？？ 或许可以写成：“a1 |-> a2 |-> b”也可以？但常用的表达是：
a1 && a2 |-> b;
//或者
a1 ##3 a2 |-> b;6、关于断言的时序：时序逻辑的断言需要注意的一个问题：
例如：假设当clk上升沿到来时，b <= a。将上述逻辑写成断言时，如果写成“@(posedge clk) b==a”，看起来和 b<=a一样，但实际上是错的。因为当时钟上升时，b还没有得到a的值，a还需要一段保持时间。
- 断言中的信号值实际上是时钟沿到来之前的值，而不是时钟沿到来后他们将要變成的值。
- 所以，b <= a逻辑的断言应是：@ (posedge clk) (a === a, tmp = a) |=> (b === tmp);
- 针对上述几点，举一个复杂的例子：
- 断言wr的功能是检查串行地址输入是否正确，串行地址输入线是 DataIn 。
- $time返回值以0.1ns为单位（因为我在testbench中的单位规定是`timescale 1ns/100ps，精度是100ps = 0.1ns），所以$time/10才是ns。
wr: assert property(wr_p)
$display("succeed：", $time/10);
else
$display("error: ",$time/10);7、断言可以声明一个int数组
- 例如arr[4]，
@(posedge clk) !vld_pulse_r[0] && !DataIn //是真实的预备条件
##4 (read == read, arr[0] = DataIn) //只是为了在特定时间内赋值，有用的语句是“arr[0] = DataIn”，
//“read==read”是废话，为了编译通过。
//arr赋值完毕后，进入function进行处理，判断实际地址addr跟junc处理过的数据是否相同。
addr == junc(arr[0], arr[1], arr[2], arr[3]); //就是junction调用。property wr_p;
int arr[4];
@(posedge clk) !vld_pulse_r[0] && !DataIn
##4 (read==read, arr[0] = DataIn)
##1 (read==read, arr[1] = DataIn)
##1 (read==read, arr[2] = DataIn)
##1 (read==read, arr[3] = DataIn) |=>
addr == junc(arr[0],arr[1],arr[2],arr[3]);
endproperty/////////////////////////////////////////////////////////////////////////////////////////////////////////
function [3:0] junc;
input a,b,c,d;
reg [3:0] a1;
reg [3:0] b1;
reg [3:0] c1;
reg [3:0] d1;
a1 = {3'b0,a};
b1 = {3'b0,b};
c1 = {3'b0,c};
d1 = {3'b0,d};
junc = a1 + (b1<<1) + (c1<<2) + (d1<<3);
$display(junc);
endfunction8、如果想在SVA中使用类似for() {....}的功能
8.1、别忘了语法中介绍的[*3]，这是在断言中实现for的唯一方式。
##4 (废话, cnt = 0, arr[cnt] = DataIn, cnt++) //初始化一下，
##1 (read == read, arr[cnt] = DataIn, cnt++)[*3] //循环3次8.2、[*n : $], [*] [+]连续循环，是针对sequence的连续循环
- [* n：$]结构类似于[* n：m]，除了m被$符取代，$符代表无限的意思，并且n意味着重复最少n个周期。
- [*]是[* 0：$]的缩写，表示重复至少0次，最多无限次。
- [+]是[* 1：$]的缩写，表示重复至少1次，最多无限次。
8.3、[=n], [=n:m] 非连续循环算子
能够对不连续的循环进行评价，循环评价结束时，不连续的可能性依然继续。重复次数可以是固定常数或固定范围。
b[=m] is equivalent to:
b [->m] ##1 !b [*0:$]
b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]b[=2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]- a |=> (b[=2] ##1 c);
该属性指出，如果从a成立下一个周期开始，那么b应该成立两次，b要么是连续的要么是不连续的，然后稍后一段时间（即下一个周期或之后）出现c。
如果在第二次出现b后出现新的b（且 c 没有成立），则该属性失败。但是，如果在b的第二次成立之后，c在新的b之前的任何时间发生，或者与最后一次b同时出现，则属性成功。
8.4、[->n ], [->n:m] goto循环算子
goto循环算子（Boolean[ - > n]）允许布尔表达式（而不是序列）在连续或不连续的循环中重复，而且循环评价结束时，不连续的可能性也结束了。 重复次数可以是固定常数或固定范围。
b [->m] is equivalent to:
(!b [*0:$] ##1 b)[*m]
b[->1] is equivalent to:
!b[*0:$] ##1 bb[->2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b- a |=>（b [->2] ## 1 c）;
上述属性指出，如果从a成立下一个周期开始，那么b应该成立两次，它可以是连续的或不连续的。 但是，c必须发生在b最后一次出现的下一个周期。
9、每句断言都是一个小程序：
如上例，在##4时间点上，(废话, cnt = 0, arr[cnt] = DataIn, cnt++)就是一个小程序，信号断言必须是第一句，其他运算按照顺序进行。
10、断言中的变量類型
- 除了可用C语言中的int，float外，还可以是reg [n:0]等数字电路类型。
11、注意：兩條蘊含之間不能做邏輯運算
- 像这种写法：
property ept_p;
@(posedge rd_clk)
((rd_num == 0) |-> rd_ept) &&
(rd_ept |-> (rd_num == 0));
endproperty- 是错误的，写了|->，就不能再用 && 等事件组合逻辑了。
- 解决方法是使用2个断言，没更好的方法。
12、致謝
12.1、本文摘自：Link
12.2、本文摘自：Link
12.3、特別鳴謝：白栎旸
12.4、特別鳴謝：PlPyRbC
