黑盒化技術(shù)簡化FPV計算復(fù)雜性

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

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

黑盒化優(yōu)化技術(shù)的一個好處是保證永遠不會誤報假pass（即本來應(yīng)該fail,結(jié)果證明了所有的屬性都proven了），因為黑盒化模塊使其輸出遍歷了所有值，比實際設(shè)計能夠覆蓋的場景更多了。

當(dāng)然，正因為黑盒化比實際設(shè)計的場景更多了，所有可能出現(xiàn)假fail，這個時候需要定位問題所在，然后非常慎重地增加相應(yīng)的約束。

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

一般來說，在計劃運行 FPV 工具之前，可以考慮黑盒化下列幾個模塊：

memory和cache

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

模擬電路

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

審核編輯：劉清