数字验证中Formal Verification在国内的应用以及前景如何？

老规矩，先说结论：前（钱）途并不明朗。

如果一个DV熟悉simulation验证，即使他不会formal也不会影响他找到一份不错的工作。如果一个DV在熟悉simulation验证的基础上，又会formal验证，那他会获得不错的加分项，但这还并不足以让他和前者拉开决定性的差距。

如果一个DV只会formal验证，那他在大部分公司大概率很难拿到offer，甚至都不会进入到面试环节。

以下是论证环节，我们以synopsys家的FPV（连接性检查之类的，本质上都系属FPV的范畴）和DPV两款formal工具为例。

formal可以对DUT进行全空间输入的检查（但也别高兴的太早，很多时候需要assume中把很多违规的激励场景排除在外，这部分工作可不小），这一点是simulation所不能及的，在多输入组合，小数据深度的RTL验证中，使用formal无疑是性价比最高的。

但是对大型DUT而言...目前server的算力还远远达不到能支持使用foraml的地步，不知哪位大神可以用NVIDIA家的H100优化各个engine的计算...届时看看加速效果如何...

所以，formal的定位就比较尴尬了，在大部分的block level 验证根本使不上劲，曾经尝试过用FPV对一个数据深度大约200个cycle的DUT做形式化验证，结果跑了30多小时，一个property都没证明出来，整得我直接吐了。

这种中型规模的RTL如果用simulation，妥妥的一分钟能跑十几个sanity case，所以性价比实在太低。尤其是碰到带memory的设计，用formal简直就是噩梦（不过工具好像可以替换掉memory的逻辑，你也可以dummy掉data payload，但控制逻辑的data path同样不短）。

Formal的风险

formal看上去高大上，但其实就是用另一种方式让你把RTL又给写了一遍...本质上是在学习设计细节，这个过程很烧脑的，而且性价比并不高。

simulation在做sign off review的时候，可以列出功能点，验证计划，testcase list，coverage这种比较硬核的指标，但如果是用formal，DE那边除了coverage可以看以外，他会觉得你是不是偷偷把RTL又抄了一遍，这种review的risk是非常高的...

formal蛋疼的点在于，它的检查是需要精确到cycle base的，这就意味着expected dat的产生同样需要精确到和dut同一个cycle，你需要对RTL的内部实现了如指掌！......用simulation做ref的时候大部分情况只要能保证数据完整性就行。所以你可能不是在写ref，你真的在实现RTL啊！奥，你可以说，你用的不是FPV，而且DPV，你的model不是用sv写的，用的c++，但同学，你在TCL里面同样需要完成数据对齐的工作啊！逃不掉的呀！而且，这尼玛更恐怖。

看到这里明白了吧，formal难以大规模推广的难度在于，这东西对DV owner的要求太高了，而且限制条件太多，使用它的投入产出比远远低于simulation验证，所以uvm的培训班到处都有，但formal的培训班有几个人见到过？

Formal的优势

当然了，formal在有些情况下，确实可以事半功倍，比如在soc上做同步逻辑之间的连接性检查，比如做仲裁，多路选择，或者cache controller的验证，亦或是对于计算单元的验证，以及设计的一致性检查，formal这种类似于数学证明式的效率是远远高于simulation验证的，但也仅此而已了。

simulation也好，formal也罢，归根结底都是工具，是手段，需要根据不同的场景做选择。只是目前来看在大多数情况下，formal并没有绝对的，不可替代的作用，只能作为simulation的有效补充，提升整体验证的效率，所以我当时对它的印象就是《神雕》中公孙家的闭穴神功，难练易破，不练也罢。

最后，在国内专职做formal enginee的机会可能只有AMD或者NVIDIA有（初创的几家做处理器芯片的公司可能也会用formal，但是不是专职的不清楚），海思有没有我不太清楚，可以说国内目前95%以上的公司根本用不到formal，是小众到不能再小众的领域了。