如何在SystemVerilog属性中跨时钟验证分频时钟稳定性？

我需要编写一个SystemVerilog的property来验证快时钟的分频功能，尝试了以下两种实现方式：

property clk_frequency_P(logic pll_clk, logic destination_clk, logic clk_en, logic reset, int divisor);
  @(posedge destination_clk) disable iff (~reset)
  (clk_en == 1) |-> $stable(destination_clk) ##(divisor/2) @(posedge pll_clk);
endproperty

property clk_frequency_P(logic pll_clk, logic destination_clk, logic clk_en, logic reset, int divisor);
  @(posedge destination_clk) disable iff (~reset)
  (clk_en == 1) |-> $stable(destination_clk) @(posedge pll_clk) ##(divisor/2);
endproperty

但两种写法均出现编译错误：

第一种写法报错 #

报错行：

(clk_en == 1) |-> $stable(destination_clk) ##(divisor/2) @(posedge pll_clk);

错误信息：

xmvlog: *E,ILLPRI: illegal expression primary [4.2(IEEE)].

第二种写法报错 #

报错行：

(clk_en == 1) |-> $stable(destination_clk) @(posedge pll_clk) ##(divisor/2);

错误信息：

xmvlog: *E,SVAPNS: Property declaration must end with "endproperty".

我希望通过计数快时钟周期来完成验证，而非使用$period等方法，该如何为稳定性检查的周期使用不同的时钟？

错误原因分析 #

1. 第一种写法：时序操作顺序违反SystemVerilog断言语法。##延迟操作符必须跟随在时钟事件限定的序列之后，不能在延迟后直接指定时钟事件，这种写法属于非法语法结构。
2. 第二种写法：时钟事件@(posedge pll_clk)的位置错误，它必须作为时序序列的前缀来限定后续的操作，不能直接跟在$stable表达式之后，导致编译器无法正确解析property的结构，误认为代码未完成。

正确实现方式 #

要在不同时钟域下完成稳定性检查，需要明确切换时钟并正确组织时序序列。以下是两种可行的写法：

写法1：直接在property中切换时钟 #

property clk_frequency_P(logic pll_clk, logic destination_clk, logic clk_en, logic reset, int divisor);
  @(posedge destination_clk) disable iff (~reset)
  (clk_en == 1) |-> (@(posedge pll_clk) ##(divisor/2 - 1) $stable(destination_clk));
endproperty

• 逻辑说明：当destination_clk上升沿且clk_en有效时，切换到快时钟pll_clk的上升沿，检查后续divisor/2 - 1个快时钟周期内，destination_clk保持稳定（对应分频后时钟的半周期时长）。
• 注：##(divisor/2 - 1)是因为@(posedge pll_clk)已经是第一个快时钟沿，后续需要再等待divisor/2 - 1个周期来凑足divisor/2个快时钟周期的时长。

写法2：封装跨时钟检查序列 #

将跨时钟的稳定检查封装为独立序列，提高代码可读性：

// 封装跨时钟稳定检查序列
sequence stable_on_fast_clk(pll_clk, sig, cycle_cnt);
  @(posedge pll_clk) repeat(cycle_cnt) $stable(sig);
endsequence

// 分频验证property
property clk_frequency_P(logic pll_clk, logic destination_clk, logic clk_en, logic reset, int divisor);
  @(posedge destination_clk) disable iff (~reset)
  (clk_en == 1) |-> stable_on_fast_clk(pll_clk, destination_clk, divisor/2);
endproperty

• 逻辑说明：stable_on_fast_clk序列用于在快时钟域下检查信号连续cycle_cnt个周期保持稳定；在分频property中，当destination_clk上升沿触发时，调用该序列检查分频后时钟的半周期稳定性。

内容的提问来源于stack exchange，提问作者Sarti