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