數(shù)字驗(yàn)證中Formal Verification在國(guó)內(nèi)的應(yīng)用以及前景如何？

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

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

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

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

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

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

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

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

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

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

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

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

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

Formal的優(yōu)勢(shì)

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

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

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