systemverilog 断言 - 重置后如何忽略第一个事件答案

【问题标题】：systemverilog assertion - how to ignore first event after resetsystemverilog 断言 - 重置后如何忽略第一个事件
【发布时间】：2017-10-30 08:32:29
【问题描述】：

我写了以下断言：

    assert property(@(posedge ClkRs_ix.clk) 
        disable iff (ClkRs_ix.reset) $stable(Signal_ia)[*20] |-> 
        (Signal_oq==Signal_ia));

我想表达输入信号稳定的20个时钟周期，在第21个周期，输出必须与输入具有相同的值。

这一个有效，但前提是我保证在重置期间 Signal_ia 的状态没有变化。如果我断言复位，改变 Signal_ia 的状态，然后释放复位，这个条件总是失败。这通常发生在我使用 Signal_ia = 'X' 开始模拟并且在重置期间它变为 '0' 时。

有什么办法可以写得更好吗？响应。有没有办法在重置后忽略第一个事件，因为它可能由于重置时发生的情况而跳闸？如果我理解得很好，如果我保证，这个断言在重置期间会被忽略。我试图描述的效果有一些延迟，理想情况下，我不仅需要在复位时忽略这种情况，而且在复位状态解除断言后的 20 个周期内也需要忽略这种情况。

谢谢 .d.

【问题讨论】：

标签： system-verilog system-verilog-assertions

【解决方案1】：

一种方法是使用级联蕴涵运算符：

assert property(@(posedge ClkRs_ix.clk) 
    disable iff (ClkRs_ix.reset) $stable(Signal_ia)[*20] |-> 
    $stable(Signal_ia)[*20] |-> (Signal_oq==Signal_ia));

隐含运算符是右结合的所以

A |-> B |-> C

等价于

A |-> (B |-> C)

换句话说，在 A 发生之前不要检查B |-> C。

实现此目的的另一种方法是使用卫星代码。附属代码是用宿主语言编写的代码，有助于断言。因此，您可以编写一个 FSM 来检测第一个“事件”的第一次出现，然后启用断言。如果您希望能够在正式工具中检查断言，请确保使卫星代码可合成。

【讨论】：

在整个仿真过程中，这个断言会等待 Signal_ia 的 20 个时钟，然后再等待 Signal_ia 的 20 个时钟，然后再比较信号。我相信它将检查 40 个时钟的稳定性。正如您所提到的，编写一些粘合逻辑可能是更好的选择。
@sharvil111 我和你的想法不同。我认为这个断言将等待 Signal_ia 的 20 个时钟，然后每隔一个 Signal_ia 的 20 个时钟，比较信号。我猜提问者需要实现它并尝试一下。然而，多亏了你的评论，我现在确实看到了我狡猾的计划中的一个缺陷：在 Signal_ia 的每 20 个时钟之后，将启动一个新线程，因此在模拟结束时将有无数个并发线程在运行。因此，在这种情况下，正如您所说，编写一些胶合逻辑可能是更好的选择，因为如果没有别的办法。

【解决方案2】：

首先要注意的是 disable iff (rst) 子句是异步的。因此，它不遵守常规的断言采样规则。

来自 LRM：

禁用 iff 的表达式称为禁用条件。这 disable iff 子句允许指定抢先式重置。为 property_spec 的评估，有一个评估基础属性_expr。如果禁用条件在任何时候为真在观察区域的尝试开始之间，包括在内，以及评估尝试的结束，包括在内，然后是整体财产评估结果禁用。一个属性有如果由于禁用 iff 而被抢占，则禁用评估健康）状况。禁用条件中使用的变量值是当前模拟周期，即未采样。

在您的情况下，对于重置之前的每个周期，都会为您的断言生成一个新线程。一旦重置出现，所有这些实例都被禁用并且它们的属性评估被暂停。任何新的评估只会在重置被取消断言后开始。因此，我看不出这怎么会是您的问题的原因。

但是，我可以提出两个可能导致您的问题的问题： 1. 在您的 sim Signal_ia 的开头是 'X.在 20 个周期后，如果尚未断言复位，则前面的序列 $stable(Signal_ia) 将评估为真，并且断言将立即转移到评估后续序列 Signal_oq==Signal_ia （在同一个周期中，因为非重叠暗示是用过的）。如果这两个信号都是'X，则 1'X == 1'X 评估为 1'X，因此断言将失败。 2. 您提到您希望在第 21 个周期进行检查。然而，这个断言实际上会在第 20 个周期检查。如果有 20 次 flop，此时输出仍将是 'X，即使输入已 0 持续 20 个周期。

我怀疑选项 1. 更有可能，因为 2. 可能很明显。

为了解决这两个问题，我建议您更改断言以在输入更改时触发以解决此问题。

CHECK_OUTPUT:  assert property(@(posedge ClkRs_ix.clk) 
                       disable iff (ClkRs_ix.reset) $changed(Signal_ia) |=>
                            $stable(Signal_ia)[*20] ##0 (Signal_oq==Signal_ia));

正如所指出的，您还可以选择性地启用断言。 $asserton 和 $assetkill (assertoff) 可以帮助你做到这一点：

$asserton[(levels[, list])] 等价于 $assertcontrol(3, 15, 7、levels[,list])——$assertoff[(levels[,list])]等价于 $assertcontrol(4, 15, 7, 级别 [,list]) — $assertkill[(级别[, list])] 等价于 $assertcontrol(5, 15, 7, levels [,list])

assertkill 将杀死任何已经在运行的线程（与 asseroff 不同，它只会阻止未来的线程）。在我看来，你会在 assertkill 之后。然后，您可以通过 asserton 重新启用您的断言。

正如所指出的，在正式场景中，这自然需要通过断言中的控制信号和 FSM 来生成它。

【讨论】：