黑盒的意思是說在FPV證明過程中忽略掉某些子模塊以降低FPV的計(jì)算復(fù)雜性。

當(dāng)一個(gè)模塊被黑盒化時(shí)，它的輸出被視為FPV設(shè)計(jì)的輸入，即它們可以取任何隨機(jī)值。部分模塊的黑盒化對(duì)FPV的性能有著非常巨大的影響，所以在FPV證明的開始應(yīng)該盡量地考慮任何黑盒化的可能。

黑盒化優(yōu)化技術(shù)的一個(gè)好處是保證永遠(yuǎn)不會(huì)誤報(bào)假pass（即本來應(yīng)該fail,結(jié)果證明了所有的屬性都proven了），因?yàn)楹诤谢K使其輸出遍歷了所有值，比實(shí)際設(shè)計(jì)能夠覆蓋的場(chǎng)景更多了。

當(dāng)然，正因?yàn)楹诤谢葘?shí)際設(shè)計(jì)的場(chǎng)景更多了，所有可能出現(xiàn)假fail，這個(gè)時(shí)候需要定位問題所在，然后非常慎重地增加相應(yīng)的約束。

針對(duì)不同的FPV目的，很多常見的模塊邏輯都應(yīng)該被黑盒化。例如，memory的狀態(tài)空間非常巨大，對(duì)于FPV工具來說很難全部覆蓋而且數(shù)據(jù)的索引特性一般也不會(huì)是corner case，所以在某些不受影響的特性證明上是可以被黑盒化的。

一般來說，在計(jì)劃運(yùn)行 FPV 工具之前，可以考慮黑盒化下列幾個(gè)模塊：

memory和cache

復(fù)雜算法模塊，例如乘法器、除法器、復(fù)雜函數(shù)或浮點(diǎn)邏輯

模擬電路

外部提供的（經(jīng)過驗(yàn)證的）IP

審核編輯：劉清