老規矩，先說結論：前（錢）途并不明朗。

如果一個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，是小眾到不能再小眾的領域了。