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

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

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

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

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

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

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

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

Formal的風(fēng)險(xiǎn)

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

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

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

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

Formal的優(yōu)勢

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

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

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