陳軍花 石顥 柴金寶

摘? 要：驗(yàn)證是FPGA開發(fā)流程和IC芯片設(shè)計(jì)流程中不可或缺的環(huán)節(jié)，文章首先分析了當(dāng)前數(shù)字仿真驗(yàn)證用例設(shè)計(jì)無法跨越的不完備性和不充分性，并詳細(xì)探討了為什么功能仿真會(huì)錯(cuò)過一些角落案例場景。在此基礎(chǔ)上，介紹了形式化驗(yàn)證中FPGA的主要應(yīng)用場景以及硬件邏輯功能驗(yàn)證語言SVA，并以實(shí)際工程案例闡述了基于SVA的形式化驗(yàn)證方法如何更好地在驗(yàn)證關(guān)鍵設(shè)計(jì)中發(fā)揮作用。

關(guān)鍵詞：FPGA;形式化驗(yàn)證;SVA

中圖分類號(hào)：TN79+1? ? ? ? ? ? ? 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：2096-4706（2021）19-0030-04

Research on Formal Verification Technology of FPGA Software

CHEN Junhua， SHI Hao， CHAI Jinbao

（Software Test and Evaluation Center of CASIC Fourth Academy （Wuhan）， Wuhan? 430000， China）

Abstract： Verification is an indispensable link in the FPGA development process and IC chip design process. Firstly， this paper analyzes the incompleteness and inadequacy that the current digital simulation verification use case design cannot leap over， and discusses in detail why functional simulation misses some corner case scenarios. On this basis， this paper introduces the main application scenarios of FPGA in formal verification and the hardware logic function verification language SVA， and expounds how the formal verification method based on SVA better play a role in verifying the key design with a practical engineering case.

Keywords： FPGA; formal verification; SVA

0? 引? 言

在芯片設(shè)計(jì)流程中，驗(yàn)證占整個(gè)芯片設(shè)計(jì)流70%的人力物資源，流片失敗的原因70%是由驗(yàn)證不充分導(dǎo)致的功能錯(cuò)誤。

由于FPGA設(shè)計(jì)復(fù)雜度的不斷提升，為功能驗(yàn)證帶來了前所未有的挑戰(zhàn)。因?yàn)樵O(shè)計(jì)擁有越多的信號(hào)個(gè)數(shù)，可能出現(xiàn)的信號(hào)組合將會(huì)呈現(xiàn)爆炸式的增長，所以通過仿真器達(dá)到各種情景組合的100%覆蓋幾乎是不可能的。

1? FPGA功能驗(yàn)證現(xiàn)狀

1.1? 功能仿真的局限性

功能仿真是一種非常流行和有用的FPGA驗(yàn)證技術(shù)。從操作性角度考慮，它便于設(shè)置，并且為內(nèi)部設(shè)計(jì)和測試平臺(tái)操作提供了極佳的可見性，使調(diào)試相對(duì)容易。此外，從成本角度考慮，仿真工具相對(duì)便宜，常用仿真器實(shí)際上是由FPGA供應(yīng)商免費(fèi)提供的，滿足絕大多數(shù)仿真需求。

雖然目前有諸如人工設(shè)計(jì)測試用例序列、隨機(jī)測試激勵(lì)生成等基于仿真的傳統(tǒng)驗(yàn)證技術(shù)[1]，可以從一定程度上提高FPGA單元/配置項(xiàng)級(jí)設(shè)計(jì)的驗(yàn)證質(zhì)量，但定向測試的仿真驗(yàn)證技術(shù)中依然存在明顯的關(guān)鍵難題。

以兩個(gè)小型設(shè)計(jì)為例，以便更好地理解功能驗(yàn)證的瓶頸所在。

1.2? 功能仿真的不完備性

圖1顯示了一個(gè)4輸入組合邏輯單元和后序的一個(gè)寄存器單元構(gòu)成的一個(gè)FPGA基本構(gòu)建塊。一般的FPGA可能包含數(shù)百或數(shù)千個(gè)這樣的構(gòu)建塊。每個(gè)構(gòu)造塊都可以通過編程來執(zhí)行幾乎任何包含4個(gè)二進(jìn)制輸入的布爾函數(shù)，并帶有一個(gè)可選的輸出寄存器。

為了實(shí)現(xiàn)單個(gè)構(gòu)建塊的完全驗(yàn)證，驗(yàn)證環(huán)境需要探索其所有可能的狀態(tài)，以確保設(shè)計(jì)在所有狀態(tài)中按照預(yù)期運(yùn)行。將一個(gè)特定的寄存器值（或寄存器組合值），與一個(gè)特定的輸入信號(hào)值組合在一起，構(gòu)成一個(gè)驗(yàn)證場景，定義為1個(gè)“狀態(tài)”。下圖顯示了這個(gè)基本構(gòu)建塊的所有可能的“狀態(tài)”，總共有32種狀態(tài)。所有32個(gè)狀態(tài)的集合就是構(gòu)建塊的完整“狀態(tài)空間”。

我們由此可以抽象出任何給定設(shè)計(jì)的狀態(tài)空間，如下圖所示，以一個(gè)只有1 000門的示例FPGA為目標(biāo)，假設(shè)該設(shè)計(jì)占用了可用邏輯的三分之一，使用資源如表1所示。

保守估計(jì)，狀態(tài)空間為2（49個(gè)寄存器+10輸入）=259，即5.76×1017，假設(shè)一個(gè)非?？斓倪壿嫹抡嫫?，以每秒100萬個(gè)時(shí)鐘周期運(yùn)行。如果我們運(yùn)行所有這些狀態(tài)，需要的時(shí)間5.76×1017秒，約為18 279年。

如上分析，一旦意識(shí)到完備驗(yàn)證場景（狀態(tài)空間）的驚人規(guī)模，一組人工創(chuàng)建的定向測試無法執(zhí)行所有狀態(tài)就不足為奇了。在許多情況下，考慮到設(shè)計(jì)和驗(yàn)證團(tuán)隊(duì)技術(shù)能力、經(jīng)驗(yàn)的差別，驗(yàn)證不完備性的缺點(diǎn)將會(huì)再次放大。

1.3? 功能仿真的不充分性

以一個(gè)簡單的數(shù)學(xué)題為例：

3B3=65 865

對(duì)于仿真，需要闡明并嘗試的可能解決方案，換句話說，就是通過猜測答案，然后仿真，以確定猜測是否正確，仿真驗(yàn)證激勵(lì)如表2所示。

由于仿真引擎本身只不過是一個(gè)計(jì)算工具，它可執(zhí)行你提供的任何激勵(lì)，并輸出結(jié)果，如果設(shè)計(jì)的測試用例沒有猜出答案，通過仿真將永遠(yuǎn)不會(huì)知道正確的答案。

通過以上分析，功能仿真驗(yàn)證用例集由人工設(shè)計(jì)，難以確保和評(píng)估用例集的充分性;此外，仿真驗(yàn)證還需要消耗相當(dāng)?shù)娜肆Y源和時(shí)間成本，進(jìn)行測試用例開發(fā)、測試環(huán)境搭建和具體調(diào)試。

仿真測試的先天局限性導(dǎo)致FPGA軟件測試的完備性與充分性難以得到滿足，而形式化驗(yàn)證引擎與基于ABV的功能驗(yàn)證方法學(xué)的結(jié)合方式可以很好地解決上述問題。

2? 形式化驗(yàn)證

FPGA設(shè)計(jì)的形式化驗(yàn)證，是指工具通過自動(dòng)分析電路中的邏輯結(jié)構(gòu)來推導(dǎo)出是否有極端的情況，使預(yù)先設(shè)定的設(shè)計(jì)規(guī)則有可能無法滿足。由于這種驗(yàn)證不需要用戶的測試向量，并且可以對(duì)電路做窮舉法驗(yàn)證，因此，對(duì)于某些傳統(tǒng)驗(yàn)證手段無法做到但是又至關(guān)重要的電路，就必須采用形式化驗(yàn)證這種手段來保證設(shè)計(jì)的可靠性。

2.1? FPGA形式化驗(yàn)證應(yīng)用場景

形式化方法目前主要的應(yīng)用場景為定理證明、模型檢驗(yàn)、等價(jià)性檢驗(yàn)，針對(duì)FPGA軟件，主要使用模型檢驗(yàn)和等價(jià)性檢驗(yàn)[1]。

模型檢查是一種基于有限模型并檢驗(yàn)該模型的期望行為特性的一種技術(shù)。粗略地講，就是對(duì)狀態(tài)空間的蠻力或智能搜索，模型的有限性確保了搜索可以終止。模型檢查是完全自動(dòng)且高效的，它可用于FPGA配置項(xiàng)級(jí)別，也可用于項(xiàng)目中的子系統(tǒng)或模塊，其主要局限性在于狀態(tài)組合爆炸問題。

等價(jià)性檢驗(yàn)主要目的是用來對(duì)兩個(gè)電路的設(shè)計(jì)、設(shè)計(jì)規(guī)范及實(shí)現(xiàn)之間進(jìn)行邏輯功能的等價(jià)性檢驗(yàn)?；蛘咴谠O(shè)計(jì)經(jīng)過變換之后，窮盡地檢查變換前后的功能一致性，表明設(shè)計(jì)的變換沒有產(chǎn)生功能的變化。

因此，形式化驗(yàn)證在FPGA驗(yàn)證中有兩種，一種是基于模型檢查的FPV（formal property verifacation），另一種是基于等價(jià)性檢查的FEV（formal equivalence verification）。本文中，我們將引用FPV中的SVA斷言驗(yàn)證來演示FPGA形式化驗(yàn)證的優(yōu)勢。

2.2? SVA斷言

SVA（SystemVerilog Assertions）是目前最常用的硬件邏輯功能驗(yàn)證語言之一[2]，可被FPGA仿真軟件和形式化驗(yàn)證工具自動(dòng)識(shí)別。

SVA分為立即斷言和并發(fā)斷言[3]。立即斷言基于事件的變化[4]，采用立即求值的方式，與時(shí)序無關(guān)。在仿真和形式化驗(yàn)證中通常采用并發(fā)斷言。并發(fā)斷言的計(jì)算基于時(shí)鐘周期，在時(shí)鐘邊沿根據(jù)變量的采樣值進(jìn)行表達(dá)式計(jì)算，可通過簡練的語法描述復(fù)雜的時(shí)序行為[5]。

一條SVA并發(fā)斷言由四種不同層次的結(jié)構(gòu)組成。布爾表達(dá)式（booleans）是最基礎(chǔ)的單元，有信號(hào)及其邏輯關(guān)系運(yùn)算符構(gòu)成，用以表示某個(gè)邏輯事件的發(fā)生。布爾表達(dá)式在時(shí)間上的組合構(gòu)成了序列（sequence）。屬性（property）是在仿真或形式化驗(yàn)證中被驗(yàn)證的單元。屬性將序列通過邏輯或者有序地組合起來生成更復(fù)雜的序列。屬性在斷言聲明中被調(diào)用。斷言采用assert、assume、cover中的任一一種關(guān)鍵字進(jìn)行聲明。

3? 項(xiàng)目應(yīng)用

以某型號(hào)軟件中AXI4Lite到APB4橋接設(shè)計(jì)邏輯功能驗(yàn)證為例，如圖2所示，設(shè)計(jì)實(shí)現(xiàn)為采用仲裁器（Pin MUX模塊）來確定APB4總線主控制端的讀寫事務(wù)。

其中需檢驗(yàn)的功能之一就是確定仲裁器中的信號(hào)是否存在同時(shí)有效的情況出現(xiàn)，即返回表達(dá)式中只有一個(gè)1或全為0，則表示仲裁功能實(shí)現(xiàn)正確，否則功能實(shí)現(xiàn)錯(cuò)誤。根據(jù)該需求對(duì)上述的APB4總線主控端的讀寫事務(wù)進(jìn)行檢查，采用SVA斷言進(jìn)行描述如下：

// requirement： enables are 1hot0

a_en_1hot0： assert property （@（posedge clk） $onehot0（{rd_en， wr_en}） ）;

// requirement： only read one word at a time from fifos （pulse check）

a_rd_en_pulse： assert property （@（posedge clk） disable iff （！rstn） $rose（rd_en） |=> ！rd_en ）;

a_wr_en_pulse： assert property （@（posedge clk） disable iff （！rstn） $rose（wr_en） |=> ！wr_en ）;

通過Questa Formal工具的屬性檢查PropCheck對(duì)設(shè)計(jì)進(jìn)行形式化驗(yàn)證，屬性檢查的結(jié)果如圖3所示。

結(jié)果顯示有1處斷言失敗，說明設(shè)計(jì)存在缺陷。通過PropCheck的GUI界面進(jìn)行錯(cuò)誤定位，并確定問題的出處。如圖4所示，檢查時(shí)間不到1 s。

在圖5中看到斷言觸發(fā)處的rd_en和wr_en同時(shí)為高，觸發(fā)了1hot0斷言，錯(cuò)誤定位到仲裁器的源代碼中的wr_en和rd_en的邏輯描述地方，發(fā)現(xiàn)137和151行ratio[2]&both_avail的邏輯是相同的，這與“ratio寄存器控制如何寫入和讀取，當(dāng)兩個(gè)信號(hào)都可用時(shí)，wr_en信號(hào)優(yōu)先，該寄存器的MSB應(yīng)該是1”違背。

修改151行wr_en的控制邏輯為：

if （（～ra_avail & wr_avail） | （ratio[2] & both_avail））。

再次對(duì)設(shè)計(jì)進(jìn)行檢查，結(jié)果如圖7所示，與第一次的檢查結(jié)果比較，發(fā)現(xiàn)觸發(fā)斷言失敗個(gè)數(shù)減少1個(gè)，1hot0的斷言被證明。最終所有斷言失敗被定位、分析、迭代，最終所有斷言都通過。

4? 結(jié)? 論

形式化驗(yàn)證是窮盡式數(shù)學(xué)技術(shù)，專注于證實(shí)模塊的端到端、直接對(duì)應(yīng)微架構(gòu)規(guī)范的高層要求，可幫助用戶極大地提高項(xiàng)目設(shè)計(jì)和驗(yàn)證的產(chǎn)能，同時(shí)確保正確性。近年來，形式化驗(yàn)證技術(shù)有了長足的進(jìn)步，將其與FPGA軟件數(shù)字仿真相結(jié)合是提高FPGA驗(yàn)證充分性和完備性的關(guān)鍵一步，但如何在工程實(shí)踐中更大的發(fā)揮效能還有待進(jìn)一步研究。

參考文獻(xiàn)：

[1] 劉斌.芯片驗(yàn)證漫游指南 [M].北京：電子工業(yè)出版社，2018.

[2] BERGERON J，CUERY E，HUNTER A，et al.SystemVerilog驗(yàn)證方法學(xué)[M].夏宇聞，楊雷，陳先勇，等譯.北京：北京航空航天大學(xué)出版社，2007.

[3]陳先勇，徐偉俊，楊鑫，等. SystemVerilog斷言及其應(yīng)用 [J].中國集成電路，2007（9）：19-24.

[4] 斯皮爾.SystemVerilog驗(yàn)證測試平臺(tái)編寫指南 [M].張春，麥宋平，趙益新，譯.北京：科學(xué)出版社，2019.

[5] VIJAYARAGHAVAN S，RAMANATHAN M. System Verilog Assertions 應(yīng)用指南 [M].陳俊杰，等譯.北京：清華大學(xué)出版社，2006.

作者簡介：陳軍花（1990.03—），女，漢族，湖北黃岡人，中級(jí)工程師，畢業(yè)于南京航空航天大學(xué)，碩士研究生，研究方向：FPGA和IC驗(yàn)證測試;石顥（1980.11—），男，漢族，重慶人，高級(jí)工程師，畢業(yè)于重慶大學(xué)，碩士研究生，研究方向：FPGA和IC驗(yàn)證測試;柴金寶（1993.09—），男，漢族，黑龍江哈爾濱人，初級(jí)工程師，畢業(yè)于南京理工大學(xué)，碩士研究生，研究方向：FPGA和IC驗(yàn)證測試。