1

我想说：“如果序列A发生，那么序列就B出现在该序列中”。我怎样才能做到这一点？

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

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

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

我读过：

如果第一个布尔表达式在第一个时钟节拍处计算为真，第二个布尔表达式在第二个时钟节拍处计算为真，以此类推，直到并包括最后一个布尔表达式在最后一个时钟滴答时计算为真。

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

我的特定示例是一个累加器，如果我添加足够多的正数，我希望它会溢出，所以我想要A = (input == 1)[*MAX_SIZE]and B = (output == 0)，所以这B是一个长度为 1 的序列，我不知道这是否会导致问题。

我对 system-verilog 很陌生，所以它可能是我的代码的其他部分出错了，但我没有看到这个例子在任何地方完成。

4

1 回答 1

2

您是正确的，|->运算符中的结果一旦A匹配就开始了。你想要的是回顾过去：“一旦我见过A，我见过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它。

于 2016-12-09T19:23:23.807 回答