cut point可優(yōu)化FEV的執(zhí)行效率

cut point就是在模型中指定一個位置，將這個cutpoint的值設(shè)為隨機值，去除這個點前后邏輯的關(guān)聯(lián)性。 需要確認(rèn)這個cut point的設(shè)定不會影響所需要證明的assert，如果影響了可以根據(jù)fail反例定位。 其實，這也類似于一個黑盒，只不過blackbox針對的是一個模塊，將該模塊所有的輸出都設(shè)定為隨機值，而cut point只是將特定的點（信號）設(shè)置為隨機值。 一句話概括：

cutpoint就是更細(xì)粒度的黑盒化。

前面我們提到的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中，默認(rèn)只會比較輸出的一致性，如果添加內(nèi)部某些寄存器狀態(tài)作為map點，可以優(yōu)化FEV的執(zhí)行效率。