陳 光 鄭桂燕 劉偉超

（北京全路通信信號(hào)研究設(shè)計(jì)院集團(tuán)有限公司，北京 100073）

?

軌道交通設(shè)備中FPGA芯片等效性驗(yàn)證方法

陳 光 鄭桂燕 劉偉超

（北京全路通信信號(hào)研究設(shè)計(jì)院集團(tuán)有限公司，北京 100073）

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

關(guān)鍵詞：等效性檢查；FPGA驗(yàn)證；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　概述

隨著我國(guó)軌道交通的發(fā)展，越來(lái)越多的集成電路芯片被應(yīng)用于軌道交通設(shè)備中，其中現(xiàn)場(chǎng)可編程門(mén)陣列（Field Programmabel Gate Array，F(xiàn)PGA）芯片由于其具有可編程、高集成度、高速和高可靠性等優(yōu)點(diǎn)[1]，逐漸由外圍器件演變?yōu)閿?shù)字邏輯系統(tǒng)的核心，承擔(dān)起關(guān)鍵作用。為保證設(shè)備的可靠運(yùn)行，F(xiàn)PGA的邏輯功能驗(yàn)證工作尤為重要。

在FPGA開(kāi)發(fā)流程中，寄存器傳輸級(jí)（Register Transfer Level，RTL）行為描述邏輯功能的正確性可由前仿真驗(yàn)證。但綜合[2]級(jí)結(jié)構(gòu)描述的同時(shí)，為了提高時(shí)序或減少資源消耗[3]，綜合器會(huì)采取例如組合邏輯削減、狀態(tài)機(jī)重編碼、寄存器合并或復(fù)制等的優(yōu)化算法，導(dǎo)致最終產(chǎn)生的網(wǎng)表結(jié)構(gòu)與原始描述并非一一對(duì)應(yīng)，因此代碼前仿真功能正確不代表綜合后及布局布線后的網(wǎng)表功能完全正確，驗(yàn)證工作除應(yīng)對(duì)代碼進(jìn)行仿真測(cè)試外，還應(yīng)包括對(duì)網(wǎng)表的檢查。

2　綜合后網(wǎng)表功能驗(yàn)證方法分析

FPGA綜合后網(wǎng)表功能驗(yàn)證目前通常利用仿真進(jìn)行，即在布局布線后對(duì)結(jié)果進(jìn)行后仿真。該方法以綜合后或布局布線后導(dǎo)出的網(wǎng)表為測(cè)試對(duì)象，將測(cè)試激勵(lì)向量輸入到待測(cè)對(duì)象，通過(guò)檢查輸出來(lái)判斷功能是否正確。通常后仿真的測(cè)試案例及測(cè)試向量需能夠覆蓋前仿真，通過(guò)對(duì)比前仿真的結(jié)果來(lái)驗(yàn)證功能是否出現(xiàn)錯(cuò)誤。但該方法的執(zhí)行存在兩個(gè)難點(diǎn)，導(dǎo)致后仿真驗(yàn)證并不被一般項(xiàng)目采用。

首先，后仿真時(shí)間開(kāi)銷較大。由于綜合及布局布線后的門(mén)級(jí)網(wǎng)表中包含了所有實(shí)際存在的邏輯單元，因此仿真器的計(jì)算量較前仿真大大增加，從而導(dǎo)致運(yùn)算速度嚴(yán)重降低，例如一個(gè)6萬(wàn)門(mén)占用率80%時(shí)鐘頻率30 MHz的FPGA設(shè)計(jì)，前仿真1 ms實(shí)際耗時(shí)約1 s，但后仿真1 ms實(shí)際耗時(shí)約4 s。對(duì)于目前動(dòng)輒幾十萬(wàn)上百萬(wàn)門(mén)級(jí)的大規(guī)模FPGA芯片，或者對(duì)于仿真時(shí)間長(zhǎng)度及時(shí)鐘頻率有更高要求的設(shè)計(jì)，仿真時(shí)間的消耗嚴(yán)重影響產(chǎn)品開(kāi)發(fā)進(jìn)度。

其次，后仿真驗(yàn)證時(shí)，衡量測(cè)試覆蓋率的指標(biāo)目前通常使用語(yǔ)句覆蓋率和分支覆蓋率，但對(duì)于一些異常狀態(tài)（如狀態(tài)機(jī)的異常跳轉(zhuǎn)）依然缺少測(cè)試覆蓋。對(duì)程序正常工作不會(huì)出現(xiàn)異常狀態(tài)的仿真需要人為對(duì)寄存器進(jìn)行強(qiáng)制賦值，這種操作難度較高，且工作量巨大。假設(shè)有N個(gè)寄存器，那么最差情況下需要人為設(shè)置的狀態(tài)則有2^（N-1）-1個(gè)，當(dāng)N較大時(shí)，仿真驗(yàn)證幾乎不可能完成。為更好地說(shuō)明，可用如下代碼為例進(jì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;

假設(shè)代碼走讀與前仿真已經(jīng)驗(yàn)證該段代碼功能的正確性，在網(wǎng)表的功能驗(yàn)證中，由于正常運(yùn)行中cnt不會(huì)大于“100001”，因此，需要人為將cnt設(shè)置“100010”～“111111”共30個(gè)狀態(tài)，并檢查輸出是否為預(yù)期的“100001”，工作量大大增加。

是否可以使用另一種編碼風(fēng)格，來(lái)避免以上代碼仿真時(shí)人為設(shè)置的工作量？例如將累加器拆分為一個(gè)1位的進(jìn)位寄存器與一個(gè)5位的累加寄存器，這樣進(jìn)位寄存器的2種值與累加寄存器的32種值都會(huì)被自然運(yùn)行到。但需要注意的是，進(jìn)位寄存器與累加寄存器的某些組合狀態(tài)依然是自然運(yùn)行不可達(dá)的狀態(tài)，必須強(qiáng)制賦值，并不能減少測(cè)試工作量。

因此，需要有一種不借助測(cè)試向量即可對(duì)所有可能的情況進(jìn)行驗(yàn)證的方法來(lái)提高工作效率，保證驗(yàn)證工作的順利進(jìn)行，而ASIC設(shè)計(jì)常用的等效性檢查方法恰好可以解決以上兩個(gè)難點(diǎn)。下面，就等效性檢查進(jìn)行具體的描述。

3　等效性檢查

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

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

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

軟件對(duì)綜合工具及其優(yōu)化策略、輸入文件格式等均有一定限制，F(xiàn)ormality支持DC Ultra 或Design Compiler Graphical的所有默認(rèn)選項(xiàng)，其支持的輸入格式包括[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　常用芯片的驗(yàn)證流程

由于等效性檢查常用于ASIC設(shè)計(jì)，而FPGA設(shè)計(jì)受器件廠商及其開(kāi)發(fā)工具的限制，其文件格式、綜合算法、標(biāo)準(zhǔn)單元庫(kù)均不受控，無(wú)法像ASIC設(shè)計(jì)過(guò)程中一樣方便導(dǎo)出需使用的過(guò)程文件，因此FPGA驗(yàn)證雖可利用工具進(jìn)行，但其過(guò)程較為復(fù)雜，且不同F(xiàn)PGA廠家需使用的方法不同。以下，將對(duì)幾個(gè)主流芯片廠商的FPGA等效驗(yàn)證方法進(jìn)行描述。

4.1Xilinx

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

4.1.1RTL與綜合后網(wǎng)表

1）使用綜合工具FCII對(duì)程序進(jìn)行綜合；

2）使用ISE集成的NDG2VER程序產(chǎn)生網(wǎng)表；

3）使用Perl腳本xilinx2formality.pl產(chǎn)生Formality兼容的網(wǎng)表；

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

5）使用Perl腳本core2formal.pl產(chǎn)生Formality兼容的IP核的網(wǎng)表；

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

7）在執(zhí)行驗(yàn)證前設(shè)置verification_merged_ duplicated_registers變量，以兼容綜合時(shí)執(zhí)行的最大扇出控制；

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

9）執(zhí)行驗(yàn)證。

4.1.2RTL與布局布線后網(wǎng)表

1）對(duì)程序進(jìn)行綜合、映射及布局布線；

2）使用ISE集成的NGD2VER程序產(chǎn)生網(wǎng)表；

3）使用xilinx2formality.pl產(chǎn)生Formality兼容的網(wǎng)表以及與映射算法相關(guān)的Formality約束文件；

4）執(zhí)行驗(yàn)證。

4.2Altera

Altera可利用Conformal LEC軟件進(jìn)行等效性檢查，過(guò)程如下。

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

2）編譯過(guò)程應(yīng)選擇增量編譯，可在Category選項(xiàng)中選擇Incremental Compilation，或使用Tcl命令打開(kāi)增量編譯：set_global_assignmen -name INCREMENTAL_COMPILATION FULL_ INCREMENTAL_COMPILATION；

3）對(duì)綜合優(yōu)化選項(xiàng)進(jìn)行設(shè)置，在Physical Synthesis Optimization中關(guān)閉Perform register retiming；

4）在Optimize for fitting中，關(guān)閉以下兩個(gè)選項(xiàng)：Perform physical synthesis forcombinational logic，Perform logic to memory mapping，以防止將邏輯綜合為RAM；

5）對(duì)工程進(jìn)行完整的編譯；

6）編譯后Quartus II軟件產(chǎn)生一系列用于驗(yàn)證的文件，存儲(chǔ)路徑為/fv/ conformal；

7）將生成的腳本復(fù)制到UNIX環(huán)境下，啟動(dòng)Conformal LEC軟件；

8）在File選項(xiàng)中，選擇Do Dofile，選擇/fv/conformal/.ctc，自動(dòng)執(zhí)行并完成驗(yàn)證。

4.3Actel

Actel系列FPGA未見(jiàn)官方的驗(yàn)證手冊(cè)，因此尚不明確對(duì)于調(diào)用了核的設(shè)計(jì)如何進(jìn)行驗(yàn)證。但對(duì)于未調(diào)用特定電路功能的程序IP核的設(shè)計(jì)，可以用通用的方法來(lái)進(jìn)行驗(yàn)證，以下為使用Conforml LEC軟件的驗(yàn)證過(guò)程。

1）對(duì)設(shè)計(jì)進(jìn)行綜合，綜合選項(xiàng)中應(yīng)避免使用retiming、FSM reconding等會(huì)導(dǎo)致寄存器無(wú)法一一對(duì)應(yīng)的優(yōu)化選項(xiàng)，若使用Synplify Pro還應(yīng)注意選擇Conservative Register Optimization，否則綜合結(jié)果優(yōu)化程度較高，某些語(yǔ)句會(huì)被作為死代碼屏蔽掉；

2）Designer中對(duì)設(shè)計(jì)進(jìn)行編譯及布局布線，完成后利用Back-Annotate導(dǎo)出.v或.vhd的布局布線后的網(wǎng)表文件；

3）啟動(dòng)Conformal LEC，SETUP模式下，讀入設(shè)計(jì)前設(shè)置黑盒，例如對(duì)于模塊ULSICC_INT，設(shè)置命令為：add notranslate module ULSICC_ INT-Revised；

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

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

6）LEC模式下進(jìn)行驗(yàn)證，GUI界面選擇run-> compare；

7）可由GUI界面查詢結(jié)果，或使用命令report compare data>result將結(jié)果導(dǎo)出到名為result的文件中，完成驗(yàn)證。

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

由于EDA軟件的算法限制，等效性檢查的工作過(guò)程并非一次性的，而是一個(gè)互動(dòng)循環(huán)的過(guò)程。為了確認(rèn)等效性檢查覆蓋到全部邏輯，可對(duì)代碼中的寄存器進(jìn)行統(tǒng)計(jì)，與比對(duì)結(jié)果中的總寄存器數(shù)目進(jìn)行比對(duì)，由于EDA軟件算法不會(huì)自行創(chuàng)建節(jié)點(diǎn)，因此可保證在數(shù)目相同的情況下，軟件完成了全部邏輯的比對(duì)。

此外，一次比對(duì)結(jié)果得出后，可能將一些正確電路識(shí)別為錯(cuò)誤電路，即產(chǎn)生虛假不等項(xiàng)。因此需要根據(jù)其比對(duì)結(jié)果，人為的對(duì)軟件添加約束，消除虛假不等項(xiàng)，再次比對(duì)甚至循環(huán)操作幾次才能得到正確的結(jié)果。以下為Conformal LEC軟件幾個(gè)常見(jiàn)虛假不等項(xiàng)的解決措施。

1）寄存器復(fù)制

在綜合及布局布線階段，高扇出的信號(hào)會(huì)影響電路時(shí)序性能及布通率[7]。為了控制扇出數(shù)從而提高時(shí)序性能，某些高扇出寄存器會(huì)被復(fù)制，從而避免一個(gè)寄存器驅(qū)動(dòng)過(guò)多器件。默認(rèn)情況下，寄存器復(fù)制會(huì)使待驗(yàn)證網(wǎng)表中的寄存器多于參考設(shè)計(jì)，從而導(dǎo)致復(fù)制出的寄存器無(wú)法映射，同時(shí)導(dǎo)致受復(fù)制寄存器驅(qū)動(dòng)的寄存器比對(duì)失敗。解決措施是在SETUP模式下，使用以下命令：set flatten model -all_seq_merge。

2）寄存器反相

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

3）寄存器對(duì)應(yīng)關(guān)系錯(cuò)誤

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

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　結(jié)論

本文介紹了利用等效性檢查工具對(duì)FPGA綜合及布局布線后邏輯進(jìn)行驗(yàn)證的方法，詳細(xì)給出了目前常用FPGA廠商的驗(yàn)證步驟及常見(jiàn)問(wèn)題解決方案。該方法利用數(shù)學(xué)方法對(duì)網(wǎng)表的功能正確性進(jìn)行驗(yàn)證，不需要開(kāi)發(fā)復(fù)雜的測(cè)試向量，縮短了開(kāi)發(fā)時(shí)間，并可保證100%的驗(yàn)證覆蓋率，對(duì)于更大規(guī)模的FPGA產(chǎn)品開(kāi)發(fā)及提高設(shè)計(jì)可靠性有著重要意義。

參考文獻(xiàn)

[1]楊海鋼，孫嘉斌，王慰.FPGA器件設(shè)計(jì)技術(shù)發(fā)展概述[J].電子與信息學(xué)報(bào)，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]舒適，唐長(zhǎng)文，閔昊.ASIC綜合后的靜態(tài)驗(yàn)證方法的研究[J].微電子學(xué)，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]崔秀海，楊海鋼，郝亞男，等.基于時(shí)延和信號(hào)扇出數(shù)的時(shí)序優(yōu)化裝箱算法[C].//中國(guó)電子學(xué)會(huì)電路與系統(tǒng)學(xué)會(huì)第二十二屆年會(huì)論文集.上海:中國(guó)電子學(xué)會(huì)，2020：382-389.

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

DOI:10.3969/j.issn.1673-4440.2016.01.019