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