介紹使用SVA的幾個(gè)優(yōu)勢(shì)

1. SVA支持多時(shí)鐘域（clock domain crossing (CDC)）邏輯，例如異步FIFO。

2. SVA是一種描述語(yǔ)言，可讀性比較強(qiáng)。

3. 可以方便描述可執(zhí)行的設(shè)計(jì)規(guī)格，而不是一些模棱兩可的自然語(yǔ)言。

4. 可用來(lái)檢查設(shè)計(jì)不允許的異常場(chǎng)景，或者設(shè)計(jì)必須滿足的規(guī)格等等

5. 支持開(kāi)發(fā)參數(shù)化的check ，在不同模塊或者不同項(xiàng)目之間復(fù)用，甚至在Formal工具和EDA仿真工具之間復(fù)用。

6. 可以通過(guò)“bind”方式加載到RTL上，不需要修改RTL。

7. 相比黑盒用例，SVA更容易定位。

8. “assert”可用于Formal屬性證明。

9. “assume”可用于Formal輸入場(chǎng)景約束

10. “cover”可用于Formal覆蓋率

最后，驗(yàn)證環(huán)境中每一個(gè)約束都應(yīng)該是一個(gè)assert，需要在集成驗(yàn)證環(huán)境或者周邊模塊驗(yàn)證環(huán)境中檢查。

審核編輯：劉清