形式验证及其在芯片工程中的应用-电子发烧友网

一：形式验证的基本概念

-> 广义上的形式验证？

形式验证不仅仅是芯片领域中的一个概念。正如文章开头提到过，形式验证强调使用严格的数学推理和形式化技术，以确保系统的行为是否符合预期的性质和规格。所以说只要是可以通过量化方式构建数学模型的系统，都可以使用形式验证来check其功能性以及其他可量化特性。比如：

软件工程：就拿区块链举个例子。形式验证不仅适用于智能合约本身，还适用于与智能合同交互的去中心化应用。这可以帮助确保整个应用的安全性和正确性。
金融领域：金融交易的验证是非常重要的，特别是在高频交易和算法交易领域。形式验证可以确保交易的正确性和合规性，防止错误交易和潜在的风险。

-> 芯片工程里的形式验证？

这里拿计数器举一个简单的形式验证示例。请注意，这只是一个简化的示例，实际的形式验证可能涉及更复杂的设计和性质。

假设有一个4位的计数器电路，可以从0计数到15。我们想要验证以下性质：当计数器的值达到最大值15时，下一个计数值应该是0。

设计：计数器电路有一个4位的计数器寄存器，可以递增。当计数器值达到15时，下一个时钟周期应该将计数器重置为0。

形式验证属性：我们使用SystemVerilog的属性规约 （SVA） 来表达这个性质。（一般形式验证的case都使用SVA来编写)以下是一个简化的属性规约示例：

property reset_at_max;
  @(posedge clk) disable iff (!rst_n)
    (count == 4'b1111) |= > (next_count == 4'b0000);
endproperty

assert property (reset_at_max);

在这个属性规约中，我们定义了一个属性 reset_at_max ，它表达了当计数器值为15时，下一个计数值应为0。这个属性在时钟上升沿触发时进行检查。如果属性不满足，将会产生一个验证错误。

在这个示例中，使用仿真进行验证可能需要执行多个时钟周期来验证所有可能的计数序列。但是，使用形式验证可以直接进行数学推理，验证属性在所有可能的情况下是否成立.

除此之外，与基于仿真的验证不同，基于仿真的验证会使用各种输入情景来测试设计以确保其正确行为，形式验证涉及数学分析以验证设计的属性。这些属性可以包括功能正确性、安全性、安全性以及某些类型错误的缺失（例如，竞态条件、死锁等）。

二：形式验证的优势

从上述的例子看来，那么形式验证要优于基于仿真的验证？看似高性能的形式验证，要将它发挥得淋漓尽致也是需要代价的。

其实不然，形式验证也面临着挑战。它可能计算成本高昂，需要专门的专业知识来制定属性并设置验证过程。通常与其他验证技术（如仿真和测试）结合使用，以提供全面的验证策略。形式验证和基于仿真的验证各有其优势和局限性，没有绝对的优劣之分。选择哪种验证方法取决于具体的设计需求、时间和资源限制以及设计的复杂性。

形式验证VS动态仿真

->形式验证的特点：

高度可靠性 ：形式验证提供了数学证明的可靠性，如果设计通过了形式验证，那么可以有很大的信心认为设计是正确的。
全面性 ：形式验证可以覆盖所有可能的状态，从而捕获设计中的所有潜在错误，包括一些难以通过仿真检测到的问题。
对于复杂设计 ：对于复杂的设计，特别是关键性能的设计，形式验证可以帮助发现隐藏的问题和时序错误。

->动态仿真验证的特点：

易于实施 ：基于仿真的验证通常比形式验证更容易实施，可以快速验证设计的基本功能和常见情况。
资源效率高 ：在一些情况下，形式验证可能需要更多的计算资源和时间，而基于仿真的验证可能更具资源效率。
快速迭代 ：基于仿真的验证允许设计团队迅速进行修改和验证，特别适用于快速迭代的设计流程。

可见，trade-off的概念在芯片领域里面处处可见。鱼与熊掌不可得兼。

三：在芯片验证中实现形式验证

形式验证主要由以下几个部分组成：

性质（Properties） ：这些是描述设计所需属性和规格的语句，例如时序关系、状态转换、约束等。常用的
规约语言 ：通常使用形式规约语言，如 SystemVerilog Assertions（SVA）、Property Specification Language（PSL）等，来编写性质和约束。
定理证明器（Theorem Provers） ：这些工具用于推理和证明性质是否成立。它们基于形式化逻辑和推理规则来验证性质。
模型检查器（Model Checkers） ：这些工具用于穷举系统状态空间，检查是否存在满足性质的状态序列。

在电子设计自动化 （EDA） 工具中，许多主要的形式验证工具已经集成到综合工具链中，以帮助硬件工程师验证他们的设计。这些工具通常基于硬件描述语言 （如Verilog或VHDL） 。

比如：

1. Cadence JasperGold ：JasperGold是一个集成式形式验证平台，支持属性规约和模型检查，广泛应用于验证硬件设计。

2. Synopsys VC Formal ：VC Formal是Synopsys的形式验证工具，用于验证功能、时序和系统级性质。