本课程假设学习者具备数字设计原理和硬件描述语言（HDL）的基础知识，熟悉SVA语言虽非必需但会有所帮助。拥有形式验证方面的经验更为有利，但并非必要条件。具备集成电路设计或验证相关背景者优先。要求具备基本编程能力和数字逻辑知识，并能够使用形式验证工具来执行SVA断言。

随着形式验证技术的持续发展，无论是形式化工具的性能，还是相关方法学，这些年来都取得了显著提升。形式验证在行业内也逐渐受到广泛关注。在芯片验证领域最具影响力的技术大会DVCon上，与形式验证相关的主题演讲逐年增多。这些演讲展示了形式验证技术在实际项目中的应用情况，业内主要的芯片设计公司也分享了具体的应用案例。

在验证设计功能时，形式验证具备独特的可证真优势。这一特点已逐步得到设计和验证工程师的认可。越来越多的工程师将形式验证视为一项必须掌握的重要技能，开始主动学习如何将其应用于各自项目，并探索其在传统仿真方法之外所带来的额外价值。

在项目中有效部署形式验证的前提是具备编写高质量属性的能力。属性编码是将形式验证引入实际设计流程中的第一步。SystemVerilog Assertions（SVA）为表达设计意图、描述功能预期以及实现自动形式检查提供了一种标准且强大的手段。

本课程“形式化验证SVA编码”的目标是帮助工程师掌握SVA属性编写的关键技术和实践方法。通过学习这项技能，工程师能够为形式验证建立坚实基础，充分利用工具的自动化能力，从而提高验证的深度和设计的可靠性。本课程内容将引导学习者理解如何在形式验证环境下构建、完善并应用基于属性的验证策略。

1、在形式验证中，验证的对象是属性检查。需要从这些模块的规格中逐一识别适合形式验证的设计模块，并抽象其功能特性。使用基于属性的语言将这些特性转化为对应的属性，构建基于属性的形式验证测试平台，并将 RTL 设计代码与属性检查进行对比，以验证 RTL 设计代码的功能是否满足设计规范的要求。

2、随着形式技术研究的成熟并逐渐达到行业所需的复杂程度，我们必须采取措施以确保成功过渡到这种更高要求的阶段。其中一步是从根本上改变设计方法论，从模糊的自然语言规格转向数学上精确且可验证的规格形式。形式属性验证是这一方法学变革的关键因素。最终结果是通过更深入理解设计空间、改善设计意图的沟通以及提升验证质量来提高设计质量。

3、SVA 是 SystemVerilog 语言的一部分，由行业标准 IEEE1800 定义。SVA 是一种属性描述语言，其基本语法由四个层次组成：布尔表达式、序列、属性以及验证指令。

4、SVA 从验证的角度描述设计的行为，使用属性描述设计应做与不应做的事情。课程提供了多种使用 SVA 语言的实用方法，以及推荐的编码风格、常见 SVA 问题及其规避方法，以及不同 SVA 放置方式的优缺点。

5、对于效率低下的 SVA，其创建和调试需要耗费大量时间。效率低下的 SVA 问题不仅限于工具和技术，还涉及许多人为因素，使属性难以理解，并在维护和复用方面带来巨大问题。在形式验证中，所有 SVA 和设计代码都需要由综合工具建模为状态空间，它们都是复杂性的一部分，因此 SVA 的效率尤为重要。

6、在基于属性的验证环境中，通常需要大量辅助 HDL 代码，而 SVA 的比例往往较小。通过创建辅助代码，可以让属性的编写更加简单、可读性更强且易于理解。使用辅助代码还能帮助工具更容易地评估验证问题，并缩短工具运行时间。SVA 语言存在一些局限性，面对复杂设计时，SVA 语言根本无法完整描述，必须借助辅助代码来帮助建模和构建这些设计行为。

7、基于断言的验证测试平台的开发通常需要大量时间和精力，因此需要考虑验证环境（如模型、断言、假设、覆盖点等）的可复用性。对于一些常见的设计模块，可以开发并封装成基于断言的验证组件，使其更加标准化和通用化，从而成为基于断言的验证 IP。在形式验证过程中，更多地使用此类验证 IP，可以显著减少搭建验证环境的时间，并有助于提高验证工作的效率和质量。