如何在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);

然而,这在启动后第二个时钟边沿立即失败,我无法弄清楚原因.

Answer 1

你想在throughout你的断言中使用运算符是正确的,但是你编写的代码存在一些问题.让我们一块一块地看一下.

每当我写一个断言时,我都会注意我要检查的自然语言描述.根据你的情况,我们知道我们想要触发时,a从去0到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上找到一个工作示例.