validation - 系统verilog属性定义中[->1]的含义

Question

我一直无法找到[->]表达式的含义。我熟悉使用范围作为[a:b]或序列，例如EVENT1|->EVENT2，但不熟悉我在开头提到的那个。

上下文是一个断言属性，可确保在复位为低电平时 clk1 始终处于切换状态。

@(clk2) disable iff(rst) !$stable(clk1)[->1];

关于[->]真正含义的任何想法？

提前致谢！

Answer 1

基本上有3个这样的运营商：

连续重复 [*n] -

(a ##1 b[*2] ##1 c) = (a ##1 b ##1 b ##1 c)

这意味着，a 应该被断言，然后 b 应该在连续 2 个时钟滴答上被断言，在下一个时钟滴答中 c 的断言之后。

转到重复 [->n] -

(a ##1 b[->2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 c)

这意味着，a 应该被断言，然后 b 应该在 2 个时钟滴答上被断言，但不是连续的。并且一旦 b 在 2 个时钟节拍上被断言，在下一个时钟节拍上 c 应该被断言

非连续重复 [=n] -

(a ##1 b[=2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 !b[*0:$] ##1 c)

这意味着，a 应该被断言，然后 b 应该在 2 个时钟滴答上被断言，但不是连续的。并且一旦 b 在 2 个时钟滴答上被断言， c 应该被断言，然后 b 再次被断言第三次。

请记住，[->n] 和 [=n] 运算符之间的区别与最后一个操作数“c”有关。在 [->2] 中，只要 b 被断言两次（非连续），就应该在下一个时钟滴答声中断言 c。但是在 [=2] 中，c 应该被断言，在 b 被第三次断言之前（非连续）

Answer 2

如其他答案所述和解释，系统verilog中基本上有3个重复运算符可用。

编码

    @(clk2) disable iff(rst) !$stable(clk1)[->1];

可以解释如下：

如果“rst”为高，则“禁用”断言属性。如果不是这样，请检查“clk1”对于“1”clk2 时钟变化（从高到低或从低到高）是否“不稳定”，不一定在连续的 clk2 时钟变化上。

这意味着断言：

• 如果 rst 为 1，将被禁用（即既不通过也不失败）。

• 如果 clk1 在 1 个 clk2 时钟变化时不稳定（保持其状态，即高或低），则将通过。但是，clk1 不必在连续的 clk2 时钟变化上不稳定。

• 否则会失败。

建议您要检查 clk1 是否以高于 clk2 的频率运行。

Answer 3

[->N]意思是“不连续的精确重复”。a[->N]表示 a 的 N 次非连续重复，匹配恰好发生在 a 的第 N 次重复之后。

因此，例如，a ##1 b[->2] ##1 c将匹配

          _
a _______/ \_____________________
         |          _     _ 
b _________________/ \___/ \_____
         |                  _
c _________________________/ \___
         |                   |
         |                   |
match    |<----------------->|

但不是

          _
a _______/ \___________________________
                    _     _ 
b _________________/ \___/ \___________
                                  _
c _______________________________/ \___

[=N]意思是“不连续的重复”。a[=N]表示 a 的 N 次非连续重复，匹配发生在 a 的第 N 次重复之后的任何时间。

因此，例如，a ##1 b[=2] ##1 c将匹配上面的第二个模式。