軌道交通設備中FPGA芯片等效性驗證方法

陳 光 鄭桂燕 劉偉超

（北京全路通信信號研究設計院集團有限公司，北京 100073）

?

軌道交通設備中FPGA芯片等效性驗證方法

陳 光 鄭桂燕 劉偉超

（北京全路通信信號研究設計院集團有限公司，北京 100073）

摘要：FPGA芯片綜合及布局布線后的功能驗證對于保證設計可靠性有重要意義，目前常用的后仿真驗證方法存在兩個問題，一個是復雜度大時間較長，另一個是異常狀態的測試覆蓋率不足。提出利用等效性檢查進行功能驗證的方法，并給出主流廠商芯片的驗證流程及異常處理措施。與后仿真的驗證方法相比，本方法驗證工作量更低，測試覆蓋率高，對提高設計可靠性有重要作用。

關鍵詞：等效性檢查；FPGA驗證；Formality軟件；Conformal LEC軟件

Abstract:Veri fi cation of the FPGA netlist generated by Synthesis or Place & Route has great importance for ensuring the design reliability. The post-synthesis simulation method widely used now has two major problems. One is the complexity with a long process, the other is the test coverage de fi ciency. The paper puts forward a verification method using equivalence checking and presents the verification process of FPGAs from majority manufacturers and the false treatment solutions. Comparing with post-synthesis simulation method, the equivalence checking method has lower cost and higher test coverage and would bene fi t greatly the design reliability.

Keywords:equivalence checking; FPGA veri fi cation; Formality; Conformal LEC

1　概述

隨著我國軌道交通的發展，越來越多的集成電路芯片被應用于軌道交通設備中，其中現場可編程門陣列（Field Programmabel Gate Array，FPGA）芯片由于其具有可編程、高集成度、高速和高可靠性等優點[1]，逐漸由外圍器件演變為數字邏輯系統的核心，承擔起關鍵作用。為保證設備的可靠運行，FPGA的邏輯功能驗證工作尤為重要。

在FPGA開發流程中，寄存器傳輸級（Register Transfer Level，RTL）行為描述邏輯功能的正確性可由前仿真驗證。但綜合[2]級結構描述的同時，為了提高時序或減少資源消耗[3]，綜合器會采取例如組合邏輯削減、狀態機重編碼、寄存器合并或復制等的優化算法，導致最終產生的網表結構與原始描述并非一一對應，因此代碼前仿真功能正確不代表綜合后及布局布線后的網表功能完全正確，驗證工作除應對代碼進行仿真測試外，還應包括對網表的檢查。

2　綜合后網表功能驗證方法分析

FPGA綜合后網表功能驗證目前通常利用仿真進行，即在布局布線后對結果進行后仿真。該方法以綜合后或布局布線后導出的網表為測試對象，將測試激勵向量輸入到待測對象，通過檢查輸出來判斷功能是否正確。通常后仿真的測試案例及測試向量需能夠覆蓋前仿真，通過對比前仿真的結果來驗證功能是否出現錯誤。但該方法的執行存在兩個難點，導致后仿真驗證并不被一般項目采用。

首先，后仿真時間開銷較大。由于綜合及布局布線后的門級網表中包含了所有實際存在的邏輯單元，因此仿真器的計算量較前仿真大大增加，從而導致運算速度嚴重降低，例如一個6萬門占用率80%時鐘頻率30 MHz的FPGA設計，前仿真1 ms實際耗時約1 s，但后仿真1 ms實際耗時約4 s。對于目前動輒幾十萬上百萬門級的大規模FPGA芯片，或者對于仿真時間長度及時鐘頻率有更高要求的設計，仿真時間的消耗嚴重影響產品開發進度。

其次，后仿真驗證時，衡量測試覆蓋率的指標目前通常使用語句覆蓋率和分支覆蓋率，但對于一些異常狀態（如狀態機的異常跳轉）依然缺少測試覆蓋。對程序正常工作不會出現異常狀態的仿真需要人為對寄存器進行強制賦值，這種操作難度較高，且工作量巨大。假設有N個寄存器，那么最差情況下需要人為設置的狀態則有2^（N-1）-1個，當N較大時，仿真驗證幾乎不可能完成。為更好地說明，可用如下代碼為例進行分析：

process(clk，nrst)

begin

if nrst = '0' then

cnt<= "000000";

elsif rising_edge(clk) then

if cnt<= "100000" then

cnt<= cnt + "000001";

else

cnt<= "100001";

end if;

end if;

end process;

假設代碼走讀與前仿真已經驗證該段代碼功能的正確性，在網表的功能驗證中，由于正常運行中cnt不會大于“100001”，因此，需要人為將cnt設置“100010”～“111111”共30個狀態，并檢查輸出是否為預期的“100001”，工作量大大增加。

是否可以使用另一種編碼風格，來避免以上代碼仿真時人為設置的工作量？例如將累加器拆分為一個1位的進位寄存器與一個5位的累加寄存器，這樣進位寄存器的2種值與累加寄存器的32種值都會被自然運行到。但需要注意的是，進位寄存器與累加寄存器的某些組合狀態依然是自然運行不可達的狀態，必須強制賦值，并不能減少測試工作量。

因此，需要有一種不借助測試向量即可對所有可能的情況進行驗證的方法來提高工作效率，保證驗證工作的順利進行，而ASIC設計常用的等效性檢查方法恰好可以解決以上兩個難點。下面，就等效性檢查進行具體的描述。

3　等效性檢查

在設計ASIC芯片的時候，設計者除了要考慮如何按照要求設計出正確的電路外，還要考慮設計電路在物理層實現后，原本在RTL級正確的邏輯關系是否還會保證不出錯。等效性檢查[4]是對參考設計與待驗證設計之間邏輯形式和功能一致性的驗證，是靜態驗證方法中的一種，它借用數學上的方法將待驗證電路和功能描述直接進行比較，有成熟工具可以使用，無需開發測試向量?，F有工具經過多年ASIC設計使用，可信度較高，且工具軟件中使用的算法包括多層迭代、邏輯相互關聯，可保證工具不會對某個單一邏輯漏判或錯判。等效性檢查可用于驗證寄存器傳輸級設計與門級網表之間、門級網表與門級網表之間功能是否一致。當確認設計的功能仿真正確性以后，設計實現的每一個步驟的結果都可以與上個步驟的結果做等效性檢查，不需再重復功能仿真，可以節省大量驗證工作的時間。

邏輯錐是等效性檢查的常用劃分單位，其含義如圖1所示，其中方形代表觸發器/鎖存器，不規則形代表組合邏輯等其他異步邏輯，觸發器與組合邏輯共同組成邏輯錐。檢查工具首先將參考設計和待驗證設計中的觸發器進行一對一或一對多的映射，其次檢查具有映射關系的邏輯錐輸入來源是否相同以及輸入數據相同情況下輸出是否相同，當比對結果為相同認為二者等效，否則為不等效。由于檢查對象可覆蓋所有基本邏輯單元，因此可達到100%的測試覆蓋率。

常用的等效性檢查工具包括Synopsys公司的Formality軟件以及Cadence公司的Conformal Logic Equivalence Check軟件。

軟件對綜合工具及其優化策略、輸入文件格式等均有一定限制，Formality支持DC Ultra 或Design Compiler Graphical的所有默認選項，其支持的輸入格式包括[5]：Synopsys DC，DDC，Milkyway；SystemVerilog；Verilog （1995，2001）；VHDL（87，93）；IEEE 1801 Unified Power Format；Spice。Conformal支持的輸入格式包括[6]Verilog（1995，2001，2005）；SystemVerilog；VHDL（87，93）；Spice；Edif；Liberty；Mixed Languages。

4　常用芯片的驗證流程

由于等效性檢查常用于ASIC設計，而FPGA設計受器件廠商及其開發工具的限制，其文件格式、綜合算法、標準單元庫均不受控，無法像ASIC設計過程中一樣方便導出需使用的過程文件，因此FPGA驗證雖可利用工具進行，但其過程較為復雜，且不同FPGA廠家需使用的方法不同。以下，將對幾個主流芯片廠商的FPGA等效驗證方法進行描述。

4.1Xilinx

Formality可支持Xilinx的FPGA驗證，包括RTL與綜合后網表之間以及RTL與布局布線后網表之間的等效性檢查。以綜合工具為Synopsys的FCII為例，驗證過程如下。

4.1.1RTL與綜合后網表

1）使用綜合工具FCII對程序進行綜合；

2）使用ISE集成的NDG2VER程序產生網表；

3）使用Perl腳本xilinx2formality.pl產生Formality兼容的網表；

4）使用Xilinx提供的unisim.fms及simprims. fms將庫文件讀入Formality；

5）使用Perl腳本core2formal.pl產生Formality兼容的IP核的網表；

6）使用Synopsys提供的makeconstraints.sh讀入FCII產生的報告，將其中被合并的寄存器信息添加到Formality的命令文件set_constraint中，在執行驗證前調入該命令文件；

7）在執行驗證前設置verification_merged_ duplicated_registers變量，以兼容綜合時執行的最大扇出控制；

8）若使用Formality進行等效性檢查，盡量減少retiming的使用，若已使用，則需對變量set_ paramiter-retimed進行設置；

9）執行驗證。

4.1.2RTL與布局布線后網表

1）對程序進行綜合、映射及布局布線；

2）使用ISE集成的NGD2VER程序產生網表；

3）使用xilinx2formality.pl產生Formality兼容的網表以及與映射算法相關的Formality約束文件；

4）執行驗證。

4.2Altera

Altera可利用Conformal LEC軟件進行等效性檢查，過程如下。

1）使用QuartusII集成綜合工具，在綜合前對EDA工具進行設置，如果使用QuartusII集成綜合工具，Design Entry/Synthesis選擇None，使用SynplifyPro則選擇SynplifyPro；Fromal Verification選擇Conformal LEC；

2）編譯過程應選擇增量編譯，可在Category選項中選擇Incremental Compilation，或使用Tcl命令打開增量編譯：set_global_assignmen -name INCREMENTAL_COMPILATION FULL_ INCREMENTAL_COMPILATION；

3）對綜合優化選項進行設置，在Physical Synthesis Optimization中關閉Perform register retiming；

4）在Optimize for fitting中，關閉以下兩個選項：Perform physical synthesis forcombinational logic，Perform logic to memory mapping，以防止將邏輯綜合為RAM；

5）對工程進行完整的編譯；

6）編譯后Quartus II軟件產生一系列用于驗證的文件，存儲路徑為/fv/ conformal；

7）將生成的腳本復制到UNIX環境下，啟動Conformal LEC軟件；

8）在File選項中，選擇Do Dofile，選擇/fv/conformal/.ctc，自動執行并完成驗證。

4.3Actel

Actel系列FPGA未見官方的驗證手冊，因此尚不明確對于調用了核的設計如何進行驗證。但對于未調用特定電路功能的程序IP核的設計，可以用通用的方法來進行驗證，以下為使用Conforml LEC軟件的驗證過程。

1）對設計進行綜合，綜合選項中應避免使用retiming、FSM reconding等會導致寄存器無法一一對應的優化選項，若使用Synplify Pro還應注意選擇Conservative Register Optimization，否則綜合結果優化程度較高，某些語句會被作為死代碼屏蔽掉；

2）Designer中對設計進行編譯及布局布線，完成后利用Back-Annotate導出.v或.vhd的布局布線后的網表文件；

3）啟動Conformal LEC，SETUP模式下，讀入設計前設置黑盒，例如對于模塊ULSICC_INT，設置命令為：add notranslate module ULSICC_ INT-Revised；

4）讀入源代碼，SETUP模式下，由GUI界面設置Format，Type為GOLDEN，選中RTL的源文件，對應的命令為：read design/.../xxx.vhd /.../ xxx2.vhd -VHDL -Golden；

5）讀入綜合后或布局布線后網表，SETUP模式下，Type為Revised，選中網表文件及庫文件，對應的命令為：read design/.../Netlist.vhd /.../ lib.vhd -VHDL-Revised，注意，由于Actel未提供底層庫文件與驗證軟件的接口，因此需要人工編寫庫文件，作為Revised文件調入，而非作為庫調入；

6）LEC模式下進行驗證，GUI界面選擇run-> compare；

7）可由GUI界面查詢結果，或使用命令report compare data>result將結果導出到名為result的文件中，完成驗證。

5　幾種虛假不等的解決措施

由于EDA軟件的算法限制，等效性檢查的工作過程并非一次性的，而是一個互動循環的過程。為了確認等效性檢查覆蓋到全部邏輯，可對代碼中的寄存器進行統計，與比對結果中的總寄存器數目進行比對，由于EDA軟件算法不會自行創建節點，因此可保證在數目相同的情況下，軟件完成了全部邏輯的比對。

此外，一次比對結果得出后，可能將一些正確電路識別為錯誤電路，即產生虛假不等項。因此需要根據其比對結果，人為的對軟件添加約束，消除虛假不等項，再次比對甚至循環操作幾次才能得到正確的結果。以下為Conformal LEC軟件幾個常見虛假不等項的解決措施。

1）寄存器復制

在綜合及布局布線階段，高扇出的信號會影響電路時序性能及布通率[7]。為了控制扇出數從而提高時序性能，某些高扇出寄存器會被復制，從而避免一個寄存器驅動過多器件。默認情況下，寄存器復制會使待驗證網表中的寄存器多于參考設計，從而導致復制出的寄存器無法映射，同時導致受復制寄存器驅動的寄存器比對失敗。解決措施是在SETUP模式下，使用以下命令：set flatten model -all_seq_merge。

2）寄存器反相

某些綜合工具會利用插入反相器的方式增強總線驅動能力。為了配合反相器的插入，原始寄存器的輸出也會反相，導致與參考設計中的功能不一致，且受反相器驅動的寄存器同樣會比對失敗。以參考設計中寄存器flag_reg為例，解決措施是在LEC模式下，應用如下命令：invert mapped points u1/ flag_reg–golden。

3）寄存器對應關系錯誤

Conformal LEC軟件在對參考設計與待驗證設計的寄存器進行映射過程中需要遵循一定策略，例如按功能映射或按命名映射，可以通過制定命名規則來提高映射成功率。但某些情況下，即使設置了一定的命名規則，仍然無法保證全部寄存器都被正確映射，可能會出現映射錯誤的情況，從而得出錯誤比對結果。為解決這一問題，應在LEC模式下，首先在mapping manager的mapped points里面刪除錯誤配對的信號；然后在mapping manager 的unmapped points中指定一個為mapping target再與另一欄中想要對應的信號共同重新加入。兩個步驟對應的命令腳本為：

delete compared points u4/u43/sig_s_reg -golden

add mapped points u4/u43/cnt_reg[0] u4/ u43/cnt[0]/Q_reg–noinvert。

6　結論

本文介紹了利用等效性檢查工具對FPGA綜合及布局布線后邏輯進行驗證的方法，詳細給出了目前常用FPGA廠商的驗證步驟及常見問題解決方案。該方法利用數學方法對網表的功能正確性進行驗證，不需要開發復雜的測試向量，縮短了開發時間，并可保證100%的驗證覆蓋率，對于更大規模的FPGA產品開發及提高設計可靠性有著重要意義。

參考文獻

[1]楊海鋼，孫嘉斌，王慰.FPGA器件設計技術發展概述[J].電子與信息學報，2010，32（3）：714-727.

[2] Deniziak S.A.A symbolic RTL synthesis for LUT-based FPGAs[C].//Proceedings of the 12th International Symposium on Design and Diagnostics of Electronic Circuits & Systems.Liberec：IEEE，2009：102-107.

[3] Cong J，Minkovich K.Optimality study of logic synthesis for LUT-based FPGAs[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2007, 26（2）：230-239.

[4]舒適，唐長文，閔昊.ASIC綜合后的靜態驗證方法的研究[J].微電子學，2004，34（1）：56-59.

[5] Formality and Formality Ultra:Equivalence Checking for DC Ultra and Design Compiler Graphical[EB/OL].2013[2014-07-14].http:// www.synopsys.com/Tools/Verification/FormalEquivalence/Documents/ formality_ds.pdf.

[6] Encounter Conformal Equivalence Checker:Fomal verification technology for fast and accurate bug detection and correction[EB/ OL].2012[2014-07-14].http://www.cadence.com/rl/Resources/ datasheets/encounter_conformal_EC_ds.pdf.

[7]崔秀海，楊海鋼，郝亞男，等.基于時延和信號扇出數的時序優化裝箱算法[C].//中國電子學會電路與系統學會第二十二屆年會論文集.上海:中國電子學會，2020：382-389.

收稿日期：（2014-08-25）

DOI:10.3969/j.issn.1673-4440.2016.01.019