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

Question

我写了以下断言：

    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”。

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

谢谢 .d.

Answer 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 来检测第一个 'event' 的第一次出现，然后启用断言。如果您希望能够在正式工具中检查断言，请确保您使卫星代码可合成。

Answer 2

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

来自 LRM：

The expression of the disable iff is called the disable condition. The disable iff clause allows preemptive resets to be specified. For an evaluation of the property_spec, there is an evaluation of the underlying property_expr. If the disable condition is true at anytime between the start of the attempt in the Observed region, inclusive, and the end of the evaluation attempt, inclusive, then the overall evaluation of the property results in disabled. A property has disabled evaluation if it was preempted due to a disable iff condition. The values of variables used in the disable condition are those in the current simulation cycle, i.e., not sampled.

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

但是，我可以提出两个可能导致您出现问题的问题： 1. 在你的 sim 的开头 Signal_ia 是 'X.在 20 个周期后，如果复位没有被断言，先行序列 $stable(Signal_ia) 将评估为真，断言将立即移动到评估后续序列 Signal_oq==Signal_ia（在同一循环中，因为使用了非重叠蕴涵）。如果这两个信号都是 'X，则 1'X == 1'X 的计算结果为 1'X，因此断言将失败。 2. 您提到要在第 21 个周期进行检查。但是，这个断言实际上会在第 20 个周期检查。如果有 20 个触发器，此时输出仍然是 'X，即使输入已经 20 个周期为 0。

我怀疑选项 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])] is equivalent to $assertcontrol(3, 15, 7, levels [,list]) — $assertoff[(levels[, list])] is equivalent to $assertcontrol(4, 15, 7, levels [,list]) — $assertkill[(levels[, list])] is equivalent to $assertcontrol(5, 15, 7, levels [,list])

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

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

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

systemverilog assertion - how to ignore first event after reset

system-verilog

system-verilog-assertions