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.

形式驗(yàn)證在IC flow有兩種常用的看起來(lái)相差甚多的領(lǐng)域：

• 模型檢查（model checking）：檢查RTL是否滿足設(shè)計(jì)規(guī)范，典型產(chǎn)品如JasperGold
• 等價(jià)性檢查（equivalence checking）：檢查兩個(gè)design是否等價(jià)，可以是RTL和RTL之間、RTL和netlist之間或者兩個(gè)netlist之間，典型產(chǎn)品如Synopsys的formality和Cadence的Conformal LEC

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

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

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

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.

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

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

本質(zhì)上講，model checking的工具使用各種數(shù)學(xué)手段來(lái)試圖證明你的design能完全match你寫的assertion，如果不能，那么就是找到bug了。當(dāng)然了，根據(jù)specification寫出assertion也是一個(gè)挑戰(zhàn)。

Model checking在IC flow中是對(duì)simulation方式的一個(gè)補(bǔ)充，使用的流行度無(wú)法和基于UVM的simulation相比。

2. Theorem proving

Theorem proving也是一種驗(yàn)證RTL功能和model是否match的手段。顧名思義，它使用的是推導(dǎo)的方法。不像model checking是工具自動(dòng)給的激勵(lì)來(lái)和assertion匹配，定理證明則是用純數(shù)學(xué)方法了。它們之間有一點(diǎn)是共通的，就是都是和根據(jù)design specification寫的model來(lái)比，model checking用assertion表達(dá)model，而theorem proving則是用某種中間語(yǔ)言來(lái)表達(dá)。

用來(lái)進(jìn)行theorem proving最有名的工具語(yǔ)言算是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來(lái)驗(yàn)證他們的浮點(diǎn)數(shù)乘法器。驗(yàn)證過(guò)程是類似這樣的：

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

3. Equivalence checking

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

3.1 Combinational equivalence checking

等價(jià)性檢查（Equivalence checking）可以用在IC流程的各個(gè)階段。

除了上圖提到的使用場(chǎng)景外，RTL和RTL進(jìn)行比對(duì)也是一項(xiàng)很有用的功能。比如我們對(duì)一個(gè)模塊優(yōu)化timing，又不想重新跑regression，我們可以比對(duì)優(yōu)化前后的RTL是否等價(jià)來(lái)進(jìn)行驗(yàn)證。

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

CEC在IC flow中是標(biāo)配，即是工程師口中狹義的形式驗(yàn)證，沒(méi)有聽(tīng)說(shuō)過(guò)不用的。

3.2 SEC與形式驗(yàn)證的統(tǒng)一

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

JasperGold SEC工具就是做這個(gè)工作的。當(dāng)然SEC主要就是針對(duì)RTL對(duì)RTL了。我們可以把SEC工具看做model checking的一個(gè)特例，這里model不是assertion，而是另一個(gè)design，甚至可以是一個(gè)周期精確的model，從這點(diǎn)看是不是很像theorem proving實(shí)現(xiàn)的功能呢？

可以想象SEC的計(jì)算復(fù)雜度很高，在不可實(shí)現(xiàn)的實(shí)現(xiàn)我們通常可以尋求bounded equivalence checking（BEC）的幫助，我們把vector sequence的長(zhǎng)度作一個(gè)限制，去證明在這個(gè)長(zhǎng)度以內(nèi)兩個(gè)design是等價(jià)的。

BEC作為SEC的一個(gè)實(shí)現(xiàn)手段，自然也可以用于RTL function的model checking。SEC在IC flow中并未普及，IC flow中通常的使用場(chǎng)景都可以用CEC解決。

4. 小結(jié)

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

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

總結(jié)

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

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。