【導(dǎo)讀】隨著集成電路規(guī)模的不斷擴大,從設(shè)計到流片(Tape-out)的全流程中,驗證環(huán)節(jié)的核心地位日益凸顯。有效的驗證不僅是設(shè)計完美的基石,更是確保電路在實際應(yīng)用中穩(wěn)定運行的保障。尤為關(guān)鍵的是,邏輯或功能錯誤是導(dǎo)致流片失敗的首要原因,占比高達50%。功能驗證正是解決這一難題的利器,它助力工程師精準識別邏輯設(shè)計漏洞、性能不達標問題以及設(shè)計代碼中的功能缺陷,從而最大限度地規(guī)避流片風險。
引言
隨著集成電路規(guī)模的不斷擴大,從設(shè)計到流片(Tape-out)的全流程中,驗證環(huán)節(jié)的核心地位日益凸顯。有效的驗證不僅是設(shè)計完美的基石,更是確保電路在實際應(yīng)用中穩(wěn)定運行的保障。尤為關(guān)鍵的是,邏輯或功能錯誤是導(dǎo)致流片失敗的首要原因,占比高達50%。功能驗證正是解決這一難題的利器,它助力工程師精準識別邏輯設(shè)計漏洞、性能不達標問題以及設(shè)計代碼中的功能缺陷,從而最大限度地規(guī)避流片風險。
針對超大規(guī)模集成電路(VLSI)設(shè)計,目前功能驗證有兩種方法:動態(tài)仿真驗證和形式驗證(Formal Verification)。形式驗證采用數(shù)學(xué)方法來比較原設(shè)計和修改設(shè)計之間的邏輯功能的異同,而動態(tài)仿真驗證是對兩設(shè)計施加相同的激勵后,觀測電路對激勵的反應(yīng)異同。
面對大型設(shè)計,傳統(tǒng)的動態(tài)仿真驗證方法在覆蓋率和效率上面臨挑戰(zhàn)。為了達到100%的覆蓋率,動態(tài)仿真驗證所需要的矢量就會越多,這時形式驗證在這方面就有優(yōu)勢了,成為現(xiàn)代IC設(shè)計驗證流程中的關(guān)鍵一環(huán)。本文就以 “芯天成EsseFCEC”工具為例,來介紹形式驗證的流程和基本概念。
什么是形式驗證
形式驗證是一種基于嚴格數(shù)學(xué)推理的設(shè)計驗證技術(shù),它摒棄了物理測試與模擬的依賴,專注于通過靜態(tài)、全面的邏輯分析來確保設(shè)計的正確性。此方法顯著降低了對龐大測試集的需求,并力求實現(xiàn)接近完美的驗證覆蓋率。
形式驗證作為EDA、數(shù)學(xué)及編程語言等多學(xué)科交叉的產(chǎn)物,自上世紀90年代起便嶄露頭角,最初應(yīng)用于RTL代碼與門級網(wǎng)表的LEC(邏輯等價性檢查),隨后逐步擴展到各類EDA工具,以應(yīng)對不同驗證場景的需求。
目前,形式驗證主要分為兩個技術(shù)方向:等價性檢查和屬性檢查。其中。等價性檢查,作為核心驗證手段,通過對比功能驗證后的HDL設(shè)計與綜合后的網(wǎng)表功能,確保兩者在功能層面上的完全一致,從而保證門級電路與寄存器傳輸級(Register Transfer Level, RTL)模型之間的一致性。這一方法有效防范了綜合工具潛在的缺陷及人為誤操作,對于提升設(shè)計質(zhì)量至關(guān)重要。
形式驗證的實施涉及多個關(guān)鍵環(huán)節(jié):
屬性定義(Properties):精確闡述設(shè)計需遵循的特性與規(guī)范,涵蓋時序邏輯、狀態(tài)轉(zhuǎn)換規(guī)則及各項約束條件。
規(guī)約語言:采用如SystemVerilog Assertions(SVA)、Property Specification Language(PSL)等形式化規(guī)約語言,將屬性與約束轉(zhuǎn)化為可驗證的表達式。
定理證明器(Theorem Provers):依托形式化邏輯與推理機制,自動驗證屬性是否成立,為設(shè)計邏輯的正確性提供堅實保障。
模型檢查器(Model Checkers):全面探索系統(tǒng)狀態(tài)空間,尋找可能違反預(yù)定性質(zhì)的執(zhí)行路徑,確保設(shè)計在所有可能情況下均能滿足既定要求。
形式驗證的基本流程是一個連貫且系統(tǒng)化的過程。這一過程從明確驗證目標開始,設(shè)計團隊首先需要界定哪些部分或功能需要接受形式驗證的嚴格審查。接著,采用形式規(guī)約語言(如SystemVerilog Assertions、PSL)定義屬性和規(guī)約,作為驗證基礎(chǔ)。進入驗證環(huán)境配置階段,團隊選擇適合的驗證工具(定理證明器、模型檢查器),并依據(jù)設(shè)計特性和需求進行優(yōu)化配置,以確保驗證效率與準確性。
驗證執(zhí)行為核心,定理證明器通過數(shù)學(xué)推理驗證屬性與規(guī)約的正確性,模型檢查器則全面探索系統(tǒng)狀態(tài)空間,檢查違規(guī)執(zhí)行序列。驗證結(jié)束后,團隊分析驗證結(jié)果,識別并修正設(shè)計中的錯誤或不一致。此過程可能多次迭代,直至設(shè)計完全符合驗證要求。
形式驗證工具的挑戰(zhàn)
形式驗證的流程雖然復(fù)雜且嚴謹,但它為設(shè)計團隊提供了一種高效且可靠的驗證方法。通過遵循這一流程,設(shè)計團隊可以顯著降低設(shè)計錯誤的風險,提高產(chǎn)品的質(zhì)量和可靠性。然而,隨著現(xiàn)代芯片設(shè)計的復(fù)雜性和規(guī)模不斷增長,形式驗證在實際應(yīng)用中面臨多重挑戰(zhàn):
復(fù)雜性增加,性能不足:現(xiàn)代芯片設(shè)計的復(fù)雜性和規(guī)模不斷增長,對驗證工具的性能提出了更高要求?,F(xiàn)有工具在處理大規(guī)模設(shè)計時可能面臨性能瓶頸,導(dǎo)致驗證過程耗時過長。
多樣化的設(shè)計環(huán)境:不同的設(shè)計團隊可能使用不同的設(shè)計語言和平臺,這要求驗證工具具備廣泛的兼容性和集成能力。然而,多樣化的設(shè)計環(huán)境可能導(dǎo)致兼容性和集成性方面的挑戰(zhàn)。
可擴展性需求增加:隨著技術(shù)的不斷進步和新的設(shè)計需求的出現(xiàn),驗證工具需要具備良好的可擴展性,以快速適應(yīng)新的設(shè)計規(guī)范和標準。這對工具的開發(fā)和維護提出了更高要求。
復(fù)雜的設(shè)計錯誤檢測:在復(fù)雜的設(shè)計中,子系統(tǒng)之間的交互和邏輯路徑可能非常復(fù)雜,驗證工具需要能夠準確地檢測這些復(fù)雜場景中的錯誤和不一致之處。這要求工具具備強大的錯誤檢測能力和智能化的分析手段。
芯天成EsseFormal形式驗證軟件
芯天成EsseFormal形式驗證軟件是一款功能全面的驗證解決方案,專為數(shù)字芯片設(shè)計領(lǐng)域的復(fù)雜驗證挑戰(zhàn)而設(shè)計。其核心包含五種工具套件,每一種都針對特定的驗證需求提供高效、精準的支持。
EsseFECT(形式化等價性驗證):該工具專注于驗證C-to-RTL的轉(zhuǎn)換過程中,設(shè)計的等價性是否得以保持。這確保了設(shè)計在不同抽象層次間的轉(zhuǎn)換無誤,是確保設(shè)計一致性的重要環(huán)節(jié)。
EsseFCEC(組合邏輯等價性驗證):作為EsseFormal的明星產(chǎn)品,EsseFCEC專門用于驗證芯片設(shè)計中各電路模塊之間的組合邏輯等價性。它不僅支持RTL到Netlist的轉(zhuǎn)換驗證,還涵蓋版本間差異的比較,確保設(shè)計更改不會引入錯誤。其強大的綜合優(yōu)化技術(shù)支持(如Clock-gating、multibit register banking和FSM recoding)顯著提升了驗證效率和性能。此外,對DesignWare元件庫的支持以及大位寬datapath驗證的能力,進一步拓寬了EsseFCEC的應(yīng)用范圍。
EsseFPV(模型檢查):通過遍歷設(shè)計的狀態(tài)空間,EsseFPV能夠發(fā)現(xiàn)設(shè)計中可能存在的違反預(yù)定義屬性的行為,是確保設(shè)計行為符合預(yù)期的關(guān)鍵工具。
EsseCC與EsseUNR(實用驗證Apps):這兩個工具提供了額外的實用功能。EsseCC是一個高效的連接性檢查驗證工具,為用戶提供快速的錯誤檢測以及信號到信號的預(yù)期設(shè)計行為驗證。EsseCC以RTL電路和連接規(guī)范作為輸入,快速檢查設(shè)計是否符合連接規(guī)范。而EsseUNR是一款高效的覆蓋不可達性檢查工具。使用傳統(tǒng)的驗證方式,在驗證后期,通過編寫測試用例提升驗證覆蓋率的難度陡然上升。該工具具有更高效、更準確、更易上手的優(yōu)點,可對未覆蓋的代碼進行全面的不可達性檢查。
芯天成EsseFormal的定制化和集成化特點,使得它能夠精準匹配不同用戶的特定需求,從而顯著降低驗證時間,提高驗證的完整性和準確性。其簡潔易用的圖形用戶界面,讓驗證過程更加直觀和高效,即使是初次接觸形式驗證的用戶也能快速上手。
驗證發(fā)展方向:覆蓋率的提升
在當前的硬件設(shè)計領(lǐng)域中,隨著設(shè)計復(fù)雜度的急劇增加,驗證已成為確保芯片功能和性能可靠性的關(guān)鍵環(huán)節(jié)。驗證技術(shù)的發(fā)展方向,尤其是覆蓋率的提升,成為了行業(yè)關(guān)注的焦點。思爾芯的軟件仿真芯神馳PegaSim通過其創(chuàng)新性的解決方案,與國微芯的形式驗證工具進行無縫集成,為提升驗證的全面性和效率樹立了新的標桿。
覆蓋率是衡量驗證完整性的重要指標,它反映了驗證過程中測試向量對設(shè)計代碼覆蓋的廣度和深度。然而,在復(fù)雜的硬件設(shè)計中,往往存在難以觸及的代碼區(qū)域,即所謂的“不可達部分”。這些區(qū)域若未經(jīng)充分驗證,就可能成為潛在的設(shè)計漏洞。因此,提升覆蓋率,特別是針對不可達部分的驗證,對于確保設(shè)計質(zhì)量和可靠性至關(guān)重要。
思爾芯的軟件仿真PegaSim通過與國微芯的形式驗證工具相結(jié)合,實現(xiàn)了對覆蓋率中不可達部分進行深入驗證。這一解決方案不僅增強了軟件仿真過程中的代碼覆蓋率,還通過增加激勵或優(yōu)化代碼的方式,進一步提高了驗證的全面性和準確性。同時,PegaSim還支持對指定模塊或特定代碼行進行精細化的覆蓋不可達性檢查,幫助設(shè)計團隊精準定位并消除無意義或冗余的代碼,從而優(yōu)化內(nèi)在邏輯,提升整體設(shè)計質(zhì)量。
面對日益復(fù)雜的硬件設(shè)計,單一的驗證方法已難以滿足全面驗證的需求。因此,驗證技術(shù)的發(fā)展趨勢是多種驗證方法的融合與互補。軟件仿真、硬件仿真、原型驗證、以及形式驗證等方法各有千秋,它們在不同的驗證階段和側(cè)重點上發(fā)揮著不可替代的作用。通過綜合運用這些驗證方法,可以實現(xiàn)對硬件設(shè)計的全方位、多角度檢驗,從而確保設(shè)計的正確性和可靠性。
關(guān)于思爾芯 S2C
思爾芯(S2C)自 2004 年設(shè)立上??偛恳詠硎冀K專注于集成電路 EDA 領(lǐng)域。作為國內(nèi)首家數(shù)字 EDA 供應(yīng)商,公司業(yè)務(wù)已覆蓋架構(gòu)設(shè)計、軟件仿真、硬件仿真、原型驗證、數(shù)字調(diào)試、EDA 云等工具及服務(wù)。已與超過 600 家國內(nèi)外企業(yè)建立了良好的合作關(guān)系,服務(wù)于人工智能、高性能計算、圖像處理、數(shù)據(jù)存儲、信號處理等數(shù)字電路設(shè)計功能的實現(xiàn),廣泛應(yīng)用于物聯(lián)網(wǎng)、云計算、5G 通信、智慧醫(yī)療、汽車電子等終端領(lǐng)域。
公司總部位于上海,并建立了全球化的技術(shù)研發(fā)與市場服務(wù)網(wǎng)絡(luò),在北京、深圳、西安、香港、東京、首爾及圣何塞等地均設(shè)有分支機構(gòu)或辦事處。 思爾芯在 EDA 領(lǐng)域的技術(shù)實力受到了業(yè)界的廣泛認可,通過多年耕耘,已在數(shù)字前端 EDA 領(lǐng)域構(gòu)筑了技術(shù)與市場的雙優(yōu)勢地位。并參與了我國 EDA 團體標準的制定,承擔了多項國家及地方重大科研項目,獲國家級專精特新“小巨人”企業(yè)、國家工業(yè)軟件優(yōu)秀產(chǎn)品、上海市級企業(yè)技術(shù)中心等多項榮譽資質(zhì)。
(來源:思爾芯S2C)
免責聲明:本文為轉(zhuǎn)載文章,轉(zhuǎn)載此文目的在于傳遞更多信息,版權(quán)歸原作者所有。本文所用視頻、圖片、文字如涉及作品版權(quán)問題,請聯(lián)系小編進行處理。
推薦閱讀:
可識別時間序列數(shù)據(jù)趨勢的嵌入式人工智能系統(tǒng)