Calculate and compare multiple clock frequencies if the condition met!

[mahdi.moradmand]

In the following code I am trying use the assertion in the way that when the signal_a == 1 and signal_b == 0, within 6 clock cycle the frequency of clka, clkb and clkc are calculate and compare with each other! Any idea what did I miss? PS. The code compile and run but never calculate frequency/period and shows always as 0. The clka, clkb and clkc are changing over simulation!

module assertions_module (
    input logic signal_a,
    input logic signal_b,
    input logic clkc,
    input logic clka,
    input logic clkb
);

real clka_freq;
real clkb_freq;
real clkc_freq;

task automatic freq_meter(input logic clk_in, ref real clk_out_freq);
    time    start_time, end_time;
    time    period;
    real    clk_freq;

    @(posedge clk_in);
    start_time = $time;
    @(posedge clk_in);
    end_time = $time;

    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_out_freq = clk_freq/1e6;

endtask : freq_meter

task automatic all_clk_freq_meter();
   
    @(posedge clka)
    freq_meter(clka, clka_freq);

    @(posedge clkb)
    freq_meter(clkb, clkb_freq);

    @(posedge clkc)
    freq_meter(clkc, clkc_freq);
    
endtask: all_clk_freq_meter

    always_comb
    begin
        clka_test_assert: assert property(
            @(posedge clka) 
            signal_a && !signal_b |-> ##[0:6] (1, all_clk_freq_meter()) ##1 (clka_freq != clkc_freq));

        clkb_test_assert: assert property(
            @(posedge clkb) 
            signal_a && !signal_b |-> ##[0:6] (1, all_clk_freq_meter()) ##1 (clkb_freq == clkc_freq));

    end
endmodule

[ben2]

In reply to MahD:
You have 3 different frequencies to compute and compare.
Thus, I can see why you used tasks to compute those frequencies.
Your code below has several errors, though it compiles OK:

[list=1]
[*] The task all_clk_freq_meter() triggers 3 sequential calls to freq_meter(), rather
than concurrently; I would use afork join_none

EDA Playground

task automatic all_clk_freq_meter();
 fork
    @(posedge clka) freq_meter(clka, clka_freq); 
    @(posedge clkb) freq_meter(clkb, clkb_freq); 
    @(posedge clkc) freq_meter(clkc, clkc_freq);
 join_none 
endtask: all_clk_freq_meter

[*] Since clocks have different frequencies, and the clk’X’_freq change at different times,
with many attempted, I would consider a ##6 in

signal_a && !signal_b |-> ##[0:6] (1, all_clk_freq_meter()) ##1 (clka_freq != clkc_freq));

I took a variation to your code. Check if this works better for you.
Basically, I run the test in 6 cycles once the antecedent is true, but also with less overlaps.

EDA Playground

/* In the following code I am trying use the assertion in the way that when the
signal_a == 1 and signal_b == 0, within 6 clock cycle 
the frequency of clka, clkb and clkc are calculates and compare with each other!  */
//Any idea what did I miss? PS. The code compile and run but never calculate
//frequency/period and shows always as 0. The clka, clkb and clkc are changing over simulation!

module assertions_module (
    input logic signal_a,
    input logic signal_b,
    input logic clkc,
    input logic clka,
    input logic clkb
  );

  real clka_freq;
  real clkb_freq;
  real clkc_freq;
  bit  ac_match, bc_match, active=1;

  task automatic freq_meter(input logic clk_in, ref real clk_out_freq);
    realtime    start_time, end_time;
    realtime    period;
    real    clk_freq;

    //@(posedge clk_in);
    start_time = $realtime;
    @(posedge clk_in);
    end_time = $realtime;

    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_out_freq = clk_freq/1e6;
  endtask  :  freq_meter

  task automatic all_clk_freq_meter();
      active <= 1; 
      repeat(6) begin
        fork : start
           @(posedge clka) freq_meter(clka, clka_freq);

           @(posedge clkb) freq_meter(clkb, clkb_freq);

           @(posedge clkc) freq_meter(clkc, clkc_freq);
        join
        @(posedge clka) am_ac:  if(clka_freq != clkc_freq) ac_match=1;
                                if(clkb_freq == clkc_freq) bc_match=1;
      end
    am_ac_bc_match: assert(ac_match==1 && bc_match==1);
      ac_match=0; bc_match=0; active=0;
    endtask  : all_clk_freq_meter
    
    always @(posedge clka) // Fire the tasks to compute the frequencies 
      clk_test_assert: assert property(
              !active && signal_a && !signal_b |-> (1, all_clk_freq_meter()));
endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

Cohen_Links_to_papers_books.pdf

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

Ben Cohen on LinkedIn: Road map to start with verification: SV, SVA , UVM and TB

[mahdi.moradmand]

In reply to ben@SystemVerilog.us:

Thank you so much @Ben for your time.
A question I have;
In the line @(posedge clka) am_ac: if(clka_freq != clkc_freq) ac_match=1;
if(clkb_freq == clkc_freq) bc_match=1;
we just consider the clka as well as here
always @(posedge clka) // Fire the tasks to compute the frequencies
clk_test_assert: assert property(
!active && signal_a && !signal_b |-> (1, all_clk_freq_meter()));

Should I do the same for clkb, or either one should fulfil my requirements!?
I believe you tried to combine 2 clka_test_assert and clkb_test_assert in the 1 assertion, if so, what should I do if 2 assertion conditions is different like:

    always_comb
    begin
        clka_test_assert: assert property(
            @(posedge clka) 
            signal_a && !signal_b |-> ##[0:6] (1, all_clk_freq_meter()) ##1 (clka_freq != clkc_freq));
 
        clkb_test_assert: assert property(
            @(posedge clkb) 
            !signal_a || (!signal_b && signal_c) |-> ##[0:6] (1, all_clk_freq_meter()) ##1 (clkb_freq == clkc_freq));
 
    end

I should add that the problem that the clocks frequencies are equal to zero.
I tried to put several displays in the task, but it seems that it is not called at all.

[ben2]

In reply to MahD:
Not knowing your requirements, I had to make some assumptions, and you know what they say about
assumptions, they make an “ASS out of U and Me” :)
[Ben] In my alternate solution, I made several assumptions. All the tests and assertions are done in the task all_clk_freq_meter() with the immediate assertion in the task, and with that task triggered once and lasting 6 cycles

am_ac_bc_match: assert(ac_match==1 && bc_match==1);
      ac_match=0; bc_match=0; active=0;
always @(posedge clka) // Fire the tasks to compute the frequencies 
      clk_test_assert: assert property(
              !active && signal_a && !signal_b |-> (1, all_clk_freq_meter()));

Here, I assumed that if (signal_a && !signal_b) then I check for the frequency relationships in within a window of 7 cycles, and I do check again until that check is completed.
That !active set and reset is done from within the task.

A question I have;
In the line @(posedge clka) if(clka_freq != clkc_freq) ac_match=1;// am_ac: label not needed
if(clkb_freq == clkc_freq) bc_match=1;
we just consider the clka as well as here
always @(posedge clka) // Fire the tasks to compute the frequencies
clk_test_assert: assert property(
!active && signal_a && !signal_b |-> (1, all_clk_freq_meter()));

[Ben] I assumed all the relationship tests were done within the task.
am I missing something here?

Should I do the same for clkb, or either one should fulfil my requirements!?
I believe you tried to combine 2 clka_test_assert and clkb_test_assert in the 1 assertion, if so, what should I do if 2 assertion conditions is different like:

always_comb
begin
clka_test_assert: assert property(
@(posedge clka) 
signal_a && !signal_b |-> ) ##1 (clka_freq != clkc_freq));
clkb_test_assert: assert property(
@(posedge clkb) 
!signal_a || (!signal_b && signal_c) |-> ##[0:6] (1, all_clk_freq_meter()) ##1 (clkb_freq == clkc_freq));
end

1. You do NOT need the lways_comb
2. The ##[0:6] (1, all_clk_freq_meter() is a red flag for me because from within the task that is called in separate cycles you are modifying module variables used in the assertion. In general, it is a red flag that really needs to be analyzed because every call to the automatic task is doing its own thing on the module variables to be later on used in the assertion. It’s a bit like building a sand castle (the variables) and having people (the automatic task calls) trampling all over it. This is why I used the alternate approach with the active lock-out bit.
3. I’ll let you analyze your design and requirements and see which assertions you need. I would also consider using $rose( !signal_a || (!signal_b && signal_c)) to minimize the trampling of the module variables by the multitude of the task calls that each makes a change to those variables.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

Cohen_Links_to_papers_books.pdf

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

Ben Cohen on LinkedIn: Road map to start with verification: SV, SVA , UVM and TB

[ben2]

In reply to ben@SystemVerilog.us:

I would put the module variables needed for the assertions within the main task.

[mahdi.moradmand]

In reply to ben@SystemVerilog.us:

Hey Ben,

I tried to simplified my question to get an idea about the process.
My main requirement is as follow:

module assertions_module (
    input logic signal_1,
    input logic signal_2,
    input logic signal_3,
    input logic signal_4,
    input logic signal_5,
    input logic clka,
    input logic clkb,
    input logic clkc
);
 
real clka_freq;
real clkb_freq;
real clkc_freq;

logic clka_t;
logic clkb_t;
logic clkc_t;

task automatic freq_meter(ref logic clk_in, ref real clk_freq);
    time    start_time, end_time;
    time    period;
 
    @(posedge clk_in);
    start_time = $time;
    @(posedge clk_in);
    end_time = $time;
 
    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_freq = clk_freq/1e6;
 
endtask : freq_meter
// I am using following 3 always because when use ref for input of freq_meter it says Variable input ports cannot be driven
    always @(posedge clka)
        clka_t <= clka;

    always @(posedge clkb)
        clkb_t <= clkb;

    always @(posedge clkc)
        clkc_t <= clkc;


    task automatic start_measurement();
        active <= 1;
        repeat(6) begin
            fork
                @(posedge clka_t)
                        freq_meter(clka_t, clka_freq);
                @(posedge clkb_t) 
                        freq_meter(clkb_t, clkb_freq);
                @(posedge clkc_t) 
                        freq_meter(clkc_t, clkc_freq);
            join
            @(posedge clka_t)
                if(clka_freq == clkc_freq) 
                    clka_match = 1;

            @(posedge clkb_t)
                if(clkb_freq == clkc_freq) 
                    clkb_match = 1;
        end

        clka_match_assert: assert(clka_match == 1);
        clkb_match_assert: assert(clkb_match == 1);

        clka_match = 0; 
        clkb_match = 0; 
        active = 0;
    endtask : start_measurement

    always @(posedge clka_t)
        clka_assert1: assert property(
        !active && signal_1 && !signal_2 && signal_3 |-> (1, start_measurement()));

    always @(posedge clkb_t)
        clkb_assert1: assert property(
        !active && signal_4 && !signal_2 && signal_5 |-> (1, start_measurement()));

    always @(posedge clka_t)
        clka_assert2: assert property(
        !active && !signal_1 && signal_2 |-> (1, start_measurement()));

    always @(posedge clkb_t)
        clkb_assert2: assert property(
        !active && !signal_4 && signal_2 |-> (1, start_measurement()));

this |-> (1, start_measurement()) means the task start_measurement() always call regardless of left side of |-> ?

In either case the condition never met and I don’t see the assertion/start_measurement/freq_meter call at all.

[ben2]

In reply to MahD:

/* this |-> (1, start_measurement()) means the task start_measurement()
always call regardless of left side of |-> ?
[Ben] If the antecedent is true the consequent is executed.
In either case the condition never met and I don’t see
the assertion/start_measurement/freq_meter call at all.
[Ben] Code below is untested, try it */

You do not need the ref for the clkX as you never you never assign values to them.
I modified the code so that is a pass occurs, the repeat 6 is broken,
thus giving you the 1:6 range that you wanted.

EDA Playground

module assertions_module (
    input logic signal_1,
    input logic signal_2,
    input logic signal_3,
    input logic signal_4,
    input logic signal_5,
    input logic clka,
    input logic clkb,
    input logic clkc
  );
  bit active;
  
  // Compute the clock frequency 
  task automatic freq_meter(logic clk_in, ref real clk_freq);
    time    start_time, end_time;
    time    period;
    @(posedge clk_in) start_time = $time;
    @(posedge clk_in) end_time = $time;
    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_freq = clk_freq/1e6;
  endtask : freq_meter

  // Do the measument 6 times, but break if a pass within the 6 cycles 
  task automatic start_measurement();
    real clka_freq, clkb_freq, clkc_freq;
    bit passa, passb; 
    active <= 1;
    repeat(6) begin : try6
      fork
        @(posedge clka) freq_meter(clka, clka_freq);
        @(posedge clkb) freq_meter(clkb, clkb_freq);
        @(posedge clkc) freq_meter(clkc, clkc_freq);
      join
      @(posedge clka);
      clka_match_assert: assert(clka_freq == clkc_freq) passa=1;
      clkb_match_assert: assert(clkb_freq == clkc_freq) passb=1;
      if(passa && passb) break; 
    end
    active <= 0;
  endtask  : start_measurement

  clka_assert1: assert property(@(posedge clka)
        !active && signal_1 && !signal_2 && signal_3 |-> (1, start_measurement()));

  clkb_assert1: assert property( @(posedge clkb)
        !active && signal_4 && !signal_2 && signal_5 |-> (1, start_measurement()));

  clka_assert2: assert property(@(posedge clka)
        !active && !signal_1 && signal_2 |-> (1, start_measurement()));  

  clkb_assert2: assert property(@(posedge clkb)
        !active && !signal_4 && signal_2 |-> (1, start_measurement()));

endmodule 

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

Cohen_Links_to_papers_books.pdf

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

Ben Cohen on LinkedIn: Road map to start with verification: SV, SVA , UVM and TB

[ben2]

In reply to MahD:

Show you complete TB.

[mahdi.moradmand]

In reply to ben@SystemVerilog.us:

module tb;
 timeunit 1ns;
 timeprecision 100ps;
        
 logic clkc = 0;
 logic clka = 0;
 logic clkb = 0;
        
 always #5  clkc = ~clkc;
 always #10 clka = ~clka;
 always #20 clkb = ~clkb;
        
 initial #5000 $finish;

 initial begin 
        #150 signal_1 = 0; signal_2 = 1; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #200 signal_1 = 0; signal_2 = 0; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #250 signal_1 = 1; signal_2 = 1; signal_3 = 0; signal_4 = 1; signal_5 = 1;
        #300 signal_1 = 1; signal_2 = 1; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #350 signal_1 = 1; signal_2 = 0; signal_3 = 1; signal_4 = 0; signal_5 = 1;
        #400 signal_1 = 0; signal_2 = 1; signal_3 = 0; signal_4 = 0; signal_5 = 1;
        #450 signal_1 = 0; signal_2 = 1; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #500 signal_1 = 0; signal_2 = 0; signal_3 = 0; signal_4 = 1; signal_5 = 1;
        $stop ; 
    end 
            
 assertions_module assertions_module_inst(
     .signal_1(signal_1),
     .signal_2(signal_2),
     .signal_3(signal_3),
     .signal_4(signal_4),
     .signal_5(signal_5),
     .clka(clka),
     .clkb(clkb),
     .clkc(clkc)
 );

endmodule

[ben2]

In reply to MahD:
The problem was that the task waited for the @(posedge clk_in) start_time = $time;
I replicated the procedure and used the input clocks directly.
Now it works.

EDA Playground

module assertions_module (
    input logic signal_1,
    input logic signal_2,
    input logic signal_3,
    input logic signal_4,
    input logic signal_5,
    input logic clka,
    input logic clkb,
    input logic clkc
  );
  bit active;
  bit debug; 
  
  // Compute the clock frequency 
  task automatic freq_metera(ref real clk_freq);
    time    start_time, end_time;
    time    period;
    @(posedge clka) start_time = $time;
    @(posedge clka) end_time = $time;
    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_freq = clk_freq/1e6;
  endtask : freq_metera
  
   task automatic freq_meterb(ref real clk_freq);
    time    start_time, end_time;
    time    period;
     @(posedge clkb) start_time = $time;
     @(posedge clkb) end_time = $time;
    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_freq = clk_freq/1e6;
  endtask : freq_meterb
  
   task automatic freq_meterc(ref real clk_freq);
    time    start_time, end_time;
    time    period;
     @(posedge clkc) start_time = $time;
     @(posedge clkc) end_time = $time;
    period = end_time - start_time;
    clk_freq = real'(1e12/period);
    clk_freq = clk_freq/1e6;
  endtask : freq_meterc

  // Do the measument 6 times, but break if a pass within the 6 cycles 
  task automatic start_measurement();
    real clka_freq, clkb_freq, clkc_freq;
    bit passa, passb; 
    active = 1; //#2 active=0; // debug
    debug =1;
    repeat(6) begin : try6
      fork
        @(posedge clka) freq_metera(clka_freq);
        @(posedge clkb) freq_meterb(clkb_freq);
        @(posedge clkc) freq_meterc(clkc_freq);
      join
      @(posedge clka);
      clka_match_assert: assert(clka_freq == clkc_freq) passa=1;
      clkb_match_assert: assert(clkb_freq == clkc_freq) passb=1;
      debug =1; #3 debug=0;
      if(passa && passb) break; 
    end
    active <= 0;
  endtask  : start_measurement

  clka_assert1: assert property(@(posedge clka)
        !active && signal_1 && !signal_2 && signal_3 |-> (1, start_measurement()));

  clkb_assert1: assert property( @(posedge clkb)
        !active && signal_4 && !signal_2 && signal_5 |-> (1, start_measurement()));

  clka_assert2: assert property(@(posedge clka)
        !active && !signal_1 && signal_2 |-> (1, start_measurement()));  

  clkb_assert2: assert property(@(posedge clkb)
        !active && !signal_4 && signal_2 |-> (1, start_measurement()));

endmodule 

module tb;
 timeunit 1ns;
 timeprecision 100ps;
 
 logic clkc = 0;
 logic clka = 0;
 logic clkb = 0;
 logic signal_1, signal_2, signal_3, signal_4, signal_5;
 always #5  clkc = ~clkc;
 always #10 clka = ~clka;
 always #20 clkb = ~clkb;
 
 initial #5000 $finish;
 
 initial begin 
    $dumpfile("dump.vcd"); $dumpvars;
        #150 signal_1 = 0; signal_2 = 1; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #200 signal_1 = 0; signal_2 = 0; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #250 signal_1 = 1; signal_2 = 1; signal_3 = 0; signal_4 = 1; signal_5 = 1;
        #300 signal_1 = 1; signal_2 = 1; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #350 signal_1 = 1; signal_2 = 0; signal_3 = 1; signal_4 = 0; signal_5 = 1;
        #400 signal_1 = 0; signal_2 = 1; signal_3 = 0; signal_4 = 0; signal_5 = 1;
        #450 signal_1 = 0; signal_2 = 1; signal_3 = 1; signal_4 = 1; signal_5 = 1;
        #500 signal_1 = 0; signal_2 = 0; signal_3 = 0; signal_4 = 1; signal_5 = 1;
        $stop ; 
    end 
 
 assertions_module assertions_module_inst(
     .signal_1(signal_1),
     .signal_2(signal_2),
     .signal_3(signal_3),
     .signal_4(signal_4),
     .signal_5(signal_5),
     .clka(clka),
     .clkb(clkb),
     .clkc(clkc)
 );
 
endmodule

[mahdi.moradmand]

In reply to ben@SystemVerilog.us:

Thanks Ben.
Really helpful.
I knew there was a reason for that ref logic clk_in, but not know why facing “Variable input ports cannot be driven”