如何在System verilog聲明中編寫屬性？

我想在SVA中編寫一個屬性來正式驗證行爲。如何在System verilog聲明中編寫屬性？

這裏是我想：

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    $fell(sig1) ##[1:$] first_match($fell(sig2)) ##0 sig3 |-> sig4 == sig3; 
endproperty

我怎樣才能把上面的屬性，以便SIG1下降之後，它保持剩餘的評估週期中低？

注：我不想把SIG1爲disable IFF（SIG1）

謝謝！

來源

2016-05-06 kkdev

是「SIG1下降之後，它保持剩餘的評估週期中低」的_precondition_或_condition_的一部分嗎？換句話說，你想檢查sig4 == sig3 _if_ sig1是否保持低電平，或者你想檢查sig1保持低電平以及檢查sig4 = sig3嗎？ –

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    (!sig1) throughout (##[1:$] first_match($fell(sig2)) ##0 sig3) 
      |-> sig4 == sig3; 
endproperty

見部分16.9.9條件在序列在2000至12年LRM

來源

2016-05-06 17:03:01

謝謝！還有一個問題：我如何擴展這個屬性來驗證16個連續週期（sig4 == sig3）[* 16]的結果/滿足序列？同時確保sig1 == 1'b0; – kkdev

你也可以在**中使用**，但是在一個簡單的情況下，你可以做'（！sig1 && sig4 == sig3）[* 16]' –

在上面的例子中，如果sig1是一個主輸入，那麼該工具將嘗試找到sig1爲1'b1的反例。我試圖在後面使用「全部」，但是沒有成功。我可以嘗試如下的東西嗎？（！sig1）全部（## [1：$] first_match（$ fell（sig2））## 0 sig3 | - > sig4 == sig3） – kkdev

如何在System verilog聲明中編寫屬性？

回答

相關問題