SVA中蘊涵（ - >）和## 0有什麼區別？

Question

是什麼下面的語句

a -> b之間VS a ##0 b

在SVA（SystemVerilog聲明）的細微差別？

Answer 1

你必須檢查的第一件事是單個蘊涵運算符的語法是a |-> b。

在SystemVerilog聲明中有兩個表達式。

1. a ##0 b
2. a |-> b

事實上，它看起來像在表達式中的類似。首先該表達式是檢查a被聲明（1），並且在0時鐘週期b被聲明（1）或沒有聲明之後。第二個表達式是當a被斷言（1）時檢查b是（on）斷言，然後在相同的posedge b被斷言（1）或不確定。

現在，實際上當驗證工程師寫這種斷言時，他們會照顧以下事情。

1. a ##0 b：在這個表達式中，如果a不然後斷言它示出了故障。

當a被斷言（1）和上相同時間戳b未被斷言然後還示出了故障。

a |-> b：在這個表達式中，如果a被斷言並且b未被斷言它就會出現一個故障。

如果a不被認定那麼它是不會檢查是否b斷言與否。此行爲與a ##0 b不同。

如果您應用不同的輸入數據，則可以看到表達式a ##0 b會給您帶來比a |-> b更多的失敗。上面已經解釋了相同的原因。

還有一點需要注意的是「蘊含結構只能用於屬性定義，不能用於序列。」

感謝，

Ashutosh說

Answer 2

你的問題說明了蘊涵算（|->）的重要性。此示例使用蘊涵算和是有用的：

a -> b意味着「如果a爲真，則b應該是true」（有用）。

這不是不和通常不是非常有用：

a ##0 b意味着「a和b應該是在任何時候都爲真」（不是很有用）。

https://www.edaplayground.com/x/47iN