递归和非递归属性：这些断言是否相等？

Posted 2021-05-03

请考虑以下规范：

"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);

谢谢

答案

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

即使我们忽略了这样的循环，第一个断言也没有发现失败的情况。

让我们从intr信号变高的时候开始分析你的例子。

• 在第一个周期intrAck失败，但or的第二部分开始匹配。 intr通过并且暗示的先行者匹配并触发下一周期的递归评估
• 在第二个周期，对房产的新评估开始，同样的事情重复。仍然存在对前一周期（递归评估）的结果的评估。对于这个，将安排另一个递归评估。现在，对该物业的两次评估是“活跃的”。
• 在第三个周期intrAck通过，新的财产尝试通过。两个先前安排的属性评估也通过，因为intrAck很高并且声明在第1和第2周期开始的属性评估也通过了。

非递归形式很好。

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