如何写属性进行形式验证？答案

【问题标题】：How to write property for formal verification?如何写属性进行形式验证？
【发布时间】：2016-05-12 10:11:41
【问题描述】：

property prop1;
@(posedge clk)
$fell(sig1) ##1 sequence1 |-> sequence2;
endproperty

我想在第一个时钟周期后禁用属性iff sig1=1'b1。

sig1 从高到低的转换是我的触发条件。如果我这样做disable iff(sig1) 将不会满足触发条件。

同样使用throughout 在形式验证器中的启用和满足序列上也是不可能的。

我该怎么做？谢谢！

【问题讨论】：

请详细说明。为什么不能使用disable iff (sig1);？
sig1 从高到低的转变是我的触发条件。如果我禁用 iff(sig1) 触发条件将不会被满足。
已更新。只是一个旁注。您可以使用非重叠 (|=>) 运算符，以便仅当 $fell(sig1) 评估为 TRUE 时，才评估 sequence1？喜欢：$fell(sig1) |=> sequence1 |-> sequence2;
我很确定语法明智这是不可能的，我的问题是不同的。一个时钟周期后禁用该属性。

标签： system-verilog formal-verification system-verilog-assertions

【解决方案1】：

如何编写一些卫星代码来推导出sig 的延迟版本：

  always @(posedge clk) sig1d <= sig1;

  property prop1;
    @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 sequence1 |-> sequence2;
  endproperty

http://www.edaplayground.com/x/2tbX

【讨论】：

如果我没记错的话，它仍然会将禁用 iff 延迟一个时钟周期。
但请注意，我仍然有 $fell(sig1) 而不是 $fell(sig1d)。当然，如果你想禁用它，即使sig1 在第一个时钟周期为高电平，那么$fell(sig1) 永远不会是真的？也许我们需要一个时序图？（或者修改我的代码来生成一个？）
@MatthewTaylor 您必须小心disable 表达式是异步采样的，并且可能导致竞争条件。你应该使用disable iff ($sampled(sig1d))。
@MatthewTaylor ：您提供的代码似乎适用于模拟（我没有尝试）。但在形式化工具上，会导致证据空洞，即无法实现使能序列。
@Tudor 谢谢。因此，sig1d 将在 NBA 区域中被驱动，$fell(sig1) 将在 preponed 区域中进行采样，并且可能会评估 disable（因此 sig1d采样）在观察到的区域，因此是种族。

【解决方案2】：

您可以重写您的断言以仅在第一个循环后没有看到sig1 高电平时触发：

property prop1;
  @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 !sig1 ##0 sequence1 |-> sequence2;
endproperty

【讨论】：

我已经试过了。问题是，我不能在 sequence2 上做到这一点。例如： $fell(sig1) ##1 !sig1 through (sequence1) |-> sequence2;但我不能把整个序列2（正式工具不允许）。所以我认为最好的情况是在一个周期后禁用 sig1 上的属性。欢迎任何其他建议。
@kkdev 据我所知，您应该重新表述您的问题，因为它含糊不清。如果sig1 在第一个周期后变高（可以解释为第一个周期后的周期），您不想禁用该属性。如果sig1 在任何后续循环中变高，您想禁用它。您应该尝试使用@MathewTaylor 的答案，因为这是唯一的方法。