SVA - use different clocks in the property from the sample clock

SystemVerilog
1

I need to write a property to check the divisor of a fast clock. I’ve tried the following options:

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

However, I encountered compilation errors with both options:

  1. (clk_en == 1) |-> $stable(destination_clk) ##(divisor/2) @(posedge pll_clk);
xmvlog: *E,ILLPRI: illegal expression primary [4.2(IEEE)].
  1. (clk_en == 1) |-> $stable(destination_clk) @(posedge pll_clk) ##(divisor/2);
xmvlog: *E,SVAPNS: Property declaration must end with "endproperty".

How can I use a different clock for the stable cycles? I know there are other ways to check that the divided clock generates the correct frequency, such as using $period, but I want to verify it by counting the fast clock cycles.

2 
$stable(destination_clk) ##(divisor/2) @(posedge pll_clk);
does not make sense. 
  @(posedge pll_clk) expression_or_signal_or_a_sequence_must_be_here.
You have nothing atger the  @(posedge pll_clk.

I suggest that you use support logic with immediate assertions. 
for counts, you could use a task with 2 forked threads and count then number of clocks.  something like (untested)
task automatic t_clk; 
    int v1, v2; 
    bit done1, done2;
    fork 
         begin 
           repeat(20) @(posedge clk1) v1++; 
            done1=1;
         end 
         begin 
             repeat(20) @(posedge clk2) v1++; 
            done2=1;
            end   
     join_none
     wait(done1 && done2);
     am12: assert(v1/v2 == 2);  // v1 is 2x v2
  endtask

initial @(posedge clk) begin
       fork t_clk(); 
        join_none; 
end
3

That’s not what I asked.
I asked how can I make the stable works by the pll_clk, instead of the destination clock.
I just want to verify that the destination_clk is stable for N pll_clk cycles

4 
property clk_frequency_P(logic pll_clk, logic destination_clk, logic clk_en, logic reset, int divisor);
   bit v;
  @(posedge destination_clk) disable iff (~reset)
  divisor==2 && (clk_en == 1) |=> 
      @(pll_clk) ((1, v=destination_clk) ##1 destination_clk==v)[*2];
endproperty
property clk_frequency_P(logic pll_clk, logic destination_clk, logic clk_en, logic reset, int divisor);
   bit v;
  @(posedge destination_clk) disable iff (~reset)
  divisor==4 && (clk_en == 1) |=> 
      @(pll_clk) ((1, v=destination_clk) ##1 destination_clk==v)[*4];
endproperty
// You can use the generate for more divisor values. 
// Untested, but I see it this way: 
ppl_clk        1 0 1 0 1 0 1 0 
dest_clk       0 1 1 0 0 1 1 0 0 // divisor==2 
dest_clk       0 1 1 1 1 0 0 0 0 1 1 1 1 // divisor==4