2

我写了以下断言：

    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。

4

2 回答 2

2

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

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)

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

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

于 2017-10-30T09:31:26.113 回答
1

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

来自 LRM：

禁用 iff 的表达式称为禁用条件。disable iff 子句允许指定抢先式重置。对于 property_spec 的评估，存在对基础 property_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 次触发器，此时输出仍将是 '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, levels [,list]) — $assertkill[(levels[, list])] 等价于 $assertcontrol(5, 15, 7, levels [,list])

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

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

于 2017-10-31T22:08:19.063 回答