陈军花 石颢 柴金宝

摘  要：验证是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验证测试。