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

（二）AveMC的工作逻辑？

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

 （三）AveMC验证应用场景？

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

1. 模块级验证交付。即在模块级，采用 AveMC 作为主要的验证手段，利用形式化验证方法学完备性的优势，进行完整的功能验证。
2. Bug Hunting。在某些复杂的关键模块中，采用 AveMC 作为一种辅助的验证手段，尽可能去发现 corner case 中隐藏的 bug。这些 bug 通常很难通过仿真或者其他验证手段发现。
3. Bug 重现。在系统级或原型验证时发现的 bug，如果是模块的功能 bug，经常需要在模块级进行 bug 重现。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 查看
  • 信号 drive/load 追踪
  • 波形查看
  • 波形和 RTL 联动调试
• 空泛性检查报告：如果一个属性表达式存在一个冗余的子表达式，子表达式没有影响到整个属性表达式的正确性，那么这个属性就叫空泛性属性，包括：
  • 断言前置条件空泛性检查
  • 断言子序列空泛性检查
• 覆盖率结果报告：精确检查断言属性的覆盖率状况，帮助提高形式化验证testbench的质量，包括：
  • 代码覆盖率：衡量验证约束的完整性
  • 断言覆盖率：检查断言检查功能的完整性
  • 功能覆盖率：用断言描述的覆盖检查点，用于检查功能覆盖率