SVA - assert signal rise with its clock - difference between codes

Hi!
I verify a generic block.
It receives an array of signals and a corresponding array of clocks - each signal has its own clock.
The desire is to make sure that the signal rises at the rise of its clock (and not, for example, in the middle of the pulse).
I inherited code that does not refer to the generics of the block, and it checks all entries, even though they are sometimes incomplete:


event ev0,  ev1 , ev2 , ev3 .... ev31;

    generate
    if (EN_CLK_DOMAIN_CHECKER) begin 
    initial begin 
        fork
          forever @( posedge src_clk[0])  -> ev0;
          forever @( posedge src_clk[1])  -> ev1;
          forever @( posedge src_clk[2])  -> ev2;
          forever @( posedge src_clk[3])  -> ev3;
          ...
          forever @( posedge src_clk[31]) -> ev31;
        join_none
      end 
    end  
endgenerate
   
    
    `define DETECT_CLK_DOMAIN(INDEX)\
    function bit func``INDEX``();\
          if (ev``INDEX``.triggered) return 1;\
          else return 0;\
      endfunction\
      property detect``INDEX``;\
          @(posedge sig_in[``INDEX``])\
          (func``INDEX``());\
      endproperty : detect``INDEX``\
      DETECT``INDEX``  : assert property (detect``INDEX``) else $error("ERROR - WRONG CLOCK DOMAIN");\
          initial begin\
              $assertoff(0,generic_checker.DETECT``INDEX``);\
              wait (rstn === 1'b1);\
              #1ns;\
              if (EN_CLK_DOMAIN_CHECKER) begin\
                  $asserton(0,generic_checker.DETECT``INDEX``);\
              end\
          end
      
        `DETECT_CLK_DOMAIN(0)
        `DETECT_CLK_DOMAIN(1)
        `DETECT_CLK_DOMAIN(2)
        `DETECT_CLK_DOMAIN(3)
        ...
        `DETECT_CLK_DOMAIN(31)

This code works fine, but it throws up a lot of warnings during the elaboration.

I tried a different approach:


genvar idx;
generate
if (EN)
    for (idx =0; idx < NUM; idx++) begin
        always @(posedge sig_in[idx]) begin
                CLK_RISE_ASSERT: assert property (@(posedge sig_in[idx]) $rose(sig_in[idx]) |-> $rose(src_clk[idx]))
                else $error ("ERROR - WRONG CLOCK DOMAIN");
        end
    end
endgenerate

But the code didn’t work at all.
I tried to make adjustments to the first code and make it more generic - like this:



event clk_event_array[NUM];
    
    function automatic event new_clk_event();
        event e;
        return e;
    
    endfunction
    
    initial begin
        foreach (clk_event_array[i]) begin
            clk_event_array[i] = new_clk_event();
            $display ("clk_event_array[%0d]", i);
        end
    end 
    
    generate
    if (EN_CLK_DOMAIN_CHECKER) begin 
        initial begin
            for (int i = 0; i < NUM; i++) begin
                automatic int j = i;
                fork
                begin
                        forever @( posedge src_clk[j]) -> clk_event_array[j];
                end
                join_none          
            end
        end
    end 
    endgenerate

    function clk_trig_evaulate(int i);
        if (clk_event_array[i].triggered)
            return 1;
        else
            return 0;
    endfunction
    
    property detect(i, sig_in, rstn, clk_event_array);
        @(posedge sig_in) disable iff (!rstn) clk_trig_evaulate(i);
    endproperty : detect
  
    initial begin
        if (EN_CLK_DOMAIN_CHECKER) begin
            for (int i = 0; i < NUM; i++) begin : assert_loop
                DETECT : assert property (detect(i, sig_in[i], rstn, clk_event_array[i])) else $error("ERROR - WRONG CLOCK DOMAIN - INDEX [%0d]", i);
            end
        end
    end

And indeed it caught all the cases that the first code caught, but this time it dropped tests for me even in the case that the signal did arrive with the increase of its clock.

Can you tell me why the second code did not identify the violations at all, and why the third code identified cases as violations even though they were normal?
Can you suggest how to make the first code generic?

Many thanks in advance

In reply to OE93:

It would help to separate this into two separate issues. The first is the property you want to check between src_clk and sig_in. Then we can deal with the arrayed nature of the checks.

Can you create a self contained example that shows the first issue and how the two signals are generated?

In reply to dave_59:

Hi Dave
Thanks for your response.
I hope I understood your request-

Of course, due to information security I cannot provide detailed information, but I can explain the motivation:

My concern in the block is missing a signal as a result of crossing domains. Suppose I have a low-frequency system clock, and a signal whose nature is that it rises for only one clock cycle. If the clock in the domain of that signal is faster than the system clock of my block, I may miss the arrival of the signal. Therefore the signal will enter the synchronizer, where it will be sampled and transferred to the domain of my block.
My desire in the code I wrote above is to make sure that the signal is synchronous, and therefore depends on the clock provided to me, meaning that the rise of the signal will always occur at the rise of its clock.

Thanks again! It is not obvious at all that you dedicate your time to helping and mentoring young engineers.

In reply to OE93:

Your second code never works because $rose(sig_in[idx]) is always 0. You are using the same signal as the clock event, and its sampled value is always 0 before it rises. The function call in the first code is a convoluted way of avoiding using sampled values.

Without know exactly how your clocks are modelled and how the signals get assigned, or what is particular about the tests that produced false violations, it is difficult to know what might be wrong. I suggest you might try making your code generic in stages rather than replace the macro all at once. For example the event generation can be replace with this

ev[NUM]
for(genvar i=0;i<NUM;i++) 
  always @( posedge src_clk[i])  -> ev[i];

Then replace the function, then the property.

Finally replace the assertion. Do not place it inside an initial block.

if (EN_CLK_DOMAIN_CHECKER) begin
  for (genvar i = 0; i < NUM; i++) begin : assert_loop
         DETECT : assert property (detect(i, sig_in[i], rstn, clk_event_array[i])) else $error("ERROR - WRONG CLOCK DOMAIN - INDEX [%0d]", i);
     end
end

In reply to dave_59:

Many thanks.
I don’t know what solved the problem, but I made some adjustments according to your comments, and now it’s generic and works :)