天天新动态：AveMC工具学习

(一) 什么是AveMC?

AveMC是一款高效的用于前端数字集成电路功能验证的EDA软件。不同于传统的仿真验证工具软件，AeMC基于形式化验证方法学，用模型验证(Model Checking)的方法进行完备的功能验证。模型检验不使用用户定义的激励输入，而是用户将电路规格(Sepcification)用设计属性(property) 和断言(assertion) 描述出来，然后采用数理证明的方式证明设计属性和断言在任何情况下都与RTL设计一致。相比于传统的仿真验证方法学，采用AveMC进行模块级功能验证，具有高效、完备的优势。

【资料图】

(二) AveMC的工作逻辑?

AveMC 前端组件会将待测试的设计 DUT (Design under test，RTL行为级可综合代码)和证环境 (testbench = SVA + 属性 + 一些综合的Veriloa/Svstem Verloo辅助逻辑) -同读入，并对它们进行数学建模，然后将建模结果交给 AVeMC 验证引警进行证明。证明结果会通过文字报告、图形界面波形显示、自动生成仿真复现 testbench 等方式交由用户进行 Debug 和结果统计(通常就是指所有断言/属性的证明结果以及覆盖率报告)。

(三) AveMC验证应用场景?

在数字前端功能验证领域，AveMC可以应用于以下验证场景:

1.模块级验证交付。即在模块级，采用 AVeMC 作为主要的验证手段，利用形式化验证方法学完备性的优势，进行完整的功能验证。

2.Bug Hunting。在某些复杂的关键模块中，采用 AVeMC 作为一种辅助的验证手段，尽可能去发现 corner case 中隐藏的 bug。这些 bug 通常很难通过仿真或者其他验证手段发现。

3.Bug 重现。在系统级或原型验证时发现的 bug，如果是模块的功能 bug，经常需要在模块级进行 bu 重现。AVeMC 可以通讨自动产生错误波形和 testbench 的方式帮助用户在模块级自动重现 bug。

4.Bug 修复检验。对 Bug 进行修复之后，可以用 AVeMC 进行完备验证，以保证该 bug 修复的够完全修复问题并不会影响其他能。

5.逻辑等价性检查。AveMC 还提供 AveMC SEC检查工具，帮助用户检查在设计经过了修改之后，是否和原有的设计在功能逻辑上保持了一致性。

6.冗余代码检查。AveMC Coverage 检查工具，可以帮助用户发现 RTL 中的冗余代码。

(四) AveMC的多种debug方式?

图形化运行界面

波形查看器 RTL 查看器: AveMC 提供了图形化界面的波形调试器和 RTL 查看器 AveTrace。AveTrace 以 AveMC的结果作为输入，提供了如下功能:

RTL 查看