轨道交通设备中FPGA芯片等效性验证方法
2016-04-01郑桂燕刘伟超
陈 光 郑桂燕 刘伟超
（北京全路通信信号研究设计院集团有限公司，北京 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]是对参考设计与待验证设计之间逻辑形式和功能一致性的验证，是静态验证方法中的一种，它借用数学上的方法将待验证电路和功能描述直接进行比较，有成熟工具可以使用，无需开发测试向量。现有工具经过多年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软件产生一系列用于验证的文件，存储路径为
7）将生成的脚本复制到UNIX环境下，启动Conformal LEC软件；
8）在File选项中，选择Do Dofile，选择
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
