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

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

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

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

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

上述兩個問題用Formal就可以很好的解決掉。

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

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

下面是一個簡單的例子，當設(shè)計如下

我們可以通過下面描述來驗證該段邏輯,先驗證req_valid 為高時，dataout等于datain；

再驗證req_valid 為低時，dataout等于0。

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

審核編輯：劉清