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

如果一個DV熟悉simulation驗證，即使他不會formal也不會影響他找到一份不錯的工作。如果一個DV在熟悉simulation驗證的基礎上，又會formal驗證，那他會獲得不錯的加分項，但這還并不足以讓他和前者拉開決定性的差距。

如果一個DV只會formal驗證，那他在大部分公司大概率很難拿到offer，甚至都不會進入到面試環(huán)節(jié)。

以下是論證環(huán)節(jié)，我們以synopsys家的FPV（連接性檢查之類的，本質(zhì)上都系屬FPV的范疇）和DPV兩款formal工具為例。

formal可以對DUT進行全空間輸入的檢查（但也別高興的太早，很多時候需要assume中把很多違規(guī)的激勵場景排除在外，這部分工作可不小），這一點是simulation所不能及的，在多輸入組合，小數(shù)據(jù)深度的RTL驗證中，使用formal無疑是性價比最高的。

但是對大型DUT而言...目前server的算力還遠遠達不到能支持使用foraml的地步，不知哪位大神可以用NVIDIA家的H100優(yōu)化各個engine的計算...屆時看看加速效果如何...

所以，formal的定位就比較尷尬了，在大部分的block level 驗證根本使不上勁，曾經(jīng)嘗試過用FPV對一個數(shù)據(jù)深度大約200個cycle的DUT做形式化驗證，結果跑了30多小時，一個property都沒證明出來，整得我直接吐了。

這種中型規(guī)模的RTL如果用simulation，妥妥的一分鐘能跑十幾個sanity case，所以性價比實在太低。尤其是碰到帶memory的設計，用formal簡直就是噩夢（不過工具好像可以替換掉memory的邏輯，你也可以dummy掉data payload，但控制邏輯的data path同樣不短）。

Formal的風險

formal看上去高大上，但其實就是用另一種方式讓你把RTL又給寫了一遍...本質(zhì)上是在學習設計細節(jié)，這個過程很燒腦的，而且性價比并不高。

simulation在做sign off review的時候，可以列出功能點，驗證計劃，testcase list，coverage這種比較硬核的指標，但如果是用formal，DE那邊除了coverage可以看以外，他會覺得你是不是偷偷把RTL又抄了一遍，這種review的risk是非常高的...

formal蛋疼的點在于，它的檢查是需要精確到cycle base的，這就意味著expected dat的產(chǎn)生同樣需要精確到和dut同一個cycle，你需要對RTL的內(nèi)部實現(xiàn)了如指掌！......用simulation做ref的時候大部分情況只要能保證數(shù)據(jù)完整性就行。所以你可能不是在寫ref，你真的在實現(xiàn)RTL??！奧，你可以說，你用的不是FPV，而且DPV，你的model不是用sv寫的，用的c++，但同學，你在TCL里面同樣需要完成數(shù)據(jù)對齊的工作??！逃不掉的呀！而且，這尼瑪更恐怖。

看到這里明白了吧，formal難以大規(guī)模推廣的難度在于，這東西對DV owner的要求太高了，而且限制條件太多，使用它的投入產(chǎn)出比遠遠低于simulation驗證，所以uvm的培訓班到處都有，但formal的培訓班有幾個人見到過？

Formal的優(yōu)勢

當然了，formal在有些情況下，確實可以事半功倍，比如在soc上做同步邏輯之間的連接性檢查，比如做仲裁，多路選擇，或者cache controller的驗證，亦或是對于計算單元的驗證，以及設計的一致性檢查，formal這種類似于數(shù)學證明式的效率是遠遠高于simulation驗證的，但也僅此而已了。

simulation也好，formal也罷，歸根結底都是工具，是手段，需要根據(jù)不同的場景做選擇。只是目前來看在大多數(shù)情況下，formal并沒有絕對的，不可替代的作用，只能作為simulation的有效補充，提升整體驗證的效率，所以我當時對它的印象就是《神雕》中公孫家的閉穴神功，難練易破，不練也罷。

最后，在國內(nèi)專職做formal enginee的機會可能只有AMD或者NVIDIA有（初創(chuàng)的幾家做處理器芯片的公司可能也會用formal，但是不是專職的不清楚），海思有沒有我不太清楚，可以說國內(nèi)目前95%以上的公司根本用不到formal，是小眾到不能再小眾的領域了。