0.注意

在sequence序列、property属性和断言语句中都可以触发事件，但是建议在property中定义；

1.作用

可以进行时序检查和覆盖率统计。

2.分类

即时断言：执行到程序块，立即执行断言，可以结合信息打印机制进行使用；
并发断言：在整个仿真过程中，都会连续地检查信号。

3.断言的语法

//含bool表达式的sequence
sequence sequence名字;
	bool表达式;
endsequence
//含sequence的property
property 名字;
	@(敏感事件列表)   sequence；
endproperty
//含property的断言语句
断言的名字: 断言关键字(assert/cover/assume) property(property名字)；
   断言执行结果；
else
   不满足断言执行结果；

4.基本组成

sequnce序列：表示事件；
property属性：仿真过程中被验证的单元；
实例化property的关键字：
assert：时序检查，要求在整个验证场景中必须为真；
cover：覆盖断言，在整个验证场景中必须出现过；
assume：约束断言，一般用来规范电路的输入激励；

5.实现断言

bool表达式构成sequence序列；
sequence序列构成property属性；
使用属性进行断言；

6.常见断言方法

A 运算符
a 说明:（过于简单的断言可以不用sequence序列）
直接使用运算符；
b 语法:
直接使用运算符；
c 例子：


B 内建方法
a 说明
使用systemverilog内建的方法进行断言；
b 语法：
$rose(expression or signal)
当表达式/信号由0变为1时，返回真；
$fell(expression or signal)
当表达式/信号由0变成1时，返回真；
$stable(expression or signal)
当表达式/信号不变时，返回真。
$past(signal，pad)
检查信号前几拍；
例子1：


例子2：


例子3：


C 参数化
说明:
sequence序列和property都可以传参；
语法：
sequence sequence名字(参数列表)；
bool表达式;
endsequence
property property名字(参数列表)；
sequence序列或bool表达式;
endproperty
例子：


D 延时
说明：当先行算子满足后，延时拍数，后续算子需满足；
语法：先行算子 ##延时拍数 后续算子；
注意：拍数表示延迟的周期数，而不是时间单位；
例子：


说明:上图波形不能反映断言结果，截出断言列表；

D1 延时1
说明：当先行算子满足后，延时拍数区间，后续算子在延时区间满足其中一个时刻即可；
语法：先行算子 ##延时拍数区间 后续算子；
注意：拍数表示延迟的周期数，而不是时间单位；
例子：


E 交叠蕴含
说明：当先行算子满足时，在同一周期，计算后续算子的表达式；
当先行算子不满足时，会显示空成功；
语法：先行算子 |-> 后续算子；
代码：

结果：

F 非交叠蕴含
语法：先行算子 |=> 后续算子；
说明：当先行算子满足时，在下一周期，计算后续算子的表达式；
当先行算子不满足时，会显示空成功；
代码：

结果：

注意：断言结果为后续算子满足时显示；
G sequence序列的拼接（ended没有考虑）
说明：
序列可以按照起点进行拼接，前面序列断言后，继续断言后续序列，同时满足断言成功；
起点拼接，直接用断言符号；
例子：


H 连续重复跟随运算符
说明：信号或序列连续多拍满足，且次算子判定必须紧跟前序算子和后续算子。
语法:signal or sequence [*n]
例子:


I 非连续重复跟随运算符
说明：信号或序列连续或间断满足要求，且信号或序列必须紧跟前序算子和后续算子；
语法：信号或序列[->次数]
例子：


j 非连续重复非跟随重复运算符
说明:信号或序列连续或间断满足要求，且信号或序列必须紧跟前序算子和后续算子；
语法:信号或sequence序列[=n] 后续断言；
例子：


注意1：会重复检测。
注意2：三个重复算子的区别：
a重复序列的构造

	前序算子   重复算子   后续算子；
	//前序算子和后续算子不是必须项；

b重复序列的特性
连续性：重复算子必须紧跟前序算子执行，且必须连续满足重复算子（[*3]即为三个连续的高电平）；
跟随性：后续算子必须紧跟重复算子执行；
c 三个重复算子满足的特性

表	连续性	跟随性
[*n]	√	√
[->n]	×	√
[=n]	×	×

k and构造
说明:
可以并列组合两个序列，两个序列都成功时，整个属性成功；
两个sequence序列起点要相同，终点可以不同；
检验的起始点是两个sequnce序列检验的起始点，检验的终点是后结束sequence序列检验的终点；
语法:
序列1 and 序列2；
例子：

结果：


注意：两个sequence序列起始点必须相同，当起始点不同时，后一个sesquence序列的起始点也可作为前一个sequence序列的起始点时，可以将后一个序列的起始点作为总的起始点；
例子：



l intersect构造
说明:
可以并列组合两个sequnce序列，两个sequence序列都成功时，property属性才成功；
两个sequence序列必须同时开始和同时结束，即需要有相同的长度；
例子1：起点和终点都不同，and和intersect都断言失败；


例子2：起点相同和终点不同，and断言成功intersect断言失败；


例子3：起点和终点都相同，and和intersect都断言成功；



m or构造
说明：
可以并列组合两个sequence序列，只要有一个序列成功，property属性就成功；
n first_match构造(没跑通例子，例子和理论违背)
说明:当序列由多个并行序列通过通过逻辑运算符进行组合（and /or等），会出现一次检测有多个匹配的结果，使用first_match够着只会用第一次序列匹配；
语法:first_match(sequence序列或信号);
例子：

说明：
序列：

	a ##[1:2] b

等价于由两个序列通过or运算符进行组合：

	（a ##1 b） or（a ## 2 b）

所以，一般会将所有序列检查完，才会检查后续序列；
当使用first_match构造后，多个并行序列检查到第一次满足后，立刻执行后续序列：

	first_match (a ##[1:2] b)

o throughout构造
说明：bool表达式，在整个后续序列过程中，为高电平；
语法:（bool表达式） throughout 后续sequence序列；
例子:


说明:
在50到90时刻，断言失败，因为前提条件a为低；
90到130时刻，断言失败，因为前提a并没有在整个过程中满足；
130到170时刻，断言成功，因为前提a在整个过程中满足后续表达式也满足。
p within构造
说明:后续序列发生的时间段，包含前面序列发生的时间段；
即，后续序列必须先于 先行序列开始，后续序列必须后于 先行序列结束；
语法:先行序列 within 后续序列；
例子：


q 局部变量
说明：sequence序列和property属性内都可以定义局部变量，局部变量可以赋值，紧接着子程序放置用逗号隔开；
语法：

局部变量声明；
bool表达式，局部变量赋值；

例子：APB协议中的断言；

r 例子
a 例1

说明:
先行算子:a和b同时为高；
后续算子:在1到3拍内，c至少在一个时钟周期内为高；
结果：

b 例子2

说明:
先行算子: a为高；
后续算子:在一拍以后，b存在高电平；
b为高，同时及以后，c存在高电平；

7.APB的断言

7.1APB的时序

（1）写操作时序

（3）读操作时序

7.2 断言的检查

（1）公共断言
A PSEL信号拉高，APBADDR信号不应该为X；
使用的断言：交叠蕴含和$unknown内建方法；
代码：

结果:

B PSEL信号拉高，下一个周期PENABLE信号也应该拉高；
使用的断言：$rose内建方法和非交叠蕴含；
代码：

结果：

C PENABLE信号拉高，下一个周期PENABLE信号应该拉低；
使用的断言： $rose(), $fell()内建方法和非交叠覆盖；
代码:

结果:

D在下一次传输前，PADDR和PWRITE信号应该保持不变；
使用的断言：$rose(),局部参数，##1,[=1],基本运算符，$past(),，first_match,|->
例子：

代码分析：
a 用$rose内建方法判定PENABLE信号的上升沿前一次传输过程的开始,并记录地址；
b用延时(##1)和基本运算符和非连续重复非跟随运算符判定下一次传输的开始，并用$past记录地址；
c用first_match结构只检查第一次满足要求的结果；
d用交叠蕴含（|->）判定地址的一致性；
（2）写模式断言
说明：无论是在读还是写数据模式，依次数据传输过程中，写数据线（PWDATA）保持不变；
代码：

结果：

7.4 断言覆盖率的统计

（1）非连续写操作
说明：进行一次写操作，空缺一拍，再进行下一次写操作；
时序如下图：

代码：

说明：
a PSEL为高且PENABLE为低，判定一次传输的开始；
b 通过交叠蕴含（|->）和througout结构要求从此刻开始到下一次传输结束，PWRITE保持为高；
c 通过延迟结构（##）、连续重复跟随结构、非连续重复非跟随结构，要求下一拍PENABLE为高、PENABLE连续两拍低、PENABLE在后一次传输结束前为高一拍；
结果：

（2）连续写
说明：前一次写完，立刻写第二次
时序：

代码：

代码说明：
a PSEL为高且PENABLE为低，判定一次传输的开始；
b 通过交叠蕴含（|->）和througout结构要求从此刻开始到下一次传输结束，PWRITE保持为高；
c 通过延迟结构（##）、要求下一拍PENABLE为高、再下一拍PENABLE为低、再下一拍PENABLE在后一次传输结束前为高一拍；
结果：

…未完待续