如何編寫正式驗證屬性？

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的答案，因爲這是唯一的方法。 –

如何編寫正式驗證屬性？

回答

相關問題