cut point可優(yōu)化FEV的執(zhí)行效率
cut point就是在模型中指定一個位置，將這個cutpoint的值設(shè)為隨機值，去除這個點前后邏輯的關(guān)聯(lián)性。 需要確認這個cut point的設(shè)定不會影響所需要證明的assert，如果影響了可以根據(jù)fail反例定位。 其實，這也類似于一個黑盒，只不過blackbox針對的是一個模塊，將該模塊所有的輸出都設(shè)定為隨機值，而cut point只是將特定的點（信號）設(shè)置為隨機值。 一句話概括：
cutpoint就是更細粒度的黑盒化。
前面我們提到的FEV等價性驗證中的每一個map點都是一個cut point。所以內(nèi)部能夠map上的點越多，F(xiàn)EV等價性證明的效率越高。 像黑盒化一樣，cutpoint也是一個安全的復(fù)雜度優(yōu)化手段，可能會導(dǎo)致假fail，但絕不會引入假pass。因為使用cut point后證明的空間比原來更大了，并且降低了被證明邏輯的復(fù)雜度。
在combinational FEV中，所有寄存器的狀態(tài)都是一個cut point。在sequential FEV中，默認只會比較輸出的一致性，如果添加內(nèi)部某些寄存器狀態(tài)作為map點，可以優(yōu)化FEV的執(zhí)行效率。
審核編輯：彭靜
聲明：本文內(nèi)容及配圖由入駐作者撰寫或者入駐合作網(wǎng)站授權(quán)轉(zhuǎn)載。文章觀點僅代表作者本人，不代表電子發(fā)燒友網(wǎng)立場。文章及其配圖僅供工程師學習之用，如有內(nèi)容侵權(quán)或者其他違規(guī)問題，請聯(lián)系本站處理。
舉報投訴
-
寄存器
+關(guān)注
關(guān)注
31文章
5528瀏覽量
128613 -
模型
+關(guān)注
關(guān)注
1文章
3628瀏覽量
51619
原文標題：FPV復(fù)雜度優(yōu)化之cut point
文章出處：【微信號：芯片驗證工程師，微信公眾號：芯片驗證工程師】歡迎添加關(guān)注！文章轉(zhuǎn)載請注明出處。
發(fā)布評論請先 登錄
相關(guān)推薦
熱點推薦
程序結(jié)構(gòu)的優(yōu)化及執(zhí)行速度
對程序進行優(yōu)化，通常是指優(yōu)化程序代碼或程序執(zhí)行速度。優(yōu)化代碼和優(yōu)化速度實際上是一個予盾的統(tǒng)一。一般是優(yōu)化
發(fā)表于 07-25 11:36
?1275次閱讀
新一代CUT75系列PCB基板式開關(guān)電源問世
導(dǎo)讀：日前，TDK公司宣布推出新一代PCB基板式開關(guān)電源--CUT75系列產(chǎn)品。CUT75系列新品是伴隨著市場對更輕薄、更高效率，更高性價比的三路輸出開關(guān)電源的需求而問世，為客戶系統(tǒng)的小型化
發(fā)表于 09-27 15:24
常用優(yōu)化編譯選項對ARM平臺的影響
buffer+10的數(shù)據(jù)被修改。而在point2.s中，貌似又針對流水線進行了優(yōu)化，程序執(zhí)行順序會有所變化，在對buffer部分位置賦初值的順序是在str r3, [sp, #7]之后，所以
發(fā)表于 06-16 14:38
SPC574K7x的CUT 2.3和CUT 2.4之間有什么區(qū)別？
CUT 是什么意思？我想是一個 CPU 識別標簽，但我不確定。我使用 SPC5 studio V.6.0 開發(fā)一個項目，但我不明白我的項目中必須包含 spc574k_cut
發(fā)表于 01-13 07:44
Floating-Point設(shè)計編碼風格與技巧
有限的數(shù)據(jù)動態(tài)范圍，需要深入的分析來決定整個設(shè)計中間數(shù)據(jù)位寬變化的pattern，為了達到優(yōu)化的QoR，并且要引入很多不同類型的Fixed-Point中間變量。
發(fā)表于 11-22 15:20
?1956次閱讀
如何提高單片機程序執(zhí)行效率
首先什么是執(zhí)行效率。我們平常所說的執(zhí)行效率就是使用相同的算法在相同輸入條件下完成相同計算所產(chǎn)生的系統(tǒng)開銷，目前來說一般會更多關(guān)注執(zhí)行時間方面
發(fā)表于 02-11 15:42
?6次下載
MAX6324CUT29-T PMIC - 監(jiān)控器
電子發(fā)燒友網(wǎng)為你提供Maxim(Maxim)MAX6324CUT29-T相關(guān)產(chǎn)品參數(shù)、數(shù)據(jù)手冊，更有MAX6324CUT29-T的引腳圖、接線圖、封裝手冊、中文資料、英文資料，MAX6324CUT29-T真值表，MAX6324
發(fā)表于 12-12 19:09
MAX6323CUT46-T PMIC - 監(jiān)控器
電子發(fā)燒友網(wǎng)為你提供Maxim(Maxim)MAX6323CUT46-T相關(guān)產(chǎn)品參數(shù)、數(shù)據(jù)手冊，更有MAX6323CUT46-T的引腳圖、接線圖、封裝手冊、中文資料、英文資料，MAX6323CUT46-T真值表，MAX6323
發(fā)表于 12-12 19:13
可以通過降低約束的復(fù)雜度來優(yōu)化Formal的執(zhí)行效率嗎？
我們可以通過降低約束的復(fù)雜度來優(yōu)化Formal的執(zhí)行效率，但是這個主要是通過減少Formal驗證空間來實現(xiàn)的，很容易出現(xiàn)過約，導(dǎo)致bug遺漏。
英特爾推出Hala Point全球最大仿神經(jīng)形態(tài)系統(tǒng)，解決AI效率問題
英特爾實驗室神經(jīng)形態(tài)運算總監(jiān)Mike Davies指出，“當前AI模型訓練及部署成本增長迅速，行業(yè)亟需創(chuàng)新方法。因此，英特爾實驗室研發(fā)了Hala Point，融合深度學習效率、類人腦持續(xù)學習和優(yōu)化功能。
怎么提升單片機代碼執(zhí)行效率
?
提升單片機代碼執(zhí)行效率需要從多個方面入手，包括代碼優(yōu)化、硬件資源利用、編譯器設(shè)置、中斷處理優(yōu)化以及其他技巧等。在實際應(yīng)用中，需要根據(jù)具體需求和硬件條件綜合考慮這些因素，以實現(xiàn)
工商網(wǎng)監(jiān)
評論