一、形式验证方法学
（一）什么是形式化验证？
形式化验证方法学是使用数学证明的方法，分析设计中所有可能的状态空间来验证设计是否符合预期。形式化验证方法主要有三个方面的应用：定理证明、模型检验和等价性检查。
（二）与传统验证的区别？
- 仿真的验证方法学类似于进行枚举法，每一个测试用例测试一个特定的场景。
- 形式化验证达到的效果等价于穷举法。形式化验证在实现的时候，并不是真的采取了穷举的方式，而是采取了数理证明的方式来证明在所有的情况下，某些断言一定成立或存在反例。不需要用户去生成测试激励，一条属性的真伪结论是基于严格的数学证明——证明为真的属性在任何激励下再进行仿真都不会出错。
二、AveMC工具学习
（一）什么是AveMC？
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可以应用于以下验证场景：
- 模块级验证交付。即在模块级，采用 AveMC 作为主要的验证手段，利用形式化验证方法学完备性的优势，进行完整的功能验证。
- Bug Hunting。在某些复杂的关键模块中，采用 AveMC 作为一种辅助的验证手段，尽可能去发现 corner case 中隐藏的 bug。这些 bug 通常很难通过仿真或者其他验证手段发现。
- Bug 重现。在系统级或原型验证时发现的 bug，如果是模块的功能 bug，经常需要在模块级进行 bug 重现。AveMC 可以通过自动产生错误波形和 testbench 的方式帮助用户在模块级自动重现 bug。
- Bug 修复检验。对 Bug 进行修复之后，可以用 AveMC 进行完备验证，以保证该 bug 修复能够完全修复问题并不会影响其他功能。
- 逻辑等价性检查。AveMC 还提供 AveMC SEC检查工具，帮助用户检查在设计经过了修改之后，是否和原有的设计在功能逻辑上保持了一致性。
- 冗余代码检查。AveMC Coverage 检查工具，可以帮助用户发现 RTL 中的冗余代码。
（四）AveMC的多种debug方式？
- 图形化运行界面
- 波形查看器 /RTL 查看器：AveMC 提供了图形化界面的波形调试器和 RTL 查看器——AveTrace。AveTrace 以 AveMC的结果作为输入，提供了如下功能：
- RTL 查看
- 信号 drive/load 追踪
- 波形查看
- 波形和 RTL 联动调试
- 空泛性检查报告：如果一个属性表达式存在一个冗余的子表达式，子表达式没有影响到整个属性表达式的正确性，那么这个属性就叫空泛性属性，包括：
- 断言前置条件空泛性检查
- 断言子序列空泛性检查
- 覆盖率结果报告：精确检查断言属性的覆盖率状况，帮助提高形式化验证testbench的质量，包括：
- 代码覆盖率：衡量验证约束的完整性
- 断言覆盖率：检查断言检查功能的完整性
- 功能覆盖率：用断言描述的覆盖检查点，用于检查功能覆盖率
