Calculate and compare multiple clock frequencies if the condition met!

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.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog