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

Question

这里有一个规范:如果信号a被断言，那么它必须被断言，直到信号b被断言，然后它应该在下一个时钟边沿取消断言。我正在通读LRM16.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);

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

Answer 1

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

每当我写一个断言时，我都会注意我想要检查的东西的自然语言描述。在您的例子中，我们知道要在a从0转到1时触发。之后发生的所有事情都是我们想要检查的行为，所以它应该在隐含运算符的右侧：

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

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

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

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

将所有这些放在一起，整个属性应该是：

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

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

你可以在EDAPlayground上找到一个可用的例子。