SystemVerilog中Assertions
本文部分内容是来自SV LRM书的翻译。
断言是设计的属性的描述。
● 如果一个在模拟中被检查的属性(property)不像我们期望的那样表现,那么这个断言失败。
例子如下:
仿真结果如下:在90ns时,and是成功的,intersect是失败的。
or构造就不讲了,很简单,二选一成立即可。
代码如下:因为含有|->,所以都是等到所有情况都满足才能进入下一阶段,如果不是所有情况都满足,一直为黄色横三角。也不算断言失败。
● 如果一个在模拟中被检查的属性(property)不像我们期望的那样表现,那么这个断言失败。
● 如果一个被禁止在设计中出现的属性在模拟过程中发生,那么这个断言失败。
关于系统的论述,我后面应该会写文章更新,今天主要讲讲几个比较容易疑惑的地方。
首先看个例子:
![](https://uploadfiles.nowcoder.com/images/20220623/926360688_1655947288429/6048F36E832A506F79D2DACC41789D22)
关于系统的论述,我后面应该会写文章更新,今天主要讲讲几个比较容易疑惑的地方。
无限的时序窗口
在时序窗口的窗口上限可以用符号“$”定义,这表明时序没有上限。这叫“可能性”(eventuality)运算符。检验器不停地检查表达式是否成功直到模拟结束。因为会对模拟的性能产生巨大的负面影响,所以这不是编写SVA 的一个高效的方式。最好总是使用有限的时序窗口上限。那么问题来了,我们是捕捉到一次成功断言就结束了呢?还是得一直捕捉下去?永不结束?首先看个例子:
还是同样的,那我如果是多添加一个事件,并且采用$符号呢?
例子如下:
and 构造
可以用来逻辑地组合两个序列。当两个序列都成功时整个属性才成功。两个序列必须具有相同的起始点,但是可以有不同的结束点。检验的起始点是第一个序列的成功时的起始点,而检验的结束点是使得属性最终成功的另一个序列成功时的点。看个例子
仿真结果如下:
intersect 构造
例子如下:
仿真结果如下:在90ns时,and是成功的,intersect是失败的。
or构造就不讲了,很简单,二选一成立即可。
first_match 构造
开始比较难理解的是first_match构造,这个在语言手册上也有一个例子,例子如下:
不是说first_match没用。只能说指导手册LRM提供的案例是不适合这种情况的...
前面特意提到$运算符,是因为这儿是有个大新闻的,就是蕴含运算和$放在一起就不得了...
蕴含等效于一个if-then 结构。蕴含的左边叫作“先行算子”(antecedent),右边叫作“后续算子”(consequent)。先行算子是约束条件。当先行算子成功时,后续算子才会被计算。我们来看点能起作用的~前面特意没说的是下面这种情况:
有没有想过,在什么情况下会到e呢?是a满足了然后满足1次b,然后就到e了吗?
仿真结果说明一切...
仿真是没有结果的,处于一直断言的过程中,这是因为,存在$符号以后,必须保证所有的情况都是满足的才是真的断言成功,进入下一阶段。但是又因为$是无限大的,因此就不会存在真的断言成功了...当然,只有当所有的断言都是失败的,才会断言失败,但是因为无限大,谁又能保证...下一次不会成功呢?所以这就是个无解题。。。
那么这时候,first_match的作用就出来了。。。因为它只需要匹配一次就可以跳出这个阶段,进入下一阶段。
代码如下:
代码如下:因为含有|->,所以都是等到所有情况都满足才能进入下一阶段,如果不是所有情况都满足,一直为黄色横三角。也不算断言失败。
最后,回到原点,还是以LRM手册中的例子,如果添加|->会不会不一样?
仿真结果如下:
这样写,first_match也是起作用的。
总结
当前者为某个区间取值,例如[1:5],如果没有|->或者|=>时,则匹配一次即可进入下一阶段或者断言成功,但是如果有|->或者|=>时,则必须保证所有情况都满足才能进入下一阶段,否则卡死。而first_match的作用就是在此时,使得只要出现一种满足情况即可进入下一阶段。
欢迎点赞,关注,分享~~,本文原发于微信公众号【 数字ic小站】