SVA：并发断言的$rose, $fell, $past
Examples
property check(@ posedge clk) $rose(a) -> ##1 b[*3] ##1 c
endproperty
checker : assert property(check)
在上式中，需要关注的两点：
- 并发断言的采样时钟边沿的跳变，是否和时序逻辑采样值一样？
- $rose和posedge是否一样？
并发断言的采样
并发断言是根据每个时钟边沿的采样值，进行逻辑判断后，确认断言的成功和失败。
和正常的时序逻辑采样相同，在时钟沿跳变的变量，在当前时钟沿采的都是变化之前的值。
例如： 上例中在T2 的时候，a的采样值为0 而不是1.
$rose 和 posedge的区别
$rose和posedge都是用来捕捉边沿，但定义有所不同：
posedge
Define ： 数值由0->1的时刻
例如 ： 上例中T2就是a的一个posedge
$rose
Define ：连续连个采样周期所采值有变化，并且当前采样值为1。
例如上例中：
| Times | Value |
|---|---|
| T1 | 0 |
| T2 | 0 |
| T3 | 1 |
| T4 | 0 |
只有在T3的时候才符合定义，$rose为真，而不是在T2.
同理 $fell也是一样
$rose/ $fell在真实的posedge和negedge的时候是永远不会成立的。
$past
$rose $fell有个限制是只捕捉信号的最低比特， 如果捕捉的是个bus，就会跟预期不一致。
如果是对bus进行操作最好用 $past.
$past(var，num_of_ticks, enable)
- 需要注意$past是对之前的数值进行采样，但是如果在仿真一开始就执行 $past，没有足够的past，它会去看这个变量在声明时候的初始值，如果没有初始值，就会fail。
enable
第三个参数enable，相当于是门控， 只有在enable为1的时候才回去计算$past的值，如果enable为0 ， $past只会返回上一次的计算值。
property check(@ posedge clk) c -> $past(b,1,a)
endproperty
checker : assert property(check)
- 只有C为真， 即前置条件为真才会进行$past的计算
- 在计算$past之前，需要看a：
- a为1，计算
- a为0，返回上一次past值。
本文来自互联网用户投稿，文章观点仅代表作者本人，不代表本站立场，不承担相关法律责任。如若转载，请注明出处。 如若内容造成侵权/违法违规/事实不符，请点击【内容举报】进行投诉反馈！