形式驗(yàn)證如何加速超大規(guī)模芯片設(shè)計(jì)？

引言

隨著集成電路規(guī)模的不斷擴(kuò)大，從設(shè)計(jì)到流片（Tape-out）的全流程中，驗(yàn)證環(huán)節(jié)的核心地位日益凸顯。有效的驗(yàn)證不僅是設(shè)計(jì)完美的基石，更是確保電路在實(shí)際應(yīng)用中穩(wěn)定運(yùn)行的保障。尤為關(guān)鍵的是，邏輯或功能錯(cuò)誤是導(dǎo)致流片失敗的首要原因，占比高達(dá)50%。功能驗(yàn)證正是解決這一難題的利器，它助力工程師精準(zhǔn)識(shí)別邏輯設(shè)計(jì)漏洞、性能不達(dá)標(biāo)問題以及設(shè)計(jì)代碼中的功能缺陷，從而最大限度地規(guī)避流片風(fēng)險(xiǎn)。

針對(duì)超大規(guī)模集成電路（VLSI）設(shè)計(jì)，目前功能驗(yàn)證有兩種方法：動(dòng)態(tài)仿真驗(yàn)證和形式驗(yàn)證（Formal Verification）。形式驗(yàn)證采用數(shù)學(xué)方法來比較原設(shè)計(jì)和修改設(shè)計(jì)之間的邏輯功能的異同，而動(dòng)態(tài)仿真驗(yàn)證是對(duì)兩設(shè)計(jì)施加相同的激勵(lì)后，觀測(cè)電路對(duì)激勵(lì)的反應(yīng)異同。

面對(duì)大型設(shè)計(jì)，傳統(tǒng)的動(dòng)態(tài)仿真驗(yàn)證方法在覆蓋率和效率上面臨挑戰(zhàn)。為了達(dá)到100%的覆蓋率，動(dòng)態(tài)仿真驗(yàn)證所需要的矢量就會(huì)越多，這時(shí)形式驗(yàn)證在這方面就有優(yōu)勢(shì)了，成為現(xiàn)代IC設(shè)計(jì)驗(yàn)證流程中的關(guān)鍵一環(huán)。本文就以 “芯天成EsseFCEC”工具為例，來介紹形式驗(yàn)證的流程和基本概念。

什么是形式驗(yàn)證

形式驗(yàn)證是一種基于嚴(yán)格數(shù)學(xué)推理的設(shè)計(jì)驗(yàn)證技術(shù)，它摒棄了物理測(cè)試與模擬的依賴，專注于通過靜態(tài)、全面的邏輯分析來確保設(shè)計(jì)的正確性。此方法顯著降低了對(duì)龐大測(cè)試集的需求，并力求實(shí)現(xiàn)接近完美的驗(yàn)證覆蓋率。

形式驗(yàn)證作為EDA、數(shù)學(xué)及編程語(yǔ)言等多學(xué)科交叉的產(chǎn)物，自上世紀(jì)90年代起便嶄露頭角，最初應(yīng)用于RTL代碼與門級(jí)網(wǎng)表的LEC（邏輯等價(jià)性檢查），隨后逐步擴(kuò)展到各類EDA工具，以應(yīng)對(duì)不同驗(yàn)證場(chǎng)景的需求。

目前，形式驗(yàn)證主要分為兩個(gè)技術(shù)方向：等價(jià)性檢查和屬性檢查。其中。等價(jià)性檢查，作為核心驗(yàn)證手段，通過對(duì)比功能驗(yàn)證后的HDL設(shè)計(jì)與綜合后的網(wǎng)表功能，確保兩者在功能層面上的完全一致，從而保證門級(jí)電路與寄存器傳輸級(jí)（Register Transfer Level, RTL）模型之間的一致性。這一方法有效防范了綜合工具潛在的缺陷及人為誤操作，對(duì)于提升設(shè)計(jì)質(zhì)量至關(guān)重要。

形式驗(yàn)證的實(shí)施涉及多個(gè)關(guān)鍵環(huán)節(jié)：

屬性定義（Properties）：精確闡述設(shè)計(jì)需遵循的特性與規(guī)范，涵蓋時(shí)序邏輯、狀態(tài)轉(zhuǎn)換規(guī)則及各項(xiàng)約束條件。

規(guī)約語(yǔ)言：采用如SystemVerilog Assertions（SVA）、Property Specification Language（PSL）等形式化規(guī)約語(yǔ)言，將屬性與約束轉(zhuǎn)化為可驗(yàn)證的表達(dá)式。

定理證明器（Theorem Provers）：依托形式化邏輯與推理機(jī)制，自動(dòng)驗(yàn)證屬性是否成立，為設(shè)計(jì)邏輯的正確性提供堅(jiān)實(shí)保障。

模型檢查器（Model Checkers）：全面探索系統(tǒng)狀態(tài)空間，尋找可能違反預(yù)定性質(zhì)的執(zhí)行路徑，確保設(shè)計(jì)在所有可能情況下均能滿足既定要求。

形式驗(yàn)證的基本流程是一個(gè)連貫且系統(tǒng)化的過程。這一過程從明確驗(yàn)證目標(biāo)開始，設(shè)計(jì)團(tuán)隊(duì)首先需要界定哪些部分或功能需要接受形式驗(yàn)證的嚴(yán)格審查。接著，采用形式規(guī)約語(yǔ)言（如SystemVerilog Assertions、PSL）定義屬性和規(guī)約，作為驗(yàn)證基礎(chǔ)。進(jìn)入驗(yàn)證環(huán)境配置階段，團(tuán)隊(duì)選擇適合的驗(yàn)證工具（定理證明器、模型檢查器），并依據(jù)設(shè)計(jì)特性和需求進(jìn)行優(yōu)化配置，以確保驗(yàn)證效率與準(zhǔn)確性。

驗(yàn)證執(zhí)行為核心，定理證明器通過數(shù)學(xué)推理驗(yàn)證屬性與規(guī)約的正確性，模型檢查器則全面探索系統(tǒng)狀態(tài)空間，檢查違規(guī)執(zhí)行序列。驗(yàn)證結(jié)束后，團(tuán)隊(duì)分析驗(yàn)證結(jié)果，識(shí)別并修正設(shè)計(jì)中的錯(cuò)誤或不一致。此過程可能多次迭代，直至設(shè)計(jì)完全符合驗(yàn)證要求。

形式驗(yàn)證工具的挑戰(zhàn)

形式驗(yàn)證的流程雖然復(fù)雜且嚴(yán)謹(jǐn)，但它為設(shè)計(jì)團(tuán)隊(duì)提供了一種高效且可靠的驗(yàn)證方法。通過遵循這一流程，設(shè)計(jì)團(tuán)隊(duì)可以顯著降低設(shè)計(jì)錯(cuò)誤的風(fēng)險(xiǎn)，提高產(chǎn)品的質(zhì)量和可靠性。然而，隨著現(xiàn)代芯片設(shè)計(jì)的復(fù)雜性和規(guī)模不斷增長(zhǎng)，形式驗(yàn)證在實(shí)際應(yīng)用中面臨多重挑戰(zhàn)：

復(fù)雜性增加，性能不足：現(xiàn)代芯片設(shè)計(jì)的復(fù)雜性和規(guī)模不斷增長(zhǎng)，對(duì)驗(yàn)證工具的性能提出了更高要求。現(xiàn)有工具在處理大規(guī)模設(shè)計(jì)時(shí)可能面臨性能瓶頸，導(dǎo)致驗(yàn)證過程耗時(shí)過長(zhǎng)。

多樣化的設(shè)計(jì)環(huán)境：不同的設(shè)計(jì)團(tuán)隊(duì)可能使用不同的設(shè)計(jì)語(yǔ)言和平臺(tái)，這要求驗(yàn)證工具具備廣泛的兼容性和集成能力。然而，多樣化的設(shè)計(jì)環(huán)境可能導(dǎo)致兼容性和集成性方面的挑戰(zhàn)。

可擴(kuò)展性需求增加：隨著技術(shù)的不斷進(jìn)步和新的設(shè)計(jì)需求的出現(xiàn)，驗(yàn)證工具需要具備良好的可擴(kuò)展性，以快速適應(yīng)新的設(shè)計(jì)規(guī)范和標(biāo)準(zhǔn)。這對(duì)工具的開發(fā)和維護(hù)提出了更高要求。

復(fù)雜的設(shè)計(jì)錯(cuò)誤檢測(cè)：在復(fù)雜的設(shè)計(jì)中，子系統(tǒng)之間的交互和邏輯路徑可能非常復(fù)雜，驗(yàn)證工具需要能夠準(zhǔn)確地檢測(cè)這些復(fù)雜場(chǎng)景中的錯(cuò)誤和不一致之處。這要求工具具備強(qiáng)大的錯(cuò)誤檢測(cè)能力和智能化的分析手段。

芯天成EsseFormal形式驗(yàn)證軟件

芯天成EsseFormal形式驗(yàn)證軟件是一款功能全面的驗(yàn)證解決方案，專為數(shù)字芯片設(shè)計(jì)領(lǐng)域的復(fù)雜驗(yàn)證挑戰(zhàn)而設(shè)計(jì)。其核心包含五種工具套件，每一種都針對(duì)特定的驗(yàn)證需求提供高效、精準(zhǔn)的支持。

EsseFECT（形式化等價(jià)性驗(yàn)證）：該工具專注于驗(yàn)證C-to-RTL的轉(zhuǎn)換過程中，設(shè)計(jì)的等價(jià)性是否得以保持。這確保了設(shè)計(jì)在不同抽象層次間的轉(zhuǎn)換無(wú)誤，是確保設(shè)計(jì)一致性的重要環(huán)節(jié)。

EsseFCEC（組合邏輯等價(jià)性驗(yàn)證）：作為EsseFormal的明星產(chǎn)品，EsseFCEC專門用于驗(yàn)證芯片設(shè)計(jì)中各電路模塊之間的組合邏輯等價(jià)性。它不僅支持RTL到Netlist的轉(zhuǎn)換驗(yàn)證，還涵蓋版本間差異的比較，確保設(shè)計(jì)更改不會(huì)引入錯(cuò)誤。其強(qiáng)大的綜合優(yōu)化技術(shù)支持（如Clock-gating、multibit register banking和FSM recoding）顯著提升了驗(yàn)證效率和性能。此外，對(duì)DesignWare元件庫(kù)的支持以及大位寬datapath驗(yàn)證的能力，進(jìn)一步拓寬了EsseFCEC的應(yīng)用范圍。

EsseFPV（模型檢查）：通過遍歷設(shè)計(jì)的狀態(tài)空間，EsseFPV能夠發(fā)現(xiàn)設(shè)計(jì)中可能存在的違反預(yù)定義屬性的行為，是確保設(shè)計(jì)行為符合預(yù)期的關(guān)鍵工具。

EsseCC與EsseUNR（實(shí)用驗(yàn)證Apps）：這兩個(gè)工具提供了額外的實(shí)用功能。EsseCC是一個(gè)高效的連接性檢查驗(yàn)證工具，為用戶提供快速的錯(cuò)誤檢測(cè)以及信號(hào)到信號(hào)的預(yù)期設(shè)計(jì)行為驗(yàn)證。EsseCC以RTL電路和連接規(guī)范作為輸入，快速檢查設(shè)計(jì)是否符合連接規(guī)范。而EsseUNR是一款高效的覆蓋不可達(dá)性檢查工具。使用傳統(tǒng)的驗(yàn)證方式，在驗(yàn)證后期，通過編寫測(cè)試用例提升驗(yàn)證覆蓋率的難度陡然上升。該工具具有更高效、更準(zhǔn)確、更易上手的優(yōu)點(diǎn)，可對(duì)未覆蓋的代碼進(jìn)行全面的不可達(dá)性檢查。

芯天成EsseFormal的定制化和集成化特點(diǎn)，使得它能夠精準(zhǔn)匹配不同用戶的特定需求，從而顯著降低驗(yàn)證時(shí)間，提高驗(yàn)證的完整性和準(zhǔn)確性。其簡(jiǎn)潔易用的圖形用戶界面，讓驗(yàn)證過程更加直觀和高效，即使是初次接觸形式驗(yàn)證的用戶也能快速上手。

驗(yàn)證發(fā)展方向：覆蓋率的提升

在當(dāng)前的硬件設(shè)計(jì)領(lǐng)域中，隨著設(shè)計(jì)復(fù)雜度的急劇增加，驗(yàn)證已成為確保芯片功能和性能可靠性的關(guān)鍵環(huán)節(jié)。驗(yàn)證技術(shù)的發(fā)展方向，尤其是覆蓋率的提升，成為了行業(yè)關(guān)注的焦點(diǎn)。思爾芯的軟件仿真芯神馳PegaSim通過其創(chuàng)新性的解決方案，與國(guó)微芯的形式驗(yàn)證工具進(jìn)行無(wú)縫集成，為提升驗(yàn)證的全面性和效率樹立了新的標(biāo)桿。

覆蓋率是衡量驗(yàn)證完整性的重要指標(biāo)，它反映了驗(yàn)證過程中測(cè)試向量對(duì)設(shè)計(jì)代碼覆蓋的廣度和深度。然而，在復(fù)雜的硬件設(shè)計(jì)中，往往存在難以觸及的代碼區(qū)域，即所謂的“不可達(dá)部分”。這些區(qū)域若未經(jīng)充分驗(yàn)證，就可能成為潛在的設(shè)計(jì)漏洞。因此，提升覆蓋率，特別是針對(duì)不可達(dá)部分的驗(yàn)證，對(duì)于確保設(shè)計(jì)質(zhì)量和可靠性至關(guān)重要。

思爾芯的軟件仿真PegaSim通過與國(guó)微芯的形式驗(yàn)證工具相結(jié)合，實(shí)現(xiàn)了對(duì)覆蓋率中不可達(dá)部分進(jìn)行深入驗(yàn)證。這一解決方案不僅增強(qiáng)了軟件仿真過程中的代碼覆蓋率，還通過增加激勵(lì)或優(yōu)化代碼的方式，進(jìn)一步提高了驗(yàn)證的全面性和準(zhǔn)確性。同時(shí)，PegaSim還支持對(duì)指定模塊或特定代碼行進(jìn)行精細(xì)化的覆蓋不可達(dá)性檢查，幫助設(shè)計(jì)團(tuán)隊(duì)精準(zhǔn)定位并消除無(wú)意義或冗余的代碼，從而優(yōu)化內(nèi)在邏輯，提升整體設(shè)計(jì)質(zhì)量。

面對(duì)日益復(fù)雜的硬件設(shè)計(jì)，單一的驗(yàn)證方法已難以滿足全面驗(yàn)證的需求。因此，驗(yàn)證技術(shù)的發(fā)展趨勢(shì)是多種驗(yàn)證方法的融合與互補(bǔ)。軟件仿真、硬件仿真、原型驗(yàn)證、以及形式驗(yàn)證等方法各有千秋，它們?cè)诓煌尿?yàn)證階段和側(cè)重點(diǎn)上發(fā)揮著不可替代的作用。通過綜合運(yùn)用這些驗(yàn)證方法，可以實(shí)現(xiàn)對(duì)硬件設(shè)計(jì)的全方位、多角度檢驗(yàn)，從而確保設(shè)計(jì)的正確性和可靠性。

關(guān)于思爾芯 S2C

思爾芯（S2C）自 2004 年設(shè)立上?？偛恳詠硎冀K專注于集成電路 EDA 領(lǐng)域。作為國(guó)內(nèi)首家數(shù)字 EDA 供應(yīng)商，公司業(yè)務(wù)已覆蓋架構(gòu)設(shè)計(jì)、軟件仿真、硬件仿真、原型驗(yàn)證、數(shù)字調(diào)試、EDA 云等工具及服務(wù)。已與超過 600 家國(guó)內(nèi)外企業(yè)建立了良好的合作關(guān)系，服務(wù)于人工智能、高性能計(jì)算、圖像處理、數(shù)據(jù)存儲(chǔ)、信號(hào)處理等數(shù)字電路設(shè)計(jì)功能的實(shí)現(xiàn)，廣泛應(yīng)用于物聯(lián)網(wǎng)、云計(jì)算、5G 通信、智慧醫(yī)療、汽車電子等終端領(lǐng)域。