防止Formal证明假PASS的办法是什么

在FPV过程中，我们尤其需要注意假PASS，你以为完成了FPV full proven，实际上排除了很多合理的场景，最后得出的full proven是没有意义的。  

也就是说，

FPV主要分成2个部分，assert的证明以及思考我们是否已经覆盖了所有合法的状态空间。

工程师相互检视是一个不错的办法，不过说实话，人太灵活，不够靠谱。我们应该具有更加安全可靠的办法来保证fpv cover和assume的正确性。  

除了人为检视之外，最常用的防止Formal证明假PASS的办法就是将Formal环境中的所有assume和assert都集成在Simulation仿真验证环境中。  

如果某个子模块能够用Formal进行Sign off,那么不建议再开发一个EDA simulation验证环境。但是不可避免地我们会有一个更高level的验证环境，将这些formal assume和assert集成到这个high-level的验证环境即可。  

对于Formal验证环境自身，最好的防止formal假PASS的方式还是多次强调的cover，只有Formal cover覆盖到所有你关心的corner case，你才有足够的交付信心。  

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

审核编辑：刘清