system-verilog - SVA：使用暗示（|=>）与序列？

Question

SystemVerilog 断言属性可以使用隐含运算符|=>和序列构建##1

例如 ：

property P1;
  @(posedge clk)
    A ##1 B |=> C ##1 D;
endproperty

上面我们使用A ##1 B了作为启动序列（前件）和C ##1 D完成序列（后件）。

我不明白为什么它不能被重写为：

property P2;
  @(posedge clk)
    A ##1 B ##1 C ##1 D;
endproperty

您何时以及为什么会选择暗示|=>而不是序列##1？

Answer 1

序列通过的上述属性相同，但失败条件不匹配。

如果它们都是 1A ##1 B ##1 C ##1 D;则为A ##1 B |=> C ##1 D;真。

如果我们将 A 作为 1，那么其余的 0：

A ##1 B ##1 C ##1 D;失败并且A ##1 B |=> C ##1 D;会通过。

由于未满足启用序列的条件，后者不被视为失败。