1. 签核交付工程总览

在数字芯片与IP的交付链条中，“签核”不是一次简单的仿真通过，而是一组有明确证据、明确责任人和明确验收口径的工程活动。Xcelium与Jasper分别承担动态仿真验证与形式化验证两条主线的签核任务：Xcelium以激励驱动的方式覆盖时序行为、协议交互和系统场景，Jasper以数学穷举的方式证明或反证属性、等价性和安全性。两者不是替代关系，而是互补关系——动态仿真回答“在给定激励下是否出现错误”，形式化回答“在所有合法输入下是否可能出错”。签核交付工程的核心，就是把这两类证据组织成可追溯、可复现、可评审的交付包。

一、签核流程中的定位：两条证据链的交汇

从流程位置看，Xcelium通常位于模块级、子系统级和SoC级验证的中后段，承接UVM环境、回归用例和覆盖率收敛；Jasper通常位于模块级和关键控制逻辑的前中段，承接属性提取、断言验证、等价性检查和X-propagation分析。两者在签核节点上交汇：动态仿真提供覆盖率与场景通过率，形式化提供属性证明与反例波形。签核评审时，评审人需要同时看到“覆盖率是否达标”和“关键属性是否全部证明”，缺一不可。

一个常见的误区是把Jasper当作“补充手段”，只在仿真跑不动时才启用。实际上，在签核交付工程中，Jasper的证明结果往往具有更高的确定性权重：一旦属性被证明，就不需要再依赖随机激励的覆盖程度。因此，合理的策略是先用Jasper收敛控制逻辑和接口协议的核心属性，再用Xcelium覆盖数据通路、性能场景和系统集成行为。

二、交付物定义：从“跑过了”到“可评审”

签核交付物不是仿真日志的堆砌，而是经过整理、可追溯、可复现的证据集合。Xcelium侧的核心交付物包括：回归通过率报告、功能覆盖率与代码覆盖率合并数据库、失败用例清单及根因分析、覆盖率豁免申请与批准记录。Jasper侧的核心交付物包括：属性证明报告（proven/cex/unreachable分类统计）、反例波形及根因分析、等价性检查报告、X-propagation分析结果、约束合理性评审记录。

两类交付物最终汇入统一的签核包，通常包含以下字段：签核对象（模块/IP/SoC）、签核版本（RTL commit ID）、工具版本（Xcelium/Jasper版本号）、运行环境（OS、license、机器配置）、用例/属性清单、通过/证明状态、未关闭项及责任人、评审结论。这些字段不是形式主义，而是当后续版本出现回归问题时，能够快速定位“当时签核的是哪个版本、哪些项被豁免、谁批准的”。

三、团队角色与协作接口

签核交付工程涉及四类核心角色：验证工程师（DV）、形式化工程师（FV）、设计工程师（RTL）和签核评审人（Sign-off Reviewer）。DV负责Xcelium环境搭建、用例编写、回归执行和覆盖率收敛；FV负责Jasper属性提取、证明收敛、反例分析和约束评审；RTL负责修复设计缺陷、提供设计意图说明和时钟复位定义；评审人负责确认证据完整性、判据合理性和豁免项合规性。

协作接口的关键在于“问题传递”和“证据回传”。当Jasper发现反例时，FV需要将反例波形、触发属性、约束条件和复现脚本打包传递给RTL和DV；RTL修复后，DV需要在Xcelium中补充对应场景的定向用例，FV需要重新证明该属性。当Xcelium发现覆盖率空洞时，DV需要判断是激励不足还是设计不可达，前者补充用例，后者提交豁免申请并附上Jasper的unreachable证明作为依据。

四、签核交付的常见风险与判断依据

签核交付工程中最常见的风险不是工具跑不起来，而是“证据看起来完整但实际不可信”。典型情况包括：Jasper约束过强导致属性被虚假证明；Xcelium覆盖率通过但关键场景未被激励；签核版本与最终交付版本不一致；豁免项未经评审直接关闭。判断签核是否真正完成，不能只看“通过率100%”或“proven数量”，而要检查三个一致性：签核版本与交付版本一致、签核判据与项目验收标准一致、豁免项与评审记录一致。

在实际项目中，建议在签核启动前先冻结RTL版本和工具版本，生成签核范围清单，明确哪些模块走Xcelium签核、哪些走Jasper签核、哪些需要双签。签核过程中，每周同步一次未关闭项和豁免申请，避免在签核截止前集中处理导致评审质量下降。签核完成后，交付包应包含完整的复现脚本和运行命令，使第三方能够在相同环境下复现签核结果——这是签核交付工程区别于普通验证活动的最终标志。