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

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

形式化驗(yàn)證四大優(yōu)勢

01驗(yàn)證空間完備性

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

02精準(zhǔn)定位錯誤場景

一旦有一個設(shè)計(jì)場景導(dǎo)致斷言不成功，會精準(zhǔn)給出特定時鐘下的特定波形。而傳統(tǒng)的動態(tài)驗(yàn)證是基于Log進(jìn)行debug，需要從事務(wù)級進(jìn)行推導(dǎo)，逐級定位可能的設(shè)計(jì)問題。

03驗(yàn)證環(huán)境簡單高效

不需要搭建復(fù)雜、層次繁多的驗(yàn)證環(huán)境，針對待測試場景精準(zhǔn)描述Property，進(jìn)而進(jìn)行輸入場景遍歷和推導(dǎo)證明。

04覆蓋率收集脫離工程師人為風(fēng)險

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

總體來說，形式化驗(yàn)證技術(shù)效率高，完備性強(qiáng)，是發(fā)現(xiàn)人類正常思維以外的corner bug的利器，有利于盡快、盡早的發(fā)現(xiàn)并協(xié)助改正電路設(shè)計(jì)中的錯誤，提高設(shè)計(jì)質(zhì)量，縮短芯片設(shè)計(jì)周期。

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

使用GalaxFV的驗(yàn)證實(shí)例

以下實(shí)例是中國研究生創(chuàng)“芯”大賽中，深圳大學(xué)參與芯華章企業(yè)命題“糾錯編解碼算法實(shí)現(xiàn)和驗(yàn)證”的優(yōu)秀作品。

基于Verilog語言設(shè)計(jì)的信道糾錯編解碼算法實(shí)現(xiàn)模塊

下面我們對一個基于Verilog語言設(shè)計(jì)的信道糾錯編解碼算法實(shí)現(xiàn)模塊，使用GalaxFV來構(gòu)建形式化驗(yàn)證流程。

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

該設(shè)計(jì)具有各種設(shè)計(jì)規(guī)格，每一個設(shè)計(jì)規(guī)格可以用一條SVA屬性(property)來描述，最終對應(yīng)一個個驗(yàn)證目標(biāo)(Goals)。

在形式化驗(yàn)證中，我們用約束(assume)Property來構(gòu)造驗(yàn)證激勵，其中‘a(chǎn)sm_ch’對應(yīng)第一個設(shè)計(jì)規(guī)格，這條屬性可描述為：信道注錯使能(低有效)信號‘channel’至少需要有5個比特位的數(shù)值為1，即發(fā)生損毀的通道數(shù)最多為2個。

形式化驗(yàn)證通過斷言(assert)屬性來實(shí)現(xiàn)功能檢查。而‘a(chǎn)st_sym_data_0’則對應(yīng)第二個設(shè)計(jì)規(guī)格，這條屬性可描述為：在復(fù)位結(jié)束之后的每一個時鐘周期，如果信道0的輸入數(shù)據(jù)為標(biāo)記數(shù)據(jù)，那么從當(dāng)前周期開始的四個周期后，信道0的輸出數(shù)據(jù)都會等于標(biāo)記數(shù)據(jù)。其中標(biāo)記數(shù)據(jù)為常量，下方的波形圖展示了該屬性的預(yù)期行為。

實(shí)例中的形式化驗(yàn)證環(huán)境展示

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

GalaxFV依靠自主研發(fā)的字級建模方法，可將百萬行級別的設(shè)計(jì)代碼轉(zhuǎn)化為數(shù)學(xué)模型，把驗(yàn)證問題轉(zhuǎn)化成數(shù)學(xué)求解問題，然后依靠求解器進(jìn)行求解。而求解器就像“操作系統(tǒng)”，對數(shù)學(xué)上高度復(fù)雜的系統(tǒng)進(jìn)行分解并給出最終的證明結(jié)果。

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

產(chǎn)品亮點(diǎn)

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

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

建模顆粒度大

性能表現(xiàn)好

可同時調(diào)用字級求解器和比特級求解器

可擴(kuò)展性能力強(qiáng)

自主研發(fā)的專用、高效的應(yīng)用級斷言庫

GalaxFV對于設(shè)計(jì)中常用到的標(biāo)準(zhǔn)組件構(gòu)建了專用、高效的應(yīng)用級斷言庫，對其參數(shù)化，提高可配置性，降低了用戶構(gòu)建斷言與約束的難度。可充分利用算力，提高并行效率的同時，提高易用性和使用效率，為形式化驗(yàn)證應(yīng)用于產(chǎn)業(yè)降低了門檻。

搭載自研的高并發(fā)、高性能求解器

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

芯華章穹瀚GalaxFV采用數(shù)學(xué)方法來求解驗(yàn)證難題，是對仿真技術(shù)的有力補(bǔ)充，先進(jìn)的建模方法與調(diào)度算法，在我們的rtllib模塊性能實(shí)測中，性能表現(xiàn)優(yōu)秀，對工程應(yīng)用有很高的價值。

—— 周孝斌，天數(shù)智芯形式驗(yàn)證專家

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

—— 齊正華，芯華章科技研發(fā)副總裁

原文標(biāo)題：基于字級建模的可擴(kuò)展形式化驗(yàn)證工具——穹瀚GalaxFV

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

審核編輯：湯梓紅