断言中 |-> 1[0:$] 的含义

Question

使用示例：

state==ACTIVE1 |-> 1[0:$] ##1 state==ACTIVE2

断言试图解决的问题是： 如果状态机达到

state=ACTIVE1

，最终将达到

state=ACTIVE2

。

知道

|-> 1[0:$]

实际上意味着什么吗？

另外，有更好的方法吗？

Answer 1

在 SVA 中，

1

实际上是一个通配符，因为根据定义，它是真的。所以它匹配任何东西。

<expression>[<number or range>]

是 SVA 重复运算符。

$

的意思是“无穷大”。

所以，

1[0:$]

的意思是“任何零次或多次”。

有更好的方法吗？是的。以下是一些其他方法，它们都会遇到与您的示例相同的问题：

state==ACTIVE1 |-> ##[0:$] state==ACTIVE2
state==ACTIVE1 |-> eventually state==ACTIVE2

这些问题是什么？

(i) 如果有很多

ACTIVE1

而没有

ACTIVE2

，那么将会启动越来越多的检查（即产生线程），这会减慢您的模拟速度。这是在右侧使用

$

或

eventually

的问题（结果 或 条件）。

(ii) 你的断言永远不会失败：无论宇宙热寂是否没有

ACTIVE2

，你的断言都不会失败。这是一个折衷的断言，即所谓的strong属性：

state==ACTIVE1 |-> s_eventually state==ACTIVE2

s_

代表“强”。现在，如果您的断言在模拟结束时尚未通过，则被视为失败。