基于仿真的先進(jìn)的驗(yàn)證在現(xiàn)在和可預(yù)見的將來都將保持主要芯片級驗(yàn)證骨干的地位。但是占總驗(yàn)證工作70%的模塊級驗(yàn)證又如何呢？我們可以采用已經(jīng)確認(rèn)的驗(yàn)證技術(shù)來回答下面這個基本的問題嗎-我能夠絕對肯定我的模塊/IP對于所有可能的方案都按照預(yù)期工作嗎？答案很簡單:不能。

隨著基于仿真的驗(yàn)證的過度發(fā)展,EDA產(chǎn)業(yè)已經(jīng)嘗試處理這種高風(fēng)險(xiǎn)局面。無論發(fā)展情況如何,功能驗(yàn)證復(fù)雜性、成效和成本都正在增加；工具產(chǎn)量增益未能跟上日益增加的設(shè)計(jì)復(fù)雜性的步伐；漏錯率表明沒有任何緩和跡象。結(jié)果怎樣呢？重新設(shè)計(jì)和重新流片率保持著相當(dāng)高的水平。

但是這就是喪失信心的理由嗎？當(dāng)然不是。這里回顧一下十年前綜合驗(yàn)證的情況。那時,門級仿真被新的形式驗(yàn)證技術(shù):等價(jià)性檢驗(yàn)所替代。門級仿真是在驗(yàn)證過程中開發(fā)一些案例來檢驗(yàn)等價(jià)性。但這種方法存在一個問題,即案例的質(zhì)量直接影響到等價(jià)性檢驗(yàn)的質(zhì)量。此外,門級仿真的運(yùn)行速度通常非常慢,隨著數(shù)字設(shè)計(jì)的規(guī)模呈指數(shù)級增長,它的影響也越來越大。而解決這個問題的方法就是采用等價(jià)性檢驗(yàn),典型情況下,等價(jià)性檢驗(yàn)工具還可以指明兩種描述之間在哪些地方存在不同。雖然思維模式的轉(zhuǎn)換需要新的工具、方法和技巧,但由于等價(jià)性檢驗(yàn)已被證實(shí)可以提供相當(dāng)出色的結(jié)果,因此等價(jià)性檢驗(yàn)技術(shù)得到了廣泛采用。

等價(jià)性檢驗(yàn)十年前是為綜合驗(yàn)證所做的,現(xiàn)在完全的形式功能驗(yàn)證是為數(shù)字模塊和IP做的。等價(jià)性檢驗(yàn)是在數(shù)字集成電路開發(fā)過程中使用得一種方法,它的目標(biāo)是證明一個電路的兩種描述具有完全一致的行為。與完全的基于仿真的驗(yàn)證相比,這種驗(yàn)證技術(shù)可以提供2～5倍的生產(chǎn)力,其完備性可確保100%的輸入方案覆蓋率和100%的輸出行為覆蓋率。毫無疑問,模塊將永遠(yuǎn)按照預(yù)期要求工作。它提供了一個真正的功能簽收,這也是形式驗(yàn)證最初的承諾。

不過,完全的形式驗(yàn)證并不是針對所有功能驗(yàn)證任務(wù)的萬靈丹。但是對于眾多數(shù)字模塊和IP而言,它在驗(yàn)證質(zhì)量、成果和成本方面提供了相當(dāng)出色的結(jié)果。IP公司、SoC廠商和EDA產(chǎn)業(yè)可以通過采用完全的形式功能驗(yàn)證顛覆近年來的趨勢。

作者:Peter Feist

總裁兼CEO

OneSpin Solutions GmbH公司