system-verilog - 如何在 systemverilog 断言中使用整个运算符

Question

这是一个规范：如果信号a被断言，那么它必须被断言直到信号b被断言，然后它应该在下一个时钟沿取消断言。我正在阅读 LRM 的 16.9.9 （以及http://www.testbench.in/AS_06_SEQUENCES.html）以及我理解它的方式，上面提到的规范可以写成

   property a2b_notA;
        @(posedge clk) ($rose (a) ##0 (a throughout b)) |=> (~a);
   endproperty
   a_a2b_notA: assert property (a2b_notA);

然而，这在启动后的第二个时钟边沿立即失败，我不知道为什么。

score 14 · Accepted Answer

您希望使用throughout运算符进行断言是正确的，但是您编写的代码存在一些问题。让我们一块一块地看。

每当我写一个断言时，我都会注意我想要检查的自然语言描述。在您的情况下，我们知道我们想要触发afrom0到1。之后发生的一切都是我们想要检查的行为，所以它应该在蕴涵运算符的右侧：

$rose(a) |-> ... something ...

您编写断言的方式，它只会触发检查throughout序列是否也发生在rose(a). 这将导致您忽略不良行为。

下一个难题是“a必须保持高位直到b被断言”。在这里，我们将使用整个运算符。序列“直到b被断言”表示为b [->1]。这相当于!b [*] ##1 b. 因此我们的序列应该是a throughout b [->1]。

throughout序列将在变高时结束b。在这一点上，我们需要检查a下一个周期的低电平：##1 !a. 我在这里使用了逻辑否定，因为我发现它比按位否定更清楚，但结果应该是相同的。

把它们放在一起，整个属性应该是：

$rose(a) |-> (a throughout b [->1]) ##1 !a;

我在这里使用了重叠的含义，因为当变高b时可能已经a很高了，在这种情况下，我假设a在下一个周期应该立即变低。如果没有，您可以自己摆弄细节。

您可以在EDAPlayground上找到一个工作示例。

1 回答 1