防止Formal證明假PASS的辦法是什么

在FPV過程中，我們尤其需要注意假PASS，你以為完成了FPV full proven，實際上排除了很多合理的場景，最后得出的full proven是沒有意義的。

也就是說，

FPV主要分成2個部分，assert的證明以及思考我們是否已經(jīng)覆蓋了所有合法的狀態(tài)空間。

工程師相互檢視是一個不錯的辦法，不過說實話，人太靈活，不夠靠譜。我們應該具有更加安全可靠的辦法來保證fpv cover和assume的正確性。

除了人為檢視之外，最常用的防止Formal證明假PASS的辦法就是將Formal環(huán)境中的所有assume和assert都集成在Simulation仿真驗證環(huán)境中。

如果某個子模塊能夠用Formal進行Sign off,那么不建議再開發(fā)一個EDA simulation驗證環(huán)境。但是不可避免地我們會有一個更高level的驗證環(huán)境，將這些formal assume和assert集成到這個high-level的驗證環(huán)境即可。

對于Formal驗證環(huán)境自身，最好的防止formal假PASS的方式還是多次強調的cover，只有Formal cover覆蓋到所有你關心的corner case，你才有足夠的交付信心。

使用formal進行交付，需要再次明確的是，sva cover比sva assert更加重要。