近年來，由于集成電路規模不斷擴大、復雜度日益提高，使得對確保芯片功能正確性、完整性最重要一環的驗證技術面臨一系列的巨大挑戰。如何保證快速、高效地實現對更大規模電路，進行全面有效的驗證是目前芯片設計行業不得不去面對并解決的痛點。傳統基于電路的仿真技術，一直存在諸多問題且無法有效解決，比如，對極端情況無法覆蓋、過長的仿真時間、測試環境搭建等。而業界也在不斷探索一些更為有效的驗證方法學，比如，形式化驗證，便攜式激勵標準(PSS)等。

形式化方法是一種基于嚴格的數學與算法的驗證方法學。在芯片驗證上，用戶利用SVA斷言描述清楚需要證明的設計規格，通過編譯RTL和基于SVA的斷言語言，建立Formal模型。一方面根據設計spec的要求，提取需要驗證的功能點，進而通過SVA斷言語言，逐個描述與定義待檢查的功能場景。另一方面約束非法場景的發生，并自動進行數學分析和證明，通過對所有可能的激勵空間進行遍歷，保證邏輯沒有死角。相較于動態驗證而言，形式化驗證至少有四個無可替代的重要優勢。

形式化驗證四大優勢

01驗證空間完備性

當所有輸入端的每個信號，每一時鐘周期都只有0或1兩種取值，那么任何一種測試場景都是完備測試空間的一個時空二維的子集。通過對RTL轉化成形式化驗證模型，將功能驗證問題轉化成了給定行為的數學推導，進而對完備驗證空間進行遍歷。

02精準定位錯誤場景

一旦有一個設計場景導致斷言不成功，會精準給出特定時鐘下的特定波形。而傳統的動態驗證是基于Log進行debug，需要從事務級進行推導，逐級定位可能的設計問題。

03驗證環境簡單高效

不需要搭建復雜、層次繁多的驗證環境，針對待測試場景精準描述Property，進而進行輸入場景遍歷和推導證明。

04覆蓋率收集脫離工程師人為風險

形式化驗證覆蓋率收集方案是基于算法和模型由工具自發完成，整個過程不依賴于人工定義function coverage，這極大程度地避免了因人為失誤導致的覆蓋率準確度不高的風險。

總體來說，形式化驗證技術效率高，完備性強，是發現人類正常思維以外的corner bug的利器，有利于盡快、盡早的發現并協助改正電路設計中的錯誤，提高設計質量，縮短芯片設計周期。

芯華章穹瀚GalaxFV就是這樣一種面向HDL電路設計的形式化驗證工具，能夠從數學上完備地證明“電路的實現方案是否滿足了設計規范所描述的功能”。GalaxFV在保留形式化驗證完備性的基礎上，依托于芯華章智V驗證平臺(FusionVerify Platform), 與其他驗證工具在編譯、調試、覆蓋率等方面互融互通，進一步加速設計驗證收斂，幫助芯片設計在更早期階段，完成簡單高效的完備驗證，從而極大地提升驗證效率。

使用GalaxFV的驗證實例

以下實例是中國研究生創“芯”大賽中，深圳大學參與芯華章企業命題“糾錯編解碼算法實現和驗證”的優秀作品。

基于Verilog語言設計的信道糾錯編解碼算法實現模塊

下面我們對一個基于Verilog語言設計的信道糾錯編解碼算法實現模塊，使用GalaxFV來構建形式化驗證流程。

該模塊是通信領域芯片中，為了保障信息傳輸連續不失真，而進行的信道糾錯的設計。它通過對原始五個信道編碼擴容成七個通道，并且在這七個通道中至多任意兩個通道損壞的情況下，能夠通過解碼來恢復原始輸入端五個信道的數據。

該設計具有各種設計規格，每一個設計規格可以用一條SVA屬性(property)來描述，最終對應一個個驗證目標(Goals)。

在形式化驗證中，我們用約束(assume)Property來構造驗證激勵，其中‘asm_ch’對應第一個設計規格，這條屬性可描述為：信道注錯使能(低有效)信號‘channel’至少需要有5個比特位的數值為1，即發生損毀的通道數最多為2個。

形式化驗證通過斷言(assert)屬性來實現功能檢查。而‘ast_sym_data_0’則對應第二個設計規格，這條屬性可描述為：在復位結束之后的每一個時鐘周期，如果信道0的輸入數據為標記數據，那么從當前周期開始的四個周期后，信道0的輸出數據都會等于標記數據。其中標記數據為常量，下方的波形圖展示了該屬性的預期行為。

實例中的形式化驗證環境展示

首先，我們需要通過約束屬性來規避不符合設計需求的激勵。其次，我們需要對特殊的信號(比如時鐘與復位信號)進行定義，以保證工具能夠對這些信號做合適的處理。除此之外，我們通過自研的scoreboard進行數據一致性的檢查。

GalaxFV依靠自主研發的字級建模方法，可將百萬行級別的設計代碼轉化為數學模型，把驗證問題轉化成數學求解問題，然后依靠求解器進行求解。而求解器就像“操作系統”，對數學上高度復雜的系統進行分解并給出最終的證明結果。

同時GalaxFV具備動態智能調度，就好比有一個“控制中心”，可根據驗證目標的特征匹配出最佳方案，因地制宜地選用不同的“操作系統”進行求解。最后通過分布式計算將設計 “分而治之”。對于一個大規模的計算問題，GalaxFV可將它分成一些可以同時進行的小任務，讓多個計算機對它們分別進行處理，最終得到驗證結果。

產品亮點

采用高性能字級建模(Word-Level Modeling)方法構建

相比于比特級建模(Bit-Level Modeling)方法, 字級建模方法具備以下優勢：

建模顆粒度大

性能表現好

可同時調用字級求解器和比特級求解器

可擴展性能力強

自主研發的專用、高效的應用級斷言庫

GalaxFV對于設計中常用到的標準組件構建了專用、高效的應用級斷言庫，對其參數化，提高可配置性，降低了用戶構建斷言與約束的難度。可充分利用算力，提高并行效率的同時，提高易用性和使用效率，為形式化驗證應用于產業降低了門檻。

搭載自研的高并發、高性能求解器

GalaxFV在服務器集群或云平臺上發揮分布式計算的強大性能，為快速證明求解賦能。并且，GalaxFV研發了針對求解器的智能分組和調度預測算法，結合每種引擎的算法和特性，在面對不同的設計和斷言類型時，組合調度各個求解器單元進行求解，進一步提高求解效率。結合了這些技術特點，GalaxFV在一些客戶設計上給出了亮眼的性能表現，相比于現有的業界知名形式化驗證工具，實測性能超越其約20%。( 僅針對某AsyncFIFO設計實測得出Measured only for a certain AsyncFIFO design)

芯華章穹瀚GalaxFV采用數學方法來求解驗證難題，是對仿真技術的有力補充，先進的建模方法與調度算法，在我們的rtllib模塊性能實測中，性能表現優秀，對工程應用有很高的價值。

—— 周孝斌，天數智芯形式驗證專家

形式化驗證基于數學思維進行驗證求解，具備極高的可靠性，可以大大縮短開發周期。面對形式化驗證工具使用門檻較高的難點，芯華章研發團隊采用了字級建模方法構建，并搭載自主研發的專用斷言庫與求解器，讓具有高完備性優勢的形式化驗證工具，能夠幫助更多的芯片研發工程師在項目開發初期，盡早地發現問題、快速修復。

—— 齊正華，芯華章科技研發副總裁

原文標題：基于字級建模的可擴展形式化驗證工具——穹瀚GalaxFV

文章出處：【微信公眾號：芯華章科技】歡迎添加關注!文章轉載請注明出處。

審核編輯：湯梓紅