如果出现一个序列，则在 System-Verilog 断言中会在其中出现一个子序列

Question

我想说： "if the sequence A occurs then the sequence B occurs within that sequence"。我该怎么做？

我原以为我可以使用断言：

assert property (@(posedge clk) (A |-> (B within A));

但这似乎不适用于我的示例。

我读过：

The linear sequence is said to match along a finite interval of consecutive clock ticks provided the first boolean expression evaluates to true at the first clock tick, the second boolean expression evaluates to true at the second clock tick, and so forth, up to and including the last boolean expression evaluating to true at the last clock tick.

但我怀疑时钟滴答传递到了 |-> 最后一个时钟滴答的另一边，而我希望它成为第一个时钟滴答。

我的具体示例是一个累加器，如果我添加足够多的正数，我预计它会溢出，所以我想要 A = (input == 1)[*MAX_SIZE] 和 B = (output == 0)，所以这里 B 是一个长度序列1，不知道会不会出问题

我是 system-verilog 的新手，所以可能是我代码的其他部分出了问题，但我还没有在任何地方看到这个例子。

Answer 1

您是正确的，|-> 运算符中的结果在 A 已经匹配后开始。你想要的是回顾过去："once I've seen A, have I seen B within A?".

您可以使用序列的 triggered 属性来执行此操作：

sequence b_within_a;
  @(posedge clk)
    B within A;
endsequence

assert property (@(posedge clk) A |-> b_within_a.triggered);

b_within_a序列会恰好匹配到A的末尾，当然如果B也发生了，也就是当triggered属性的计算结果为 1.

请注意，b_within_a 序列有专门定义的时钟。这是 LRM 的要求，否则您将无法在其上调用 triggered。

如果出现一个序列，则在 System-Verilog 断言中会在其中出现一个子序列

If a sequence occurs then a subsequence occurs within it in System-Verilog assertions

system-verilog

system-verilog-assertions