如何编写正式验证属性？

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

我想在第一个时钟周期后禁用属性iff sig1 = 1'b1。如何编写正式验证属性？

sig1上从高到低的转换是我的触发条件。如果我禁用iff（sig1）触发条件将不会被满足。

在正式验证程序中使用“遍及”也是不可能的。

我该怎么办？谢谢！

来源

2016-05-12 kkdev

请详细说明。为什么你不能使用'禁用iff（sig1）;'？ – sharvil111

在sig1上从高转换为低是我的触发条件。如果我禁用iff（sig1）触发条件将不会被满足。 – kkdev

已更新。只是一个侧面说明。你可以使用非重叠（| =>）运算符，只有当$ fell（sig1）的计算结果为TRUE时，才评估sequence1的值吗？像：'$ fell（sig1）| => sequence1 | - > sequence2;' – sharvil111

如何写一些卫星代码派生的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

来源

2016-05-12 12:33:02

如果我没有错，它仍然会延迟禁用iff一个时钟周期从我想要做的事情。 – kkdev

但是请注意，我仍然有'$下降（sig1）'不'$下跌（sig1d）'。当然，如果你想禁用它，即使sig1在第一个时钟周期是高电平的，那么'$ fell（sig1）'永远不会是真的？也许我们需要一个时序图？（或者修改我的代码以生成一个？） –

@MthetheTTaylor你必须小心“disable”表达式是异步采样的，并且可能导致竞争条件。你应该使用'disable iff（$ sampled（sig1d））'。 –

可以重新写你的断言只触发如果你没有看到sig1高第一个周期后：

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

来源

2016-05-13 18:10:36

我已经试过了。问题是，我无法在sequence2上做到这一点。例如： $ fell（sig1）## 1！sig1 entire（sequence1）| - > sequence2; 但我不能把整个sequence2（正式工具不允许）。所以我认为最好的情况是在一个周期后禁用sig1上的属性。任何其他建议是最受欢迎的。 – kkdev

@kkdev从我收集的内容来看，你应该改述你的问题，因为它是模糊的。如果'sig1'在第一个周期后变高（这可以理解为第一个周期后的周期），您不想要禁用该属性。如果'sig1'在任何后续循环中变高，则要禁用它。你应该尝试使用@ MathewTaylor的答案，因为这是唯一的方法。 –

如何编写正式验证属性？

回答

相关问题