這里的Formal是formality/LEC 嗎？不是。那這里的Formal是什么？

SOC V2.0里的Formal是形式驗(yàn)證。

形式驗(yàn)證不同于仿真驗(yàn)證，它是通過數(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)算是類似一種丟飛鏢的過程，想要驗(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í)，通過動(dòng)態(tài)仿真也是很難覆蓋到所有路徑的。

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

在處芯積律SOC V2的項(xiàng)目里面，提供了一個(gè)用Formal 驗(yàn)證PIN MUX 的案例。

通過實(shí)際例子讓大家感受 Formal 環(huán)境長(zhǎng)什么樣？Formal是怎么驗(yàn)證的。

除了 Formal ，SOC V2 項(xiàng)目還有什么？

No1. 有DMA，ISP，PINMUX這些模塊

審核編輯：劉清