分解一個復雜端到端斷言屬性的一種方法是基于模塊化分級斷言證明,如下圖所示:

端到端屬性被分解為分別驗證每個子模塊:
P1 驗證 Sub1
P2 驗證 Sub2
P3 驗證 Sub3
我們使用P1已證明的屬性作為P2斷言證明的假設,所以模塊化分級證明的要點就在于“后級模塊的證明假設,一定要有前級斷言的證明保證”,即“assume-guarantee”原則,這個原則在EDA仿真驗證環(huán)境集成時也是適用的。
由于這種“assume-guarantee”原則的保證,上面3個模塊如果都完成了證明,那么也相當于端到端的斷言屬性完成了證明。
分而治之,各個擊破的方法,在大規(guī)模芯片驗證中非常適用,但是也很容易引入質(zhì)量風險。
審核編輯:劉清
聲明:本文內(nèi)容及配圖由入駐作者撰寫或者入駐合作網(wǎng)站授權(quán)轉(zhuǎn)載。文章觀點僅代表作者本人,不代表電子發(fā)燒友網(wǎng)立場。文章及其配圖僅供工程師學習之用,如有內(nèi)容侵權(quán)或者其他違規(guī)問題,請聯(lián)系本站處理。
舉報投訴
-
eda
+關(guān)注
關(guān)注
72文章
3113瀏覽量
183028 -
EDA仿真技術(shù)
+關(guān)注
關(guān)注
0文章
5瀏覽量
5564
原文標題:如何降低Formal assertion的復雜性(二)
文章出處:【微信號:芯片驗證工程師,微信公眾號:芯片驗證工程師】歡迎添加關(guān)注!文章轉(zhuǎn)載請注明出處。
發(fā)布評論請先 登錄
相關(guān)推薦
熱點推薦
Intersil推出60V創(chuàng)新同步降壓控制器,大幅降低電源設計復雜性和系統(tǒng)成本
ISL8117可以大幅降低電源設計復雜性和系統(tǒng)成本。
發(fā)表于 05-27 13:47
?1818次閱讀
基于構(gòu)件回歸測試的復雜性度量框架
的軟件修改需求,維護者可以實施不同的修改手段.不同的修改手段會導致不同的回歸測試復雜性,這種復雜性是軟件維護成本和有效性的重要因素.目前的研究沒有強調(diào)構(gòu)件軟件的回歸測試復雜性問題.基于
發(fā)表于 01-19 16:41
?0次下載
如何降低人工智能的復雜性
人工智能的復雜性導致了兩個不利的結(jié)果,其一是人工智能領(lǐng)域的研發(fā)投入過高,而且研發(fā)周期過長,這本身會把大量的創(chuàng)業(yè)者擋在門外,其二是人工智能產(chǎn)品對于落地應用的條件要求也過高,導致產(chǎn)業(yè)領(lǐng)域應用人工智能產(chǎn)品的意愿降低。
發(fā)表于 09-22 16:09
?1490次閱讀
大數(shù)據(jù)分析學習的挑戰(zhàn):復雜性、不確定性及涌現(xiàn)性
來源:ST社區(qū) 科多分享的大數(shù)據(jù)分析學習與研究的新挑戰(zhàn):對于習慣結(jié)構(gòu)化數(shù)據(jù)研究的統(tǒng)計學來說,大數(shù)據(jù)分析顯然是一種嶄新的挑戰(zhàn)。 挑戰(zhàn)來自何方?來自于大數(shù)據(jù)的復雜性、不確定性和涌現(xiàn)性三個方面,其中復雜性
降低無線連接、共存的復雜性
。 ? 討論降低無線連接復雜性的小組成員。 “降低無線連接的復雜性”是最近 NXP Connects 會議上的一個小組討論的主題,我們主持了 Google、HID Global、三星和
可以通過降低約束的復雜度來優(yōu)化Formal的執(zhí)行效率嗎?
我們可以通過降低約束的復雜度來優(yōu)化Formal的執(zhí)行效率,但是這個主要是通過減少Formal驗證空間來實現(xiàn)的,很容易出現(xiàn)過約,導致bug遺漏。
Formal Verification的基礎(chǔ)知識
,如Intel,使用自研formal工具;還有一些提供formal解決方案的公司,如OneSpin(已與Siemens EDA合作),Oski Tec(已被NVIDIA收購)。 Assertion 具體
使用Emulex SAN管理器降低操作復雜性
電子發(fā)燒友網(wǎng)站提供《使用Emulex SAN管理器降低操作復雜性.pdf》資料免費下載
發(fā)表于 07-28 16:09
?0次下載
如何利用AI降低電子系統(tǒng)設計的復雜性呢?
在電子系統(tǒng)設計領(lǐng)域,復雜性一直是一個主要的挑戰(zhàn)。隨著技術(shù)的進步和對更高效、更強大的電子設備的需求的增長,工程師們面臨著越來越復雜的設計要求。
發(fā)表于 08-02 09:14
?898次閱讀
如何降低Formal assertion的復雜性呢?
評論