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);
endfunction
8、如果想在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 b
b[->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