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

在FPV過(guò)程中，我們尤其需要注意假PASS，你以為完成了FPV full proven，實(shí)際上排除了很多合理的場(chǎng)景，最后得出的full proven是沒(méi)有意義的。

也就是說(shuō)，

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

工程師相互檢視是一個(gè)不錯(cuò)的辦法，不過(guò)說(shuō)實(shí)話，人太靈活，不夠靠譜。我們應(yīng)該具有更加安全可靠的辦法來(lái)保證fpv cover和assume的正確性。

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

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

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

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

審核編輯：劉清