本文部分内容是来自SV LRM书的翻译。
断言是设计的属性的描述。
● 如果一个在模拟中被检查的属性(property)不像我们期望的那样表现，那么这个断言失败。
● 如果一个被禁止在设计中出现的属性在模拟过程中发生，那么这个断言失败。
SVA 是一种描述性语言，可以完美地描述时序相关的状况。语言的描述性本质提供了对时间卓越的控制。语言本身非常精确且易于维护。SVA 也提供了若干个内嵌函数来测试特定的设计情况，并且提供了一些构造来自动收集功能覆盖数据。
关于系统的论述，我后面应该会写文章更新，今天主要讲讲几个比较容易疑惑的地方。
- 无限的时序窗口
在时序窗口的窗口上限可以用符号“$”定义，这表明时序没有上限。这叫“可能性”(eventuality)运算符。检验器不停地检查表达式是否成功直到模拟结束。因为会对模拟的性能产生巨大的负面影响，所以这不是编写SVA 的一个高效的方式。最好总是使用有限的时序窗口上限。
那么问题来了，我们是捕捉到一次成功断言就结束了呢？还是得一直捕捉下去？永不结束？
首先看个例子：
发现仿真时只会捕捉到一次断言成功就结束了，截图如下：
还是同样的，那我如果是多添加一个事件，并且采用$符号呢？
例子如下：
通过仿真，可以看出，每次都是在最一次匹配后就进入了下一阶段。
- and 构造
可以用来逻辑地组合两个序列。当两个序列都成功时整个属性才成功。两个序列必须具有相同的起始点，但是可以有不同的结束点。检验的起始点是第一个序列的成功时的起始点，而检验的结束点是使得属性最终成功的另一个序列成功时的点。
看个例子
仿真结果如下：
这个好像很容易理解，如果同样的波形，换成intersect呢？
- intersect 构造
例子如下：
主要注意点有两个，一个是intersect不支持直接的写法，如上图中and的写法，在intersect中是报error的，二是蕴含运算符不能在sequence中使用。
仿真结果如下：在90ns时，and是成功的，intersect是失败的。
两个序列必须在相同时刻开始且结束于同一时刻。换句话说，两个序列的长度必须相等。
or构造就不讲了，很简单，二选一成立即可。
- first_match 构造
开始比较难理解的是first_match构造，这个在语言手册上也有一个例子，例子如下：
我试着仿了一下，然后发现，加没加first_match的结果是一样一样的...
代码如下：
在代码中添加了first_match和没添加做比较：
仿真结果一模一样...
不是说first_match没用。只能说指导手册LRM提供的案例是不适合这种情况的...
前面特意提到$运算符，是因为这儿是有个大新闻的，就是蕴含运算和$放在一起就不得了...
蕴含等效于一个if-then 结构。蕴含的左边叫作“先行算子”(antecedent)，右边叫作“后续算子”(consequent)。先行算子是约束条件。当先行算子成功时，后续算子才会被计算。
我们来看点能起作用的~
前面特意没说的是下面这种情况：
有没有想过，在什么情况下会到e呢？是a满足了然后满足1次b，然后就到e了吗？
仿真结果说明一切...
仿真是没有结果的，处于一直断言的过程中，这是因为，存在$符号以后，必须保证所有的情况都是满足的才是真的断言成功，进入下一阶段。但是又因为$是无限大的，因此就不会存在真的断言成功了...当然，只有当所有的断言都是失败的，才会断言失败，但是因为无限大，谁又能保证...下一次不会成功呢？所以这就是个无解题。。。
那么这时候，first_match的作用就出来了。。。因为它只需要匹配一次就可以跳出这个阶段，进入下一阶段。
代码如下：
对比来看：
这时候就有结果了...这才是first_match真实的使用情况，当然，比如如下情况也可以看看：
代码如下：因为含有|->，所以都是等到所有情况都满足才能进入下一阶段，如果不是所有情况都满足，一直为黄色横三角。也不算断言失败。
仿真结果如图所示：
因此，我再回过头看这个代码，只更改了输入波形，再看。
由此可看出first_match的作用。
最后，回到原点，还是以LRM手册中的例子，如果添加|->会不会不一样？
仿真结果如下：
这样写，first_match也是起作用的。
- 总结
当前者为某个区间取值，例如[1:5]，如果没有|->或者|=>时，则匹配一次即可进入下一阶段或者断言成功，但是如果有|->或者|=>时，则必须保证所有情况都满足才能进入下一阶段，否则卡死。而first_match的作用就是在此时，使得只要出现一种满足情况即可进入下一阶段。
本文特别感谢β＋α＝γ≧θ同学提供的支持~
End
