近年來，由于集成電路規(guī)模不斷擴(kuò)大、復(fù)雜度日益提高，使得對(duì)確保芯片功能正確性、完整性最重要一環(huán)的驗(yàn)證技術(shù)面臨一系列的巨大挑戰(zhàn)。如何保證快速、高效地實(shí)現(xiàn)對(duì)更大規(guī)模電路，進(jìn)行全面有效的驗(yàn)證是目前芯片設(shè)計(jì)行業(yè)不得不去面對(duì)并解決的痛點(diǎn)。傳統(tǒng)基于電路的仿真技術(shù)，一直存在諸多問題且無法有效解決，比如，對(duì)極端情況無法覆蓋、過長的仿真時(shí)間、測(cè)試環(huán)境搭建等。而業(yè)界也在不斷探索一些更為有效的驗(yàn)證方法學(xué)，比如，形式化驗(yàn)證，便攜式激勵(lì)標(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斷言語言，逐個(gè)描述與定義待檢查的功能場(chǎng)景。另一方面約束非法場(chǎng)景的發(fā)生，并自動(dòng)進(jìn)行數(shù)學(xué)分析和證明，通過對(duì)所有可能的激勵(lì)空間進(jìn)行遍歷，保證邏輯沒有死角。相較于動(dòng)態(tài)驗(yàn)證而言，形式化驗(yàn)證至少有四個(gè)無可替代的重要優(yōu)勢(shì)。

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

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

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

02精準(zhǔn)定位錯(cuò)誤場(chǎng)景

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

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

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

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

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

總體來說，形式化驗(yàn)證技術(shù)效率高，完備性強(qiáng)，是發(fā)現(xiàn)人類正常思維以外的corner bug的利器，有利于盡快、盡早的發(fā)現(xiàn)并協(xié)助改正電路設(shè)計(jì)中的錯(cuò)誤，提高設(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)證平臺(tái)(FusionVerify Platform), 與其他驗(yàn)證工具在編譯、調(diào)試、覆蓋率等方面互融互通，進(jìn)一步加速設(shè)計(jì)驗(yàn)證收斂，幫助芯片設(shè)計(jì)在更早期階段，完成簡(jiǎn)單高效的完備驗(yàn)證，從而極大地提升驗(yàn)證效率。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

建模顆粒度大

性能表現(xiàn)好

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

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

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

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

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

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

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

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

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

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

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

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

審核編輯：湯梓紅