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