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

SOC V2.0里的Formal是形式驗證。

形式驗證不同于仿真驗證，它是通過數學上完備地證明或驗證電路的實現方法是否確實實現了電路設計所描述的功能。

形式驗證方法分為等價性檢查(equivalence checking)如Formality，LEC等和屬性檢查(Property checking)如Jasper gold，VC Formal 等。

我們這里講的形式驗證特指屬性的檢查(Property checking)。

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

另外一種場景是當信號從設計的端口輸入，信號流的走向會根據不同設定或者狀態選擇走向不同的路徑。

如上圖所示，當信號流可選擇的路徑很多時，通過動態仿真也是很難覆蓋到所有路徑的。

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

在處芯積律SOC V2的項目里面，提供了一個用Formal 驗證PIN MUX 的案例。

通過實際例子讓大家感受 Formal 環境長什么樣？Formal是怎么驗證的。

除了 Formal ，SOC V2 項目還有什么？

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

審核編輯：劉清