2. 时钟域与复位域基础建模

在Jasper形式验证中，时钟与复位不是“仿真环境里的激励”，而是断言、属性、覆盖点赖以成立的时序基准。如果时钟域和复位域建模不准确，后续的CDC/RDC检查、协议断言、覆盖收敛都会建立在错误的前提上。本节围绕五个核心问题展开：时钟如何定义、时钟域如何划分、复位如何建模、跨域关系如何表达、边沿与电平语义如何区分。

一、时钟定义：从波形到Jasper可识别的时钟对象

Jasper并不自动“猜测”时钟。它需要你明确告诉工具：哪个信号是时钟、周期是多少、占空比如何、相位关系怎样。最基础的方式是使用create_clock命令：

create_clock -name clk_core -period 10 -waveform {0 5} [get_ports clk_core]
create_clock -name clk_io   -period 20 -waveform {0 10} [get_ports clk_io]

这里-period 10表示周期为10个时间单位，-waveform {0 5}表示上升沿在0、下降沿在5。若时钟来自PLL或分频器，通常还需要create_generated_clock描述其与源时钟的相位/分频关系。Jasper中时钟定义的关键点在于：时钟是断言采样的时间坐标。同一个信号在不同时钟下采样，会得到完全不同的时序行为。

实际工程中，建议先建立一张“时钟清单”，明确每个时钟的名称、来源、周期、相位、是否生成时钟、是否用于CDC检查。例如：

时钟名	来源	周期	相位	用途
clk_core	PLL输出	10	0	核心逻辑采样
clk_io	外部晶振	20	0	IO接口采样
clk_dsp	clk_core分频	20	5	DSP数据路径

这张表不是形式化输入，而是建模前的“设计意图对齐”。如果连设计者自己都说不清两个时钟是否同源、是否有固定相位，后续CDC断言就无法判断“同步”还是“异步”。

二、时钟域交叉：不是所有跨时钟都叫CDC

时钟域交叉（CDC）的本质是：一个信号从时钟A的采样域进入时钟B的采样域，且两个时钟之间没有固定的相位/频率关系。Jasper中通常用cdc相关命令或属性来标记跨域路径。但要注意：如果两个时钟同源且相位固定，例如clk_core和clk_dsp，它们之间的路径不一定需要CDC同步器，但需要做时序约束和相位关系检查。

CDC建模的核心是识别“跨域信号”和“同步器结构”。常见同步器包括两级触发器、握手同步、异步FIFO、脉冲同步器。Jasper中可以通过create_cdc或set_cdc类命令指定源时钟、目标时钟和同步器类型。例如：

create_cdc -from clk_core -to clk_io -name cdc_core2io
set_cdc_synchronizer -type two_flop -cells {u_sync/ff1 u_sync/ff2}

这里的关键不是命令本身，而是同步器结构必须与RTL一致。如果RTL里是三级触发器，而你在Jasper里只声明两级，工具会误判同步深度，导致CDC断言过松或过紧。

三、复位域交叉：RDC与CDC的差异

复位域交叉（RDC）关注的是：一个复位信号从一个复位域进入另一个复位域时，是否会导致目标域出现亚稳态或不确定状态。与CDC不同，RDC的“跨域对象”是复位信号，而不是数据信号。典型场景是：全局复位rst_n经过同步器后驱动某个时钟域，但同步器本身又依赖另一个复位域。

Jasper中RDC建模通常需要：定义复位源、复位同步器、复位释放顺序。例如：

create_reset -name rst_core -active_low [get_ports rst_core_n]
create_reset -name rst_io   -active_low [get_ports rst_io_n]
set_reset_synchronizer -reset rst_io -cells {u_rst_sync/ff1 u_rst_sync/ff2}

RDC检查的重点是“复位释放时刻”是否满足目标时钟的建立/保持要求。如果复位释放与目标时钟边沿太近，触发器可能进入亚稳态。Jasper会通过断言检查复位释放是否被目标时钟同步。

四、同步复位与异步复位：语义差异决定断言写法

同步复位在时钟边沿生效，异步复位则立即生效。在Jasper中，这两种复位的断言写法完全不同。同步复位可以写成：

property sync_rst_check;
  @(posedge clk) rst_sync |=> !data_valid;
endproperty

异步复位则需要使用disable iff或async语义：

property async_rst_check;
  @(posedge clk) disable iff (!rst_async_n) !data_valid;
endproperty

注意：disable iff表示“当复位有效时，整个属性不检查”，而不是“复位有效时输出为0”。如果要检查异步复位立即生效，需要单独写复位路径断言。很多初学者会把异步复位写成同步复位，导致复位释放时的亚稳态风险被漏检。

五、边沿敏感与电平敏感：Jasper中的采样语义

边沿敏感指信号在时钟边沿被采样，电平敏感指信号在电平有效期间持续影响逻辑。Jasper中，@(posedge clk)表示边沿采样，而@(clk)或组合逻辑属性则表示电平敏感。例如，锁存器是电平敏感的，其断言不能简单用posedge描述：

property latch_check;
  @(clk) enable |-> (q == d);
endproperty

这里@(clk)表示在clk为高电平期间持续检查，而不是只在上升沿检查。如果误写成@(posedge clk)，就会漏掉enable为高但clk尚未跳变时的透明行为。

六、建模检查清单与常见陷阱

完成时钟与复位建模后，建议用以下清单快速复查：

• 每个时钟是否都有明确的create_clock或create_generated_clock？
• 同源时钟之间的相位关系是否已声明？
• CDC路径是否都指定了同步器类型和深度？
• RDC路径是否检查了复位释放时刻？
• 异步复位是否使用了disable iff或等效语义？
• 电平敏感逻辑是否误用了posedge？

时钟与复位建模是Jasper形式验证的“地基”。地基不稳，后面的断言、覆盖、CDC/RDC检查都会失去意义。建议在项目初期就建立时钟/复位清单，并在每次RTL变更后同步更新Jasper约束，确保形式验证环境与设计意图始终一致。