0

考虑以下规范：

"interrupt must hold until interrupt ack is received"

在此处输入图像描述

这些断言是否相等并符合规范？

1-第一个断言（使用递归属性）：

property intr_hold(intr, intrAck);
   intrAck or (intr and (1'b1 |=> intr_hold(intr, intrAck)));
endproperty 

assert property @(posedge clk) $rose(intr) |=> intr_hold(intr, intrAck);

2-第二个断言（使用非递归属性）：

assert property @(posedge clk) intr |=> intr or past(intrAck);

谢谢

4

1 回答 1

0

第一个属性不接受两者intr都intrAck为低的循环。在这样的循环中，第一部分or失败，因此必须评估第二部分。这部分不能通过，因为第一部分and失败了，因此连词失败了。整个财产都失败了。

即使我们忽略这样的循环，第一个断言也不会捕捉到失败的情况。

intr让我们从信号变高时开始分析您的示例。

  • 第一个循环intrAck失败，但第二部分or开始匹配。intr通过并且蕴涵的前项匹配并触发下一个循环的递归评估
  • 在第二个周期，新的属性评估开始，同样的事情重复。仍然存在对前一个循环的结果的评估（递归评估）。对于这个，将安排另一个递归评估。现在对该属性的两个评估是“活跃的”。
  • 在第三个周期intrAck通过并且新的属性尝试通过。之前安排的两个属性评估也通过了，因为intrAck它是高并且状态在周期 1 和 2 开始的属性评估也通过了。

非递归形式很好。

从模拟效率的角度来看，即使以某种方式重写递归形式以符合规范，它也会更糟。这是因为有许多待定的财产评估。从周期 1 开始的属性评估在周期 3 之前仍然“有效”。从周期 2 开始的属性评估在周期 3 之前也仍然有效，因此在周期 2 中，如果需要第四个周期来确定通过/fail，将会有第三个待定评估。一旦启动了相同属性的新评估，工具可能能够通过忽略以前的评估来更有效地实现这一点（因为无论如何都会发出失败的信号），但是模拟器通常会显示何时开始为调试目的完成的属性评估，这会得到更多如果“旧”，实施起来很复杂

于 2017-12-23T16:59:47.980 回答