有没有人在使用IFV的？

cadence的Incisive Formal Verifier，
感觉对于比较简单的protocol比较好用，比较复杂的，就挺难用了。
有没有人在使用的?希望能交流一下。

好用不好用和这个tool无关吧
formal的验证方法，本质上讲基本都是基于model check的原理来实现的，eda tool做的事情也就是如何最大可能的提高运算效率，降低复杂度
对于使用者，无非就是尽可能的把你要验证的模块的property写的清楚一些罢了

In my opinion, it's not very pratical to use IFV.
First, you suffer some $ to get the lic, ;-)
Sec, for complicated designs it's always slow and always prone to abort during run-time.(as you said)
Third, there are several alternative ways I can think:
e.g.
1) You can write your own assertion IP instead of IFV assertion IP;
2) You can generate your own stimulus(like using C, system verilog) instead of IFV stimulus;
However, if you found it's easy for simple protocol, go ahead ;-)

niubia

感觉还是仿真比较有用。

做过大工程 你看你用Formal验证还是Simulation Formal有两种一种是MC一种是SEC不仅仅是比对那么简单毫不，没受过训练，和培训根本不能说会IFV顶多算是能够启动做几个简单的样例。IFV技巧和逻辑性需要非常强的的功底。