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

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

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

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