FPGA軟件形式化驗證技術研究

陳軍花 石顥 柴金寶

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

關鍵詞：FPGA;形式化驗證;SVA

中圖分類號：TN79+1? ? ? ? ? ? ? 文獻標識碼：A 文章編號：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? 引? 言

在芯片設計流程中，驗證占整個芯片設計流70%的人力物資源，流片失敗的原因70%是由驗證不充分導致的功能錯誤。

由于FPGA設計復雜度的不斷提升，為功能驗證帶來了前所未有的挑戰。因為設計擁有越多的信號個數，可能出現的信號組合將會呈現爆炸式的增長，所以通過仿真器達到各種情景組合的100%覆蓋幾乎是不可能的。

1? FPGA功能驗證現狀

1.1? 功能仿真的局限性

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

雖然目前有諸如人工設計測試用例序列、隨機測試激勵生成等基于仿真的傳統驗證技術[1]，可以從一定程度上提高FPGA單元/配置項級設計的驗證質量，但定向測試的仿真驗證技術中依然存在明顯的關鍵難題。

以兩個小型設計為例，以便更好地理解功能驗證的瓶頸所在。

1.2? 功能仿真的不完備性

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

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

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

保守估計，狀態空間為2（49個寄存器+10輸入）=259，即5.76×1017，假設一個非常快的邏輯仿真器，以每秒100萬個時鐘周期運行。如果我們運行所有這些狀態，需要的時間5.76×1017秒，約為18 279年。

如上分析，一旦意識到完備驗證場景（狀態空間）的驚人規模，一組人工創建的定向測試無法執行所有狀態就不足為奇了。在許多情況下，考慮到設計和驗證團隊技術能力、經驗的差別，驗證不完備性的缺點將會再次放大。

1.3? 功能仿真的不充分性

以一個簡單的數學題為例：

3B3=65 865

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

由于仿真引擎本身只不過是一個計算工具，它可執行你提供的任何激勵，并輸出結果，如果設計的測試用例沒有猜出答案，通過仿真將永遠不會知道正確的答案。

通過以上分析，功能仿真驗證用例集由人工設計，難以確保和評估用例集的充分性;此外，仿真驗證還需要消耗相當的人力資源和時間成本，進行測試用例開發、測試環境搭建和具體調試。

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

2? 形式化驗證

FPGA設計的形式化驗證，是指工具通過自動分析電路中的邏輯結構來推導出是否有極端的情況，使預先設定的設計規則有可能無法滿足。由于這種驗證不需要用戶的測試向量，并且可以對電路做窮舉法驗證，因此，對于某些傳統驗證手段無法做到但是又至關重要的電路，就必須采用形式化驗證這種手段來保證設計的可靠性。

2.1? FPGA形式化驗證應用場景

形式化方法目前主要的應用場景為定理證明、模型檢驗、等價性檢驗，針對FPGA軟件，主要使用模型檢驗和等價性檢驗[1]。

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

等價性檢驗主要目的是用來對兩個電路的設計、設計規范及實現之間進行邏輯功能的等價性檢驗。或者在設計經過變換之后，窮盡地檢查變換前后的功能一致性，表明設計的變換沒有產生功能的變化。

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

2.2? SVA斷言

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

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

一條SVA并發斷言由四種不同層次的結構組成。布爾表達式（booleans）是最基礎的單元，有信號及其邏輯關系運算符構成，用以表示某個邏輯事件的發生。布爾表達式在時間上的組合構成了序列（sequence）。屬性（property）是在仿真或形式化驗證中被驗證的單元。屬性將序列通過邏輯或者有序地組合起來生成更復雜的序列。屬性在斷言聲明中被調用。斷言采用assert、assume、cover中的任一一種關鍵字進行聲明。

3? 項目應用

以某型號軟件中AXI4Lite到APB4橋接設計邏輯功能驗證為例，如圖2所示，設計實現為采用仲裁器（Pin MUX模塊）來確定APB4總線主控制端的讀寫事務。

其中需檢驗的功能之一就是確定仲裁器中的信號是否存在同時有效的情況出現，即返回表達式中只有一個1或全為0，則表示仲裁功能實現正確，否則功能實現錯誤。根據該需求對上述的APB4總線主控端的讀寫事務進行檢查，采用SVA斷言進行描述如下：

// 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對設計進行形式化驗證，屬性檢查的結果如圖3所示。

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

在圖5中看到斷言觸發處的rd_en和wr_en同時為高，觸發了1hot0斷言，錯誤定位到仲裁器的源代碼中的wr_en和rd_en的邏輯描述地方，發現137和151行ratio[2]&both_avail的邏輯是相同的，這與“ratio寄存器控制如何寫入和讀取，當兩個信號都可用時，wr_en信號優先，該寄存器的MSB應該是1”違背。

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

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

再次對設計進行檢查，結果如圖7所示，與第一次的檢查結果比較，發現觸發斷言失敗個數減少1個，1hot0的斷言被證明。最終所有斷言失敗被定位、分析、迭代，最終所有斷言都通過。

4? 結? 論

形式化驗證是窮盡式數學技術，專注于證實模塊的端到端、直接對應微架構規范的高層要求，可幫助用戶極大地提高項目設計和驗證的產能，同時確保正確性。近年來，形式化驗證技術有了長足的進步，將其與FPGA軟件數字仿真相結合是提高FPGA驗證充分性和完備性的關鍵一步，但如何在工程實踐中更大的發揮效能還有待進一步研究。

參考文獻：

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

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

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

[4] 斯皮爾.SystemVerilog驗證測試平臺編寫指南 [M].張春，麥宋平，趙益新，譯.北京：科學出版社，2019.

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

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