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

cutpoint就是更細粒度的黑盒化。

前面我們提到的FEV等價性驗證中的每一個map點都是一個cut point。所以內部能夠map上的點越多，F(xiàn)EV等價性證明的效率越高。 像黑盒化一樣，cutpoint也是一個安全的復雜度優(yōu)化手段，可能會導致假fail，但絕不會引入假pass。因為使用cut point后證明的空間比原來更大了，并且降低了被證明邏輯的復雜度。

在combinational FEV中，所有寄存器的狀態(tài)都是一個cut point。在sequential FEV中，默認只會比較輸出的一致性，如果添加內部某些寄存器狀態(tài)作為map點，可以優(yōu)化FEV的執(zhí)行效率。