最近看到行業(yè)群里面經(jīng)常有人問(wèn)什么是形式驗(yàn)證，今天的文章和大家介紹下形式驗(yàn)證(Formal verification)。

相信很多人已經(jīng)接觸過(guò)驗(yàn)證。如我前面有篇文章所寫(xiě)驗(yàn)證分為IP驗(yàn)證，FPGA驗(yàn)證，SOC驗(yàn)證和CPU驗(yàn)證，這其中大部分是采用動(dòng)態(tài)仿真(dynamic simulation)實(shí)現(xiàn)，即通過(guò)給定設(shè)計(jì)(design)端口測(cè)試激勵(lì)，結(jié)合時(shí)間消耗判斷設(shè)計(jì)的輸出結(jié)果是否符合預(yù)期。動(dòng)態(tài)仿真又分為定向測(cè)試和隨機(jī)測(cè)試。現(xiàn)在很多公司用的UVM驗(yàn)證方法學(xué)便是建立在動(dòng)態(tài)仿真的基礎(chǔ)上的。

形式驗(yàn)證不同于仿真驗(yàn)證，它是通過(guò)數(shù)學(xué)上完備地證明或驗(yàn)證電路的實(shí)現(xiàn)方法是否確實(shí)實(shí)現(xiàn)了電路設(shè)計(jì)所描述的功能。形式驗(yàn)證方法分為等價(jià)性檢查(equivalence checking)如Formality，LEC等和屬性檢查(Property checking)如Jasper gold，VC Formal 等。我們這里講的形式驗(yàn)證特指屬性的檢查(Property checking)。

如上圖所示，在一個(gè)簡(jiǎn)單的加法設(shè)計(jì)中，我們采用動(dòng)態(tài)仿真的方式去驗(yàn)證上述運(yùn)算是類(lèi)似一種丟飛鏢的過(guò)程，想要驗(yàn)到所有的場(chǎng)景要運(yùn)行2的64次方即18446744073709551616次，這只是簡(jiǎn)單的加法運(yùn)算，如果再加入其它稍微復(fù)雜的邏輯，想用動(dòng)態(tài)仿真的方式打完所有情況是非常困難的。

另外一種場(chǎng)景是當(dāng)信號(hào)從設(shè)計(jì)的端口輸入，信號(hào)流的走向會(huì)根據(jù)不同設(shè)定或者狀態(tài)選擇走向不同的路徑。如上圖所示，當(dāng)信號(hào)流可選擇的路徑很多時(shí)，通過(guò)動(dòng)態(tài)仿真也是很難覆蓋到所有路徑的。

上述兩個(gè)問(wèn)題用Formal就可以很好的解決掉。

除了功能驗(yàn)證上的使用，F(xiàn)ormal也可以被用在coverage的收集上。在設(shè)計(jì)里面有不少代碼是無(wú)法執(zhí)行到的。如果用動(dòng)態(tài)仿真去找這些點(diǎn)，一般的做法是跑大量的回歸測(cè)試（regression），收集coverage，然后針對(duì)沒(méi)打到的coverage hole找designer去review。整個(gè)過(guò)程走下來(lái)會(huì)花費(fèi)不少人力。而用formal可以比較輕松高效的找到其中的一些點(diǎn)。

介紹了這么多，那么Formal是怎么實(shí)現(xiàn)的呢？用Formal驗(yàn)證需要輸入設(shè)計(jì)(design)，約束(constraint)和待驗(yàn)證的property。這里的設(shè)計(jì)一般是指RTL，約束指的是assumption，clock，reset等，propert是指assertion。

下面是一個(gè)簡(jiǎn)單的例子，當(dāng)設(shè)計(jì)如下

我們可以通過(guò)下面描述來(lái)驗(yàn)證該段邏輯,先驗(yàn)證req_valid 為高時(shí)，dataout等于datain；

再驗(yàn)證req_valid 為低時(shí)，dataout等于0。

Formal適合所有驗(yàn)證場(chǎng)景嗎？當(dāng)然不是，因?yàn)閒ormal是通過(guò)數(shù)學(xué)運(yùn)算去完成完備性驗(yàn)證，在一些簡(jiǎn)單的邏輯如arbiter，muxes，F(xiàn)SM，Control logic上比較適合用formal去驗(yàn)證，但是對(duì)一些復(fù)雜的場(chǎng)景，比如涉及到大量的memory，復(fù)雜的總線傳輸，多模塊協(xié)助工作等場(chǎng)景都不太適合用Formal。

審核編輯：劉清