标签：
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)
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
标签：
原文地址：http://www.cnblogs.com/-9-8/p/4433267.html
