C2RTL

C代码与RTL代码的功能等效性检查

C2RTL：C代码与RTL代码的功能等效性检查

越来越多公司开始采用C++编写参考模型，尤其是对算法要求较高的CPU/GPU/AI/DSP等整数和浮点设计，都会有对应的C模型。对同一个功能模块，用不同的语言，由不同的人员分别实现，可以尽量避免犯同样的设计错误。然后通过co-simulation，比较两个实现的功能是否一致来发现设计中的问题。通常这种测试方法结合UVM框架下实现。

目前，RTL功能验证基本上还是random simulation，随机产生输入向量，检查输出跟提前用其它方式计算好的结果是否一致。或者是co-simulation，比如通过UVM框架对C和RTL的实现同时跑随机产生的输入向量，然后检查两个实现的输出结果是否相等。这种方式存在以下缺陷：  
1、输入向量基本上是完全随机的或者简单的constraint random。完全遍历所有输入组合不现实。  
2、因为无法遍历所有输入组合，通常只能依赖于覆盖率统计，比如行覆盖、分支覆盖是否有提升来评估代码的质量。现实中因为代码不可达，实际覆盖率不可能达到100%。  
3、覆盖率的提升只能提高对设计功能正确的信心，但无法保证有cornel case没有测试到。  
4、很难用这种方式复现现有的bug，有针对性地造一个特殊的场景case。  
形式化验证的出现弥补了随机仿真不完备的问题，通过对源代码分析和建模，使用定理证明和约束求解的方式证明属性在所有求解空间下是否都满足。如果属性不满足，还可以自动生成输入向量，用于复现该问题。
对于unit level的设计，其实完全可以使用形式化验证技术证明两个设计的等价性。ATEC ( A Tool for Equivalence Checking) 是一款形式化验证工具，可用于验证C/C++ vs RTL，RTL vs RTL，C/C++ vs C/C++的等价性。ATEC适用于Unit Level或Super Unit Level模块的验证。ATEC有以下突出的优势和特点：  
1.  支持C/C++作为参考模型。  
2.  可以用boolean formula约束设计的行为，描述直接自然。  
3.  对于两个C/C++/RTL设计，证明在约束范围内的输入，功能都等价。  
4.  如果被证明不等价，自动生成输入向量，比如testbench。  
5.  除了用于证明完全等价，还能用于证明输出结果在一定误差范围内。  
6.  利用自动生成输入向量的功能，很容易用于复现现有的bug。
ATEC最核心的模块。包括问题的建模以及后端求解引擎。 
 

1. 支持C-RTL、C-C、RTL-RTL的等价性验证。 支持C/C++/Verilog编写的模型互相之间的等价

2. 提供IEEE754浮点黄金参考模型（golden model），支持浮点运算。 对于FPU的RTL设计，可以直接用ATEC验证是否满足IEEE754标准。ATEC自带的参考模型在多家芯片设计厂商抓到过RTL的bug。 

3. 提供常用的数学函数，比如fabs/pow/sqrt。 可以直接使用常用的数学函数。

4. 支持Clockgating的验证，完备验证gating enable/disable的功能一致性。 为了解决耗电问题，通常使用clock gating的技术将部分逻辑暂时关闭。使用ATEC可以完备地验证clock gating的正确性。 

5. 证明失败的assertion，可自动生成复现的trace，以testbench的形式给出（可自由选择仿真器）。 失败的断言自动生成反例。默认自动打开波形，方便debug。 

6. 支持blackbox，合理使用black box可验证更大的Design。 Black box是一种分而治之的验证方法。对于已经验证的子模块，可以使用black box将这部分逻辑化简，从而可验证更大的Design。

7. 支持多个不同频率的clock，支持clock domain。 可以设置多个clock，其中一个作为基准clock，其它clock用基准clock的频率关系表示。

8. 支持SVAcover property的验证。  对于感兴趣的行为，可以使用cover property描述，ATEC将自动检查和生成对应的trace。
9. 支持简单的SVAassume property，支持SVA assert property的验证。  可以支持简单的SVA。
10. 支持集群并行运算，充分利用计算资源，节省运行时间。  可利用bsub集群，将任务分散到集群中不同机器上执行。  

11. 支持Floatinglicense，局域网内共用license。  支持浮动license，只需要在一台机器上启动license。  

12. 支持booleanformula的验证，包括>/>=/</<=，可验证误差可控，不要求必须完全等价。  虽然称为等价性验证工具，实际上任何boolean formula都可以验证。常见的比如浮点结果的误差在0.000001。  

13. 可约束Design的行为（输入以及输入之间的关系约束），例如输入的值大于0小于8。  可以用接近自然语言的描述约束Design的行为。  

14. 支持不同latency的两个RTL的验证。  可以验证用不同算法、pipeline实现的两个RTL的等价。比如一个固定在第4个时钟上升沿出结果，一个在第2～3个时钟上升沿出结果。  

15. 支持条件等价，例如valid为1时才比较输出等价。验证等价时，可以指定前提条件。

Top