By definition, formal verification is the use of tools that mathematically analyze the space of possible behaviors of a design, rather than computing results for particular values.

形式驗證在IC flow有兩種常用的看起來相差甚多的領域：

• 模型檢查（model checking）：檢查RTL是否滿足設計規范，典型產品如JasperGold
• 等價性檢查（equivalence checking）：檢查兩個design是否等價，可以是RTL和RTL之間、RTL和netlist之間或者兩個netlist之間，典型產品如Synopsys的formality和Cadence的Conformal LEC

既然都是形式驗證的范疇，那必然會有一些共性的東西。它們的背后都有一系列數學工具在支撐，比如binary decision diagrams。從理解角度，不嚴格地考慮，二者都是力求遍歷所有可能的輸入，來檢查對應的輸出是否滿足目標。當然，實際實現上不可能簡單實用窮舉，EDA工具都有很多數學模型可以使用，以解決各類問題。比如對于一個加法器，如何進行model checking和equivalence checking？如果窮舉那效率太低了，我們可以根據design使用諸如AIG（and-inv graph）等手段把function抽取出來，和model或其他design進行比較。

其實formality和Conformal LEC只涵蓋了等價性檢查的一方面（CEC），equivalence checking還有一種更強大的手段：SEC，只是這個手段在IC flow中并未普及。這方面的工具有Cadence旗下的JasperGold SEC和和Mentor的SEC工具Questa SLEC。

RTL的function的形式驗證除了model checking，還有一種手段是定理證明（Theorem proving），對純計算邏輯會比較有用。

1. Model checking

Formal verification, in contrast to testing, uses rigorous mathematical reasoning to show that a design meets all or parts of its specification.

提到形式驗證的model checking，繞不開和傳統的仿真驗證方式的比較。仿真驗證依靠施加各種類型的激勵，以盡量高的覆蓋我們想驗證的邏輯功能。這種方法自然coverage很難達到100%，而形式驗證理論上是可以達到100% coverage的。

那model是怎么來的呢？model是根據design specification寫出來的，具體形式可以是用形如SVA表達的ssertion集合（當然還有其他的表達工具）。

本質上講，model checking的工具使用各種數學手段來試圖證明你的design能完全match你寫的assertion，如果不能，那么就是找到bug了。當然了，根據specification寫出assertion也是一個挑戰。

Model checking在IC flow中是對simulation方式的一個補充，使用的流行度無法和基于UVM的simulation相比。

2. Theorem proving

Theorem proving也是一種驗證RTL功能和model是否match的手段。顧名思義，它使用的是推導的方法。不像model checking是工具自動給的激勵來和assertion匹配，定理證明則是用純數學方法了。它們之間有一點是共通的，就是都是和根據design specification寫的model來比，model checking用assertion表達model，而theorem proving則是用某種中間語言來表達。

用來進行theorem proving最有名的工具語言算是ACL2了。

ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. "ACL2" denotes "A Computational Logic for Applicative Common Lisp".

Intel和AMD都拿ACL2來驗證他們的浮點數乘法器。驗證過程是類似這樣的：

Theorem proving使用的范圍比較窄，所以在IC flow中并不常見。

3. Equivalence checking

顧名思義，等價性檢查就是看兩個design是否等價。像我們常用的Synopsys的formality或者Cadence的Conformal LEC使用的是給定參考狀態（擁有match步驟）的combinational equivalence checking（CEC），針對的是同一個design的不同實現階段。還有可以針對內部狀態不match情況下的等價性檢查，比如經過retimed, pipeline重排后的design。

3.1 Combinational equivalence checking

等價性檢查（Equivalence checking）可以用在IC流程的各個階段。

除了上圖提到的使用場景外，RTL和RTL進行比對也是一項很有用的功能。比如我們對一個模塊優化timing，又不想重新跑regression，我們可以比對優化前后的RTL是否等價來進行驗證。

我們知道，equivalence checking工具如formality有個步驟叫match，用于match兩個design里的參考點，這些參考點和STA里使用的類似，為flip-flop和IO，然后再進行verify。這是很容易理解的，工具把整個等價性檢查工具拆分為一系列兩個參考點之間的組合邏輯的等價性驗證，可以讓整個工作高效完成。當然，這只是簡單的易于理解的說法，實際上里面會有很多的加速手段。

CEC在IC flow中是標配，即是工程師口中狹義的形式驗證，沒有聽說過不用的。

3.2 SEC與形式驗證的統一

實際上formal equivalence checking工具不止于此。上面說到的conception其實稱為combinational equivalence checking (CEC)，還有一種是sequential equivalence checking (SEC)。SEC可以對兩個時序邏輯設計進行比對，它可能使用BDD等symbolic算法來對設計的狀態空間進行表述，這也就演變為了model checking問題，所以SEC通常會使用更高抽象層級的reference model，這個思想和驗證RTL功能的model checking和theorem proving就有明顯的共通之處了。

JasperGold SEC工具就是做這個工作的。當然SEC主要就是針對RTL對RTL了。我們可以把SEC工具看做model checking的一個特例，這里model不是assertion，而是另一個design，甚至可以是一個周期精確的model，從這點看是不是很像theorem proving實現的功能呢？

可以想象SEC的計算復雜度很高，在不可實現的實現我們通常可以尋求bounded equivalence checking（BEC）的幫助，我們把vector sequence的長度作一個限制，去證明在這個長度以內兩個design是等價的。

BEC作為SEC的一個實現手段，自然也可以用于RTL function的model checking。SEC在IC flow中并未普及，IC flow中通常的使用場景都可以用CEC解決。

4. 小結

我們可以看到各種formal verification 手段殊途同歸到design implementation和reference model（不管是assertion， RTL ，netlist還是電路的其他中間形式表達）的比對上。

從各種形式驗證手段背后思想、算法的角度來看，不管model checking、theorem proving還是equivalence checking它們之間其實還是一致的，很多concept和algorithm可以共享。

總結

以上是生活随笔為你收集整理的uvm 形式验证_谈一谈IC flow中的形式验证的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。