SVA描述(一)
SVA简述
SystemVerilog Assertion(SVA):是一种描述性的语言，可以很容易的描述时序相关的情况，所以主要用在协议检查和协议覆盖。SVA在systemverilog仿真器中的
调度区间在RTL之后，Testbench之前。所以同一时钟断言只能采样到上一时刻的RTL值。由于是描述性语句，所以“;”用的比较多。
断言失败后会自动打印信息到log文件，用户也可以自定义打印内容。
assertion name： assert xxxx
$display(“xxxxx”);
else
$display(“xxxxx”);
SVA分为并发断言：基于时钟的，调度区间按assertion的调度区间，可以在过程块(always initial),模块(module),接口(interface),程序(program)中定义。
即时断言：基于事件的，本质不是时序关系，会立刻求值。进行检查。只能在过程块(always initial)中定义。
两者另一个区别是：并发断言会用property来声明，即时断言不需要。
always
begin
a_ia: assert (a && b); //即时断言
end
因为并发断言应用更多，所以一下均以并发断言来说：
并发断言可以自定义一个SVA块来描述自己要求的时序，两个关键字：sequence, property。
sequence s1; //sequence允许自己定义更小的时钟描述
a ##2 b;
endsequence
property s2; //property 一个assert只能有一个
@(posedg clk) s1;
endproperty
s3 ：assert property(s2); //标准形式 name : assert property();
断言中内嵌的表示信号的上升沿和下降沿的函数：$rose(expression or signal) $fell(expression or signal) $stable(expression or signal) $changed(expression)
sequence s2;
@(posedge clk) $rose(a); //时钟的上升沿仍然用posedge, 信号的上升沿才用$rose();
endsequence
断言中时序延时的描述： ##表示延时，但是注意触发加.ended，否则SVA默认都是按起始时刻来对齐的，也就是说如果断言3时刻触发，5时刻succeed，但是断言
也是会报道3时刻的对错。
sequence s2;
@(posedge clk) a ##2 b; //a为高电平延时2个时钟后如果b为高电平，则断言成功。
endsequence
property p12;
@(posedge clk) (a && b) |-> ##[1:3] c; //相当于(a && b) |-> ##1 c; 或 (a && b) |-> ##2 c; (a && b) |-> ##3 c;
endproperty
断言中时钟的定义：一般情况下，在property中定义时钟，而保证sequence独立于时钟比较好。当然从语法角度来说，时钟可以定义在property,sequence,assert
中。但是当assert定义时钟之后，property不能再重新定义时钟。
sequence s5a;
a ##2 b;
endsequence
property p5a;
@(posedge clk) s5a; //在property中定义时钟
endproperty
a5a: assert property(p5a); //assert不再定义时钟
断言通过蕴含操作符来作为断言的触发条件，交叠蕴含： “|->”来表示，表示在先行算子(蕴含前的表达式)有效的同一个时刻判断后续算子(蕴含后的表达式)。
非交叠蕴含： “|=>”来表示，表示在先行算子有效的下一时刻再判断后续算子。
property p8; property p9;
@(posedge clk) a |-> b; //同一时刻 @(posedge clk) a |=> b; //延时一个时钟
endproperty endproperty
##m延时m个clock：
[*n]重复n次：
assert property (@posedge clk) rst[*2]; end property //最开始的clock连续重复两个cycle rst
[=m]重复m次，不要求连续
[->m]重复m次，与[=m]的主要区别是，在后边加延时##1时，[=m]不准确表示延时1个clock
[->m]表示准确延时1个clock
sig1 throughout seq：throughout之前表示一个expression，之后表示一个sequence，在sequence期间，expression一直有效。
seq1 within seq2：within前后都表示sequence，在后一sequence有效期间，sequence1必须一直有效。
seq1 and seq2：两个sequence进行与运算，两个sequence必须同时start，但是不要求同时结束。
seq1 or seq2：两个sequence进行或运算，只要有一个sequence有效，该语句有效。
seq1 intersect seq2，两个seq必须完全同时开始，同时结束，同时有效。
not seq1：表示对seq的结果取反
if(expression) seq1 else seq2：if—else语句控制，但是好像不能用在local var的场景中。
sva提供的system task：
1)$onehot(expression)，在expression中只有一个1或者没有1时，表示结果正确
2)$isunknown(expression)，在expression中包含x、z时，表示结果正确
3)$countones(expression)，返回expression中1的个数， ones=$countones(busgnt)
4)$assertoff(level, list of module) $asserton $assertkill
sva中可以定义local var，
赋值与比较，前都必须有一个sequence，或者显示指明1’b1
sequence rdc;
##[1:5] rdDone;
endsequence
sequence datacheck;
int local_data;
(rdc, local_data = rData) ##5 (wData == (local_data + \’hff));
endseqence
baseP：assert property (@(posedge clk) RdWr |-> dataCheck) else gotoFail;
sequence s1;
int x;
((1\’b1, x = data) ##0 ((a ##1 b) or (d ##1 e) ) ##1 (data1 == x+1);
endsequence
延时中不可以使用参数，变量定义时，不能用参数，因为变量在elabration时，需要使用
property checkDelay;
int lv;
(readReq, lv=dataDelay) |=> ##[0:lv] readData; （错误）
endproperty
endsequence