1. CDC/RDC形式验证工程导入
在数字集成电路设计中，跨时钟域（Clock Domain Crossing，CDC）和复位域跨越（Reset Domain Crossing，RDC）问题是最难通过传统验证手段彻底覆盖的一类缺陷。它们往往不会在功能仿真中稳定复现，却可能在芯片上电、时钟切换或复位释放的瞬间引发亚稳态传播、数据丢失或状态机跑飞。Jasper CDC/RDC 正是针对这一类问题而生的形式验证工具，它把"是否存在跨域结构、是否存在亚稳态传播路径、是否存在复位释放顺序冲突"从依赖激励的仿真问题，转化为对设计结构的穷尽性数学分析问题。
工具定位：结构分析而非激励驱动
Jasper CDC/RDC 属于静态形式验证工具，其核心工作方式是读取 RTL 或网表，自动识别时钟域、复位域、同步器结构，然后对跨域路径进行结构遍历与形式化证明。它与动态仿真、传统静态检查（Lint）三者的差异可以用一句话概括：仿真验证"在给定激励下是否出错"，Lint 检查"是否违反编码规则"，而 Jasper CDC/RDC 证明"在所有可能条件下是否存在跨域风险"。
具体来说，动态仿真需要构造跨域场景的激励，而亚稳态本身无法在 RTL 仿真中真实建模，只能通过同步器模型近似；Lint 工具基于模式匹配，能发现缺少同步器这类明显问题，但无法判断同步器级数是否足够、无法分析复位域之间的释放顺序依赖；Jasper CDC/RDC 则通过结构化的时钟域划分和形式化引擎，对每一条跨域路径给出"已同步/未同步/需人工确认"的判定，并能对同步器有效性、复位顺序、毛刺传播等进行证明或给出反例。
验证目标：三类核心问题
Jasper CDC/RDC 的验证目标可以归纳为三个层次。第一层是结构识别：工具自动提取设计中的时钟域、复位域、同步器（两级触发器、握手同步、异步 FIFO、脉冲同步器等），并建立跨域路径清单。第二层是风险判定：对每条跨域路径判断是否经过有效同步器、同步器是否满足亚稳态收敛要求、是否存在多比特汇聚、是否存在组合逻辑跨越。第三层是复位域验证：检查不同复位域之间的信号交互是否满足释放顺序约束，是否存在复位释放时的亚稳态传播或状态不一致。
在实际工程中，这三层目标对应三类典型缺陷：缺少同步器导致的亚稳态直接传播、同步器级数不足或结构错误导致的 MTBF 不达标、复位释放顺序错误导致的状态机误动作。Jasper CDC/RDC 对每一类都能给出结构化的判定结果，而不是简单的"通过/失败"。
典型工程流程与交付物
一个完整的 CDC/RDC 形式验证工程通常包含以下阶段。首先是环境准备：读入 RTL 或网表，定义时钟和复位，设置时钟频率、相位关系、复位极性等约束。其次是结构分析：运行工具的 CDC 结构提取，生成时钟域报告和跨域路径清单，人工确认同步器识别是否正确。第三是规则配置：根据设计规范设置同步器结构要求（如两级触发器、指定单元名）、复位域约束、准静态信号声明等。第四是形式化证明：对每条跨域路径运行证明，工具返回"已同步""未同步""需人工确认"三类结果。第五是反例分析与修复：对未同步路径查看反例波形，定位 RTL 问题并修复。最后是签核与报告：生成 CDC/RDC 验证报告，记录所有跨域路径的判定结果和修复状态。
与工程实践的衔接
需要特别强调的是，Jasper CDC/RDC 不是"一键通过"的工具。它的有效性高度依赖约束的准确性和同步器模型的正确配置。例如，如果时钟定义遗漏了一个生成时钟，工具可能把同域路径误判为跨域；如果同步器识别规则过于宽松，可能把非同步结构误认为同步器而漏报风险。因此，工程实践中通常需要先做一轮"结构审查"，由设计人员确认工具识别的时钟域和同步器是否与设计意图一致，再进入正式证明阶段。
此外，CDC/RDC 验证应尽早介入。在 RTL 编码阶段就运行结构分析，可以在设计早期发现跨域问题，避免问题遗留到网表阶段后修复成本急剧上升。对于大型 SoC，通常按模块划分验证范围，先做模块级 CDC 检查，再做系统级集成检查，最后在网表阶段做最终签核。
# 典型 Jasper CDC 工程脚本骨架（示意）
analyze -sv09 top.sv
elaborate -top top
clock -name clk_a -period 10
clock -name clk_b -period 7
reset -name rst_n -active low
cdc struct -check
cdc verify -all
report cdc -summary -file cdc_report.rpt理解工具定位、验证目标和工程流程，是后续所有 CDC/RDC 验证工作的基础。只有清楚"工具能做什么、不能做什么、需要人工确认什么"，才能在工程中真正发挥形式验证的穷尽性优势，把跨域风险控制在流片之前。