文章目录
一、转载链接
https://blog.csdn.net/qq_41394155/article/details/83117143
自己看理解不太深刻，便照着写了一下啦
二、SVA介绍
- 断言assertion可以用来判断仿真时，是否出现异常情况，某些情况是否执行过，用于覆盖率的收集。
- 可以把断言理解为if语句，但是比if更复杂，不同的断言的语法可以构成多种条件
- 断言可以分为立即断言（条件表达式）和并发断言（连续运行，整个仿真中都在运行，基于时钟周期，用于描述一个跨时钟周期的行为）
//立即断言：类似if语句
immediately_assert:assert(expression)
$display("passed");
else $error("failed");
//并发断言：property…endproperty描述事件
property p_event;
@(posedge clk) disable iff(rst);//clk上升沿断言开始，屏蔽rst高电平时的情况，
$isunknown(request) == 0; //检查request是否为0状态
endproperty
concurrent_assertion:assert property(p_event);//assert启动断言检查
三、SVA使用
3.1 SVA位置
在一个.v文件中
module ABC ();
rtl 代码;
SVA 断言;
endmodule
3.2 SVA格式
- sequence和property可以理解为定义一个函数，assert时调用这个函数，调用方式为
name : assert property(name2)（只有property这种调用方式） - 两种格式分别为
sequence块：用于定义一个事件（砖），一般用于定义组合逻辑断言
property块：用于将事件组织起来，形成更复杂的一个过程，一般用来定义一个有时间观念的断言，它会常常调用sequence。
sequence块的内容不能为空；sequence也可以包含另一个sequence - 写断言的一般规则是： time + event，要断定发生什么event，首先要指定发生event的时间，例如:
每个时钟上升沿 + 发生某事；某信号下降时 + 发生某事
sequence
...
end sequence
property
...
endproperty
assert property(事件2)
$display("........",$time);
else
$display("........",$time);
四、基本语法
4.1 信号（或事件）间的“组合逻辑”关系
(1) 常见的有：&&, ||, !, ^
(2) a和b哪个成立都行，但如果都成立，就认为是a成立：firstmatch(a||b)，与“||”基本相同，不同点是当a和b都成立时，认为a成立。
(3) a ? b:c ———— a事件成功后，触发b，a不成功则触发c
4.2 “时序逻辑”中判断独立的一个信号的行为
@ (posedge clk) A事件; ———— 当clk上升沿时，如果发生A事件，断言将报警。
边沿触发内置函数：(假设存在一个信号a)
$rose( a );———— 信号上升
$fell( a );———— 信号下降
$stable( a );———— 信号值不变
4.3 “时序逻辑”中判断多个事件/信号的行为
(1) intersect(a,b)———— 断定a和b两个事件同时产生，且同时结束。
(2) a within b ———— 断定b事件发生的时间段里包含a事件发生的时间段。
(3) a ##2 b ———— 断定a事件发生后2个单位时间内b事件一定会发生。
a ##[1:3] b ———— 断定a事件发生后1~3个单位时间内b事件一定会发生。
a ##[3:$] b ———— 断定a事件发生后3个周期时间后b事件一定会发生。
(4) c throughout (a ##2 b) ———— 断定在a事件成立到b事件成立的过程中，c事件“一直”成立。
(5) @ (posedge clk) a |-> b ———— 断定clk上升沿后，a事件“开始发生”，同时，b事件开始发生。
(6) @ (posedge clk) a.end |-> b ———— 断定clk上升沿后，a事件执行了一段时间“结束”后，同时，b事件开始发生。
一旦 a 发生，b 必须发生，断言才成功。如果a没发生，走else，同样成功。
(7) @ (posedge clk) a |=> b ———— 断定clk上升沿后，a事件开始发生，下一个时钟沿后，b事件开始发生。
(8) @ (posedge clk) a |=>##2b ———— 断定clk上升沿后，a事件开始发生，下三个时钟沿后，b事件开始发生。
(9) @ (posedge clk) $past(a,2) == 1'b1 ———— 断定a信号在2个时钟周期“以前”，其电平值是1。
(10) @ (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];
//当clk上升沿时，断言开始。首先断定信号a由低变高，将此时的信号b的值赋给变量tmp，4个时钟周期后，断定信号c的值是4个周期前b^2+1，再过3个周期，断定信号d一定会起来，再过3个周期，信号d又起来一次。。。。。。。只有这些断定都成功，该句断言成功。otherwise，信号a从一开始就没起来，则断言也成功。
endproperty
4.4 多时钟域联合断言：一句断言可以表示多个时钟域的信号关系
@ （posedge clk1） a |-> ##1 @ (posedge clk2) b
当clk1上升沿时，事件a发生，紧接着如果过来第二个时钟clk2的上升沿，则b发生。
“##1”在跨时钟时不表示一个时钟周期，只表示等待最近的一个跨时钟事件。
所以此处不能写成##2或其他。但是可以写成：
@ （posedge clk1） a |=> @ (posedge clk2) b
4.5 总线的断言函数
总线就是好多根bit线，共同表示一个数。SVA提供了多bit状态一起判断的函数，即总线断言函数：
(1) $onehot(BUS) ————BUS中有且仅有1 bit是高，其他是低。
(2) $onehot0(BUS) ————BUS中有不超过1 bit是高，也允许全0。
(3) $isunknown(BUS) ————BUS中存在高阻态或未知态。
(4) countones(BUS)==n ————BUS中有且仅有n bits是高，其他是低。
4.6 屏蔽不定态
当信号被断言时，如果信号是未复位的不定态，不管怎么断言，都会报告：“断言失败”，为了在不定态不报告问题，在断言时可以屏蔽。
如： @(posedge clk) (q == $past(d))，当未复位时报错，屏蔽方法是将该句改写为：
@(posedge clk) disable iff (!rst_n) (q == $past(d)) //rst是低电平，关闭属性检查
not： 表示not后的序列不能出现
4.7 断言覆盖率检测：
name: cover property (func_name)
4.8 循环
for(){…}的功能，别忘了语法中介绍的[*3]，这是在断言中实现for的唯一方式。
##4 (read==read, cnt = 0, arr[cnt] = DataIn, cnt++) //初始化一下，
##1 (read==read, arr[cnt] = DataIn, cnt++)[*3] //循环3次
property p;
@(posedge clk) a |-> ##1 b ##1 b ##1 b;
endproperty
a: assert property(p);
property p;
@(posedge clk) a |-> ##1 b[*3];//等价，重复三次
endproperty
a: assert property(p);
property p;
@(posedge clk) a |-> ##1 b[->3] ##1 c;
endproperty
a: assert property(p);
//其中##1 b[->3]表示在a为高的上升沿后，经过一个周期，b在接下来要有三个上升沿为高，而且不一定要连续。(可以不连续)
//但有个要求，就是在##1 c发生之前的上升沿b是刚好完成最后一次匹配
//如果改为：b[=3]，就是非连续重复，区别是，不要求b的最后一次匹配发生在c发生之前。也就是b完成了三次匹配后，可以等若干周期c才发生
五、仿真软件中加入断言编译和显示功能
5.1 在modelsim中开启断言编译和显示功能
（1）【编译verilog代码时按照system verilog进行编译】 vlog -sv abc.v
（2）【仿真命令加一个-assertdebug】 vsim -assertdebug -novopt testbench
（3）【如果想看断言成功与否的分析，使用打开断言窗口的命令】 view assertions
5.2 在VCS中加入断言编译和显示功能
在fsdb文件中加一句话：$fsdbDumpSVA
在VCS编译参数：system "vcs $VCS_SIMULATION" 中加入一些options:
-assert enable_diag\
-assert vpiSeqBeginTime\
-assert vpiSeqFail\
-assert report=路径\
-assert finish_maxfail=100
六、练习
b<=a逻辑的断言
@ (posedge clk) (a==a,tmp=a) |=> (b==tmp);每句断言都是一个小程序：如上例，在##4时间点上，(read==read, cnt = 0, arr[cnt] = DataIn, cnt++)就是一个小程序，信号断言必须是第一句，其他运算按照顺序进行。
断言的变量除了可用C语言中的int，float外，还可以是reg [n:0]等数字电路类型。
写了|->，就不能再用 && 等事件组合逻辑
property ept_p;
@(posedge rd_clk) ((rd_num == 0) |-> rd_ept)
&& (rd_ept |-> (rd_num == 0));
endproperty
//是错误的
//解决方法是使用2个断言，没更好的方法。
property ept_p1;
@(posedge rd_clk) (rd_num == 0) |-> rd_ept);
endproperty
property ept_p2;
@(posedge rd_clk) rd_ept |-> (rd_num == 0);
endproperty
- a为高时，b为高
property p1
@(posedge clk) a |-> b;
endproperty
ast_1:assert property(p1)
- c为高时，下一个周期d为高
property p2
@(posedge clk) c |=> d;
endproperty
ast_2:assert property(p2)
- e为高时，下1-10个周期内f为高
property p3
@(posedge clk) e ##[1:10] f;
endproperty
ast_3:assert property(p3)
- a1和a2的检查效果完全一样
property p1:
@(posedge clk) a|=>b|=>c;
endproperty
a1: assert property(p1);
property p2:
@(posedge clk)a ##1 b ##1|-> c;
endproperty
a2: assert property(p2);
- 在时钟上升沿时采样到start有效开始，两个时钟周期后，信号“a”连续或者间断地出现3次为高电平，紧接着信号"stop"在下一个时钟周期为高电平，转换成断言描述
property p0: @(posedge clk)
$rose(start) 1->##2 (a[->3])##1 stop:
endproperty
a0 : assert property(p0).