cut point就是在模型中指定一個位置,將這個cutpoint的值設為隨機值,去除這個點前后邏輯的關聯性。 需要確認這個cut point的設定不會影響所需要證明的assert,如果影響了可以根據fail反例定位。 其實,這也類似于一個黑盒,只不過blackbox針對的是一個模塊,將該模塊所有的輸出都設定為隨機值,而cut point只是將特定的點(信號)設置為隨機值。 一句話概括:
cutpoint就是更細粒度的黑盒化。
前面我們提到的FEV等價性驗證中的每一個map點都是一個cut point。所以內部能夠map上的點越多,FEV等價性證明的效率越高。 像黑盒化一樣,cutpoint也是一個安全的復雜度優化手段,可能會導致假fail,但絕不會引入假pass。因為使用cut point后證明的空間比原來更大了,并且降低了被證明邏輯的復雜度。
在combinational FEV中,所有寄存器的狀態都是一個cut point。在sequential FEV中,默認只會比較輸出的一致性,如果添加內部某些寄存器狀態作為map點,可以優化FEV的執行效率。
-
寄存器
+關注
關注
31文章
5424瀏覽量
123502 -
模型
+關注
關注
1文章
3499瀏覽量
50059
原文標題:FPV復雜度優化之cut point
文章出處:【微信號:芯片驗證工程師,微信公眾號:芯片驗證工程師】歡迎添加關注!文章轉載請注明出處。
發布評論請先 登錄

新一代CUT75系列PCB基板式開關電源問世
常用優化編譯選項對ARM平臺的影響
SPC574K7x的CUT 2.3和CUT 2.4之間有什么區別?
Floating-Point設計編碼風格與技巧
如何提高單片機程序執行效率

可以通過降低約束的復雜度來優化Formal的執行效率嗎?
英特爾推出Hala Point全球最大仿神經形態系統,解決AI效率問題
怎么提升單片機代碼執行效率
制造執行系統MES:提升企業生產管理的效率與優化生產過程

評論