如何降低Formal assertion的復(fù)雜性呢？

分解一個復(fù)雜端到端斷言屬性的一種方法是基于模塊化分級斷言證明，如下圖所示：

端到端屬性被分解為分別驗證每個子模塊：

P1 驗證 Sub1

P2 驗證 Sub2

P3 驗證 Sub3

我們使用P1已證明的屬性作為P2斷言證明的假設(shè)，所以模塊化分級證明的要點就在于“后級模塊的證明假設(shè)，一定要有前級斷言的證明保證”，即“assume-guarantee”原則，這個原則在EDA 仿真驗證環(huán)境集成時也是適用的。

由于這種“assume-guarantee”原則的保證，上面3個模塊如果都完成了證明，那么也相當(dāng)于端到端的斷言屬性完成了證明。

分而治之，各個擊破的方法，在大規(guī)模芯片驗證中非常適用，但是也很容易引入質(zhì)量風(fēng)險。

審核編輯：劉清

聲明：本文內(nèi)容及配圖由入駐作者撰寫或者入駐合作網(wǎng)站授權(quán)轉(zhuǎn)載。文章觀點僅代表作者本人，不代表電子發(fā)燒友網(wǎng)立場。文章及其配圖僅供工程師學(xué)習(xí)之用，如有內(nèi)容侵權(quán)或者其他違規(guī)問題，請聯(lián)系本站處理。舉報投訴