一：初实assertion
断言就是一段描述设计期望行为的代码。 目前， 对断言的使用主要在于仿真， 但断言的能力不仅仅如此。 断言是基于一些更加基础的信息， 我们称之为属性 （ Ｐｒｏｐｅｒｔｙ）， 属性可以用来作为断言、 功能覆盖点、 形式检查和约束随机激励生成。
断言可以嵌入到设计当中， 也可以在设计以外通过绑定链接到不同的设计点中。 断言查找期望的特定事件序列， 或者说是在特定时钟周期内的事件。 这些操作其实可以通过一个状态机来实现， 设计工程师也可以通过硬件设计语言来实现， 但是这种方法不利实现，难以调试和维护。 因此， 为了提高断言 的 效 率， 针 对 断 言 描 述 的 标 准 语 言 （ 如 ＰＳＬ 和ＳＶＡ）， 被用户广泛采用。
断言有一个重要的作用就是可以提高对设计的可见度。 它能够帮助定位错误的根源， 以保证调试能更加容易和快速地进行。 这是因为断言可以分布在设计
的各个重要部位， 能及时捕捉与设计属性不一致的行为。 断言可以应用在白盒调试或者黑盒调试两种方式中， 一般情况下， 白盒调试会被设计工程师采用， 而黑盒调试会与验证工程师比较相关。
那么， 我们有哪些方式可以支持断言呢？ 第一， 我们可以采用预建的断言库， 如 ＯＶＬ； 第二， 用户可以自定义断言， 例如采用 ＳＶＡ 或者 ＰＳＬ。 在此， 我们优先推荐采用断言库， 而不建议用 户学习断言详尽的语法， 从而自定义断言。 为什么呢？
１） ＳＶＡ 和 ＰＳＬ 虽然是专门提供给用户定义断言的编程语言， 其优点是语法简练； 其缺点是在简练的语法下全面地表达特定的、 复杂的电路行为， 对语法或者电路行为理解不深刻的人， 很难写出比较有实用价值的断言。
２） 断言是设计属性的表现， 也就是采用 ＳＶＡ 和 ＰＳＬ 表示出来的是设计的意图， 这就存在证明断言代码是否正确的过程； 断言没有办法自我证明， 那么只能通过检视 （ ｒｅｖｉｅｗ）和设计仿真过程中的相互验证， 也就是在这个调试过程中， 可能是设计上的错误， 也可能是断言写错了， 或许你大部分的时间不是在调试设计， 而是在调试断言本身。
３） 验证对于调试周期有很高的要求， 为了缩短验证周期， 首先， 我们需要能更快地暴露错误的行为， 这个可以通过随机激励生成， 通过大量的随机数据测试尽可能多地设计空间； 其次， 在错误暴露的时候， 我们如何定位到这个错误， 断言就是在这个阶段起作用，若我们能够采用已经被验证过的断言库， 我们就可以遵从验证重用的思想， 做到实实在在的提高验证效率。
综上所述， 为了缩短调试周期， 我们要有采用断言的思想， 而不是陷入在长篇累牍的断言语法中。简单来说，assertion用于更容易地debug
二：SVA的语法层次结构
1：最底层是布尔表达式， 这个和 verilog中没有差别；
2：第二层是序列 （ ｓｅｑｕｅｎｃｅ）， 其中可以包含一些新的操作符， 如＃＃时隙延迟、 重复操作符、 序列操作符等， 序列是一个封装格式， 采用序列封装后可以在不同地方使用， 一个序列会被评估为真或者假；
3：第三层是属性 （ ｐｒｏｐｅｒｔｙ）， 这是重要的封装方式，其中最 重 要 的 特 点 是 属 性 内 部 可 以 定 义 蕴 涵 操 作 符（ ｜ －＞ 、 ｜ ＝＞ ）。
4: 第四层是断言指示层， 也就是采用 ａｓｓｅｒｔ对特定属性或者序列做行为检查， 或者采用assum或者采用 ｃｏｖｅｒ 做统计等。
5: 第五层是断言的最后封装， 只有通过最后封装成一个单元的断言才可以在不同的地方重用， 就如同一个可以例化模块或者类， 通常这一层可以通过 ｍｏｄｕｌｅ 或者ｐｒｏｇｒａｍ、 ｉｎｔｅｒｆａｃｅ 来封装
SVA包含两种Assertion：立即断言（Immediate Assertion），没有任何时序概念的断言为立即断言，主要用于组合逻辑电路中。可调用$error,$fatal等
并行断言（Concurrent Assertion），是基于周期采样的，可跨时钟周期的。我们下面主要介绍并行断言
三：assertion里的重要名词
1：SVA：SystemVerilog Assertion
2：ABV: Assertion Based Verification
3：CDV:Coverage Driving Verification
四：关键字
1：property：验证设计意图，内部可包含sequence
2：sequence：将一个序列做出来，包含很多场景，比如reset等
3：thread：事件相关的一个序列，可持续一拍或者多拍，每个thrad相互独立。SVA在每个时钟间隙进行asssert/assume/covered
4：##n
延迟n个周期
5：[m:n] /##[m:n]
[m:n] : m-n的任意一个周期
##[m:n] : ##m - ##n的任意一个周期
6：|->
首先对前置表达式做检查，不成立则不激发后置表达式；成立，在同一个时钟周期检查后置表达式是否满足要求。用于property
7：|=>
首先对前置表达式做检查，不成立则不激发后置表达式；成立，在下一个时钟周期检查后置表达式是否满足要求。用于property
|=>表示要延迟一个周期，相当于 |->##1
五：property
1：初识
可使用assert，assume，cover进行check；
可定义在module，interface，clocking block，package里；
2：格式举例
property对设计进行描述，用assert进行check
波形
在clk上升沿，check信号request为1时（图中标注request的T1处），clk的下一个周期处，check信号acknowledge是否拉高（图中标注acknowledge的T1处），可知拉高，在clk的再下一个周期处，同理check信号data_enable是否拉高...可知T1成功，T2失败。
3：assert/assume/cover
assert: check rtl
assume: check testbench
cover: coverage统计
如果a=2，disable 这个property，否则，执行 not @clk(b ##1 c);
4: implication (|-> |=>)
5: define
可对已经定义过的property进行define宏定义操作 ，再次使用时较为简便。 ？？可是直接使用property的名字不是也可以吗？
6：可使用not，or，and操作，可含有if else
7：可包含property，sequence，可递归
8：用于多时钟
这里的##1是指当sig0=1时，clk0的下一拍后的clk1的上升沿
但是在跨时钟时，当前拍只能操作一个时钟，即一个thread里只能操作一个时钟，如下
在clk0时钟范围内，当前拍又对clk1操作，这是不合法的操作。
六：sequence
1：初识
提供描述时序的一种方式，主要是线性顺序；sequence内可嵌套sequence
2：例子
波形
3：sequence的其它关键字
##[0:$] : 0个周期到最后一个周期
[*n] : 续n次；例如：b[*3:4] 连续三次或者四次
[->n] : goto，连续重复 ； 例如
，b先拉低一拍，再拉高一拍,2次；再如：b[->2:10] b先拉第一拍，再拉高一拍，2次-10次皆可
[=n] :非连续重复；例如
，b先拉低一拍，再拉高一拍，重复两次，最后以拉低结尾
$sample ：采样值
$rose : 采下降沿
$fell : 采下降沿
$satble : 表达式没变，返回1，改变，返回0；
$past : 采过去的前一个周期的值
and /intersect ：相当于与操作，但两者有区别
or ：或操作
4：sequence函数
（1）first_match(t2) :第一次成功匹配t2
（2）throughout
横跨多个周期，前置值都要满足
主要块要重复七拍，而burst_mode在拉低后的第六拍后即拉高，所以不满足，fail。
（3）ended
在rule里，e1.ended先执行e1的末尾语句，##1 proc2，然后依次向前执行