终于来到了断言了，嘿嘿。
assertion分为两种，立刻和并行，立刻断言其实跟普通的$display没什么不同。重点在并行断言。
（一）首先的概念是concurrent assertion的构成：sequence->property->assert
sequence 就是简单的需要判断的语句，sequence里面常用的方式：|-> |=>，前者是前面一个语句正确之后，立刻判断后面的语句，|=>则是过一个周期之后再判断后面的语句，当然也可以用##来指定具体需要间隔多少周期
对property和assert不妨这么看，property其实就是一个函数，只不过这个函数里面调用的都是sequence和其它property，而assert其实就是调用这个函数的语句。
关于property有下面一些比较细碎的知识点值得指出来:
1.就像一个函数，property里面可以调用其它property，并且可以用if else等简单语句来组织不同property之间的关系。一个property里面可以调用其它task function
2.DUT里面也是可以用assertion的
3.property里面对结果的取反用not而不是~
（二）
sv为了让assertion这个工具好用，提供了一些很好的简单语句。
rose fell stable sample就是字面意思，很好理解的，下面这个图讲得很清楚了，它们存在的意义就在于是对电平敏感的普通sequence表达的一种补充。
past（，n）指的是判断在目前这个时钟沿前面n个周期的时钟沿的情况
and or很好理解，但他们只要求sequence正确就完事了，而intersect则是在and的基础上，还要求俩sequence的结束时间也要一致，不然就报错。由此可以联想一下，如果我们要指定两个sequence的结束时间差出去某个周期该怎么半呢，也好办，只要在某一个sequence后面加上##n 1就可以了。所以过一个简单intersect实际上是彻底实现了对两个sequence结束时间的各种约束。
（三）其它的一些细节点
$的用法
within的用法
(1)assert 简单例子
module concurrent_assertion(
input wire clk,req,reset,
output reg gnt);
//=================================================
// Sequence Layer
//=================================================
sequence req_gnt_seq;
// (~req & gnt) and (~req & ~gnt) is Boolean Layer
(~req & gnt) ##1 (~req & ~gnt);
endsequence
//=================================================
// Property Specification Layer
//=================================================
property req_gnt_prop;
@ (posedge clk)
disable iff (reset)
req |-> req_gnt_seq;
endproperty
//=================================================
// Assertion Directive Layer
//=================================================
req_gnt_assert : assert property (req_gnt_prop)
else
$display("@%0dns Assertion Failed", $time);
//=================================================
// Actual DUT RTL
//=================================================
always @ (posedge clk)
gnt <= req;
endmodule
//+++++++++++++++++++++++++++++++++++++++++++++++
// Testbench Code
//+++++++++++++++++++++++++++++++++++++++++++++++
module concurrent_assertion_tb();
reg clk = 0;
reg reset, req = 0;
wire gnt;
always #3 clk ++;
initial begin
reset <= 1;
#20 reset <= 0;
// Make the assertion pass
#100 @ (posedge clk) req <= 1;
@ (posedge clk) req <= 0;
// Make the assertion fail
#100 @ (posedge clk) req <= 1;
repeat (5) @ (posedge clk);
req <= 0;
#10 $finish;
end
concurrent_assertion dut (clk,req,reset,gnt);
endmodule结果
Chronologic VCS simulator copyright 1991-2019
Contains Synopsys proprietary information.
Compiler version P-2019.06-1; Runtime version P-2019.06-1; Feb 22 08:42 2020
"testbench.sv", 25: concurrent_assertion_tb.dut.req_gnt_assert: started at 129ns failed at 129ns
Offending '((~req) & gnt)'
@129ns Assertion Failed
"testbench.sv", 25: concurrent_assertion_tb.dut.req_gnt_assert: started at 237ns failed at 237ns
Offending '((~req) & gnt)'
@237ns Assertion Failed
"testbench.sv", 25: concurrent_assertion_tb.dut.req_gnt_assert: started at 243ns failed at 243ns
Offending '((~req) & gnt)'
@243ns Assertion Failed
"testbench.sv", 25: concurrent_assertion_tb.dut.req_gnt_assert: started at 249ns failed at 249ns
Offending '((~req) & gnt)'
@249ns Assertion Failed
"testbench.sv", 25: concurrent_assertion_tb.dut.req_gnt_assert: started at 255ns failed at 255ns
Offending '((~req) & gnt)'
@255ns Assertion Failed
"testbench.sv", 25: concurrent_assertion_tb.dut.req_gnt_assert: started at 261ns failed at 261ns
Offending '((~req) & gnt)'
@261ns Assertion Failed
$finish called from file "testbench.sv", line 57.
$finish at simulation time 271
V C S S i m u l a t i o n R e p o r t
Time: 271 ns（2）
module system_assertion();
logic clk = 0;
always #1 clk ++;
logic req,gnt;
//-------------------------------------------------
// Property Specification Layer
//-------------------------------------------------
property system_prop;
@ (posedge clk)
($rose(req) && $past(!req,1)) |=>
($rose(gnt) && $past(!gnt,1));
endproperty
//-------------------------------------------------
// Assertion Directive Layer
//-------------------------------------------------
system_assert : assert property (system_prop);
//-------------------------------------------------
// Generate input vectors
//-------------------------------------------------
initial begin
req <= 0;gnt <= 0;
repeat(10) @ (posedge clk);
req <= 1;
@( posedge clk);
gnt <= 1;
req <= 0;
@( posedge clk);
// Make the assertion fail now
req <= 0;gnt <= 0;
repeat(10) @ (posedge clk);
req <= 1;
@( posedge clk);
req <= 0;
gnt <= 0;
// Terminate the sim
#30 $finish;
end
endmodule结果
Compiler version P-2019.06-1; Runtime version P-2019.06-1; Feb 22 08:54 2020
"testbench.sv", 18: system_assertion.system_assert: started at 45ns failed at 47ns
Offending '($rose(gnt) && $past((!gnt), 1))'
$finish called from file "testbench.sv", line 38.
$finish at simulation time 75
V C S S i m u l a t i o n R e p o r t
Time: 75 ns