在芯片设计领域，验证是确保设计正确的关键环节。动态仿真（Dynamic Simulation）长期以来是验证的主流方法，工程师通过覆盖率（Coverage）指标衡量验证的完整性。然而，随着设计复杂度飙升，传统仿真耗时剧增，而形式化验证（Formal Verification, FV）凭借其“穷举证明”的特性，成为发现极端场景漏洞的利器。但长期以来，FV难以独立承担验证签核（Sign-off）的重任——原因很简单：缺乏一套与仿真对标的覆盖率标准。

本文将通过一个来自英特尔的实际案例，解析如何通过覆盖率驱动的形式化验证方法论，打破这一瓶颈，让FV真正成为可量化、可信任的签核工具。

为什么传统FV无法直接用于签核？

形式化验证的核心是通过数学证明，穷举所有可能的设计行为。理论上，只要断言（Assertions）覆盖所有功能需求，就能实现100%验证。但现实往往骨感：

1. 过度约束陷阱
   FV环境中的约束条件可能无意中限制了合法状态空间的覆盖。例如，设计中的某些合法状态可能因约束过紧而未被探索，导致潜在漏洞被遗漏。

2. 有界证明的挑战
   复杂设计的验证可能因资源限制只能完成“有界证明”（Bounded Proof），即仅覆盖部分状态空间。此时如何判断验证是否足够充分？

传统FV工具虽然提供代码覆盖率指标（如Cone of Influence Coverage），但这些指标无法直接对应动态仿真的功能覆盖率，导致验证团队难以直观评估FV的进度和完整性。

破局关键：用仿真思维重构FV流程

英特尔的解决方案核心是“同语言，双驱动”——让FV的覆盖率指标与动态仿真对齐，并通过以下三步实现闭环：

步骤1：制定“形式化验证计划”（FV Vplan）

• 需求分类：将功能需求拆解为三类——
  • 生成需求（Generate）：定义输入约束条件（如信号时序规则）。
  • 检查需求（Check）：通过断言（Assertions）验证设计行为。
  • 覆盖需求（Cover）：通过覆盖点（Coverpoints）确保关键场景被触发。
• 工具无关性：需求描述独立于验证方法（FV或仿真），便于后续混合验证。

例如，针对一个微序列器（Micro-sequencer）的验证需求：

// 检查需求：当输入A满足条件时，输出B必须在下一周期拉高  
assert property (@(posedge clk) trigger_A |-> ##1 output_B);  

// 覆盖需求：记录所有触发A条件的场景  
covergroup cg_trigger_A;  
  coverpoint trigger_A { bins active = {1}; }  
endgroup

步骤2：构建覆盖率驱动的FV流水线

• 断言与覆盖点绑定：每个检查需求必须对应覆盖需求，确保验证场景的“触发-检查”闭环。
• 三阶段覆盖闭合：
  1. 代码覆盖率：确保所有RTL代码分支可被FV约束激活（排除死代码）。
  2. 功能覆盖率：通过半形式化（Semi-Formal）技术突破有界证明限制，探索深层状态。
  3. 混合验证：对仿真友好的模块（如长序列逻辑）保留动态仿真，对并发控制逻辑采用FV。

步骤3：统一覆盖率报告

• 跨方法融合：将FV与仿真的覆盖率结果合并，生成单一指标（如“总覆盖率98%”）。
• 签核标准：
  • 功能覆盖率100%（覆盖点全触发且断言无失败）。
  • 代码覆盖率100%（允许豁免死代码）。
  • 所有断言需完全证明或有充分深度的有界证明。

实际效果：ROI提升30%的验证革命

在英特尔的一个微序列器项目中，该方法实现了纯FV签核。其成果包括：

成果1：设计文档质量飞跃

• 70%的需求被完善：FV迫使设计文档精确化。例如，原需求“当输入激活时设置V_PENDING”被细化到时钟周期级条件。
• 早期发现架构缺陷：通过断言反推，5个关键漏洞在RTL编码前即被修正。

成果2：验证效率倍增

• 测试平台代码量减少75%：FV测试平台仅需4000行代码（仿真需2万行）。
• 覆盖率闭合时间减半：通过形式化引擎自动探索，覆盖率达标时间缩短2倍。

成果3：混合验证的灵活优势

在另一序列器设计中，团队对长序列逻辑使用仿真，对并发控制逻辑采用FV。最终：

• 验证周期缩短30%：并行执行FV与仿真，避免资源闲置。
• 覆盖率置信度提升：通过跨方法覆盖融合，遗漏场景接近零。

未来展望：让FV成为验证标配

这一方法论的价值不仅在于技术突破，更在于改变了验证团队的工作范式：

• 管理者可通过统一覆盖率指标，直观对比FV与仿真的进展。
• 工程师能针对模块特性选择最优方法，无需被方法论“绑架”。

下一步，团队计划将流程扩展到IP级验证，并探索AI辅助的覆盖率自动生成技术。正如论文作者所言：“当FV能说仿真的语言，它就不再是黑科技，而是工程师手中的另一把瑞士军刀。”

参考文献：

• 本文核心观点来自英特尔团队论文《A Coverage-Driven Formal Methodology for Verification Sign-off》（DVCon 2019）。
• 工具实现细节可参考Cadence JasperGold、Synopsys VC Formal等商业FV工具文档。

「数字芯片设计【不定期更新文件】」链接：https://pan.quark.cn/s/27331927a18e