形式验证：独家方法论 2022 (FVM)
与顶级正式专家一起获得开始正式验证和升级您的正式技术所需的一切
讲师：Peter Yo
口袋资源独家Udemy付费课程，独家中英文字幕，配套资料齐全！
用不到1/10的价格，即可享受同样的高品质课程，且可以完全拥有，随时随地都可以任意观看和分享。
你会学到什么
- 有效地使用形式验证
- 描述影响正式工具结果的问题
- 使用系统化流程通过形式化方法进行验证
- 在形式验证中应用属性检查
- 对正式签核方法有一定了解
- 将正式签核应用于正确的设计块
- 了解正式应用程序的不同形式验证使用模型
要求
- IC数字设计与验证基础知识
描述
关于本课程
形式化验证技术涵盖的范围非常广泛，Methodology是该技术的基础，我们的课程将主要关注形式化验证方法论。通过对方法论的学习和了解，我们可以对形式化验证技术有一个初步的了解。这门课程可以作为我们跨入形式化验证领域的一步，为后期在具体实践中应用该技术打下不可或缺的基础。
课程目标
本课程解答了形式化验证领域的诸多基本问题，阐述了形式化验证底层技术的基本原理，提出了最新的形式化签核方法论，阐述了形式化验证领域的技术发展方向。通过学习本课程，您将对形式化验证技术有一定的了解，以及一些形式化方法论的基础知识。让我们首先看一下本课程的一些基本目标。
- 形式化验证的使用效率一直是个大问题，正确的方法必不可少。关于这个问题，我们将在本课程中学到很多关于如何有效使用形式验证的知识。
- 形式化验证的过程高度依赖于工具的使用。用户需要对工具的底层技术有一定的了解，才能更好的发挥形式化验证的优势。在这里我们可以学习到如何分析理解形式化验证工具的验证结果，对于不同的结果会有不同的反应。
- 为了合理有效地使用形式验证，往往需要将整个验证过程作为一个整体来考虑，以发挥形式验证的作用。在系统化过程中，将形式化方法应用于验证过程是非常必要的。
- 形式验证的目标是以属性检查的形式。根据Spec的描述，将设计功能的特征一一抽象提取出来，并将这些提取的特征通过基于属性的语言进行翻译和表达。然后搭建平台环境进行基于属性的形式化测试，与设计RTL代码中的功能进行对比，验证设计功能的正确性。
- 形式验证，由于其经过充分验证的性质，可以对设计模块进行完整的功能验证，并且可以作为最终功能签核交付。本课程提供了全面的正式签核方法。
- 形式化验证追求的是充分证明，这对形式化工具来说一直是一个相当大的挑战。目前形式化工具在计算能力方面还存在一定的局限性，这也使得形式化验证的适用设计范围不像仿真那样随意。因此，正式签核需要适当的设计模块。
- 除了sign-off，形式验证还有很多简单易用的形式化应用。这些开箱即用的应用程序针对不同的验证问题提供了相应的形式化解决方案，使没有形式化验证技术背景的初学者或工程师能够快速高效地解决验证中遇到的一些问题。
课程议程
- 形式验证概述
在本章中，我们将介绍什么是形式化验证、它的历史视角、当前趋势、为什么需要它、它的要求、它的挑战、形式化验证工具供应商、主要供应商工具特性的比较以及形式化能力水平。
- 形式验证简介
在本章中，我们将介绍形式验证框架、编译形式模型、形式模型概念、检查断言、假设、（影响锥）COI、应用证明算法、形式证明结果以及形式证明性能、性能特征、形式化工具设置和控制、形式化调试、形式化引擎访问、形式化验证和仿真比较、形式化验证和仿真的区别、形式化验证的投资回报率、何时使用形式化验证、形式化属性验证、形式化验证应用。
- 正式签核
在本章中，我们将介绍属性检查、属性检查指南、端到端属性检查、约束开发、正式签核实现、正式签核的挑战和奖励、ROI 和正式签核标准、正式签核跟踪、正式签核流、正式签核测试台、正式签核环境、复杂性的定义、复杂性的度量、代码和功能覆盖的定义、覆盖的度量类型、覆盖的可控性和可观察性、覆盖测量后的动作。
- 使用 Full Prove 正式签核
在本章中，我们将介绍具有完整证明流程的正式签核、环境简化、断言简化、断言简化方法中的功能拆分、断言简化中的位宽拆分、辅助断言、设计简化中的参数化、设计中的分区设计缩减，设计缩减中的黑盒，模型抽象，初始值抽象，绑定证明，过度约束和错误搜索。
- 正式签收报道
在本章中，我们将介绍带有覆盖流程的正式签核、正式覆盖、正式覆盖的类型、正式覆盖的模型、正式覆盖的度量、正式覆盖的度量、正式覆盖的标准、正式覆盖的方法论、验证问题, signoff with coverage strategy, CDV, full-prove, coverage 三种验证流程的对比。
- 形式验证申请
随着形式验证应用程序的开箱即用特性越来越被接受，它在验证领域变得越来越流行。目前，各大形式验证工具供应商都在不断推出自己的形式验证应用。在本章中，我们将介绍一些当今最常用的形式验证应用程序。
关键词
SystemVerilog、Verilog、VHDL、断言、SystemVerilog 断言、属性规范语言、SVA、PSL
布尔值、序列、属性、断言、假设、覆盖
形式化、验证、基于断言的验证、ABV
Jasper、JasperGold、jg、IFV、IEV、Magellan、Hector、VC Formal、Questa Formal、OneSpin、Calypto、0-in
Cadence、Synopsys、Mentor、Siemens、Atrenta、Real Intent、Avery、Zocalo、Arcas、Veriforma、Oski、Paradigm Works、TVS
本课程适合谁：
- 正规工程师
- RTL 设计工程师
- 知识产权设计师
- 验证工程师
- DV 经理系统架构师
- DV经理
