system-verilog - SVA 重复非连续操作资格赛

Question

我有以下财产：

property p;
  @(posedge clk) a |=> b[=2] ##1 c;
endproperty

它告诉我们，如果a被断言，则从下一个开始clk，b应该非连续两次断言，然后c在最后一次之后的任何时间断言b。

我的问题是 if在 first和 secondc之间断言怎么办。断言应该立即失败还是继续？一些参考书说它应该失败，但我对此表示怀疑。预期的行为是什么？bb

Answer 1

[=or非连续重复运算符类似于goto 重复，但表达式不必在时钟周期为真之前c为真。

假设a是断言。蕴涵条件得到满足并进一步评估断言。

此后，b检查两次，不管是什么c。一旦发现在两个不连续的时钟边沿都被断言，b然后在1 c个时钟周期后检查（由于##1）。

如果在检查c2 次时断言和取消断言，b则不考虑该切换。的被认为是在2 个断言之后。cb

以下快照将给出一个清晰的想法：

传递快照：

失败快照：

在这里，即使 出现故障c，断言也没有通过。

有关更多详细信息，请参阅SystemVerilog 断言实用指南 pdf。 Doulos 教程也是一个不错的教程。

Answer 2

简而言之，是的，它会过去的。无论c在哪里被断言，在观察到两个“b”之后，它都会等到c==1。因此，如果 c 从一开始就为 1 并且永远不会变为零，那么它也会通过。

还有一点需要说明的是，这个断言何时会真正失败。当 c 被断言时它会通过，但如果不是，它将一直运行到测试结束！您只会在模拟结束时看到失败。