Scoreboarding assertion for clock crossing signals

I need to write an assertion for a set of signals that cross clock boundary, I need to check that the signal is passed from one module to the other within a certain clock cycles of destination clock. I can add the assertion at top module which instances the two sub-modules. Assertion basically have to behave like signal integrity checker so that no transitions are dropped. There is a tolerable amount of delay from source to dest. How can i write these assertions ? Does the below work ?

assert property (@(posedge dst_clock) || @(source_data)) source_data |-> ##[3:5] dest_data );

In reply to amitr5:
I would use as the clocking event for the assertion the source clock (src_clock), and then for the wait number of ccles the dest clok. Thus


// More comments below, as this may not be what you want. 
ap_src2dest: assert property (@(posedge src_clock) source_data |->
                          @(dest_clock) ##[3:5] dest_data );
 

A few comments:

  1. Am puzzled by the name of the signals “source_data” “dest_data”. Is this an integer? or is it a sync single bit signal. For the above to work, it has to be an expression the way the assertion is written If it’s a data bit, you want to check that the signal crosses the clock boundary, regardless of the value of what you call “data”. In theat case, I would prefer:

ap_src2dest_to1: assert property ( @(posedge src_clock) $rose(src_data_bit)|->
@(dest_clock) ##[3:5] $rose(dest_data_bit));
ap_src2dest_to0: assert property (@(posedge src_clock) $fell(src_data_bit)|->
@(dest_clock) ##[3:5] $fell(dest_data_bit));

I
2. The folloing is illegal as a leading clocking event:
(@(posedge dst_clock) || @(source_data)) , (@(posedge dst_clock) or @(source_data))

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for your reply, I was trying to write assertions for single bit signals crossing cdc. Your second solution suits my application, I havent tried it yet though.

In the below assertion that you suggested,

ap_src2dest_to1: assert property ( @(posedge src_clock) $rose(src_data_bit)|->
@(dest_clock) ##[3:5] $rose(dest_data_bit));
ap_src2dest_to0: assert property (@(posedge src_clock) $fell(src_data_bit)|->
@(dest_clock) ##[3:5] $fell(dest_data_bit));

Should’nt it be @(posedge dest_clock) instead of @(dest_clock) ?
Curious if there is any specific reason why it should be @(dest_clock)

Also I had tried this meanwhile, but doesnt seem to work. Any clue on what could be wrong with this, this kind of combines the two assertions of rising and falling change into one assertion where we save the value at source domain and then check later at dest domain.

property CDC_prop;
logic v_temp;
@(posedge Clk_A) ($changed(A_in), v_temp = A_in) |=>
@(posedge Clk_B) 1’b1 ##[2:3]
($changed(B_out) && (B_out === v_temp));
endproperty:CDC_prop

In reply to amitr5:

On “Should’nt it be @(posedge dest_clock) instead of @(dest_clock) ?”
You are correct, my mistake. On

 property CDC_prop;
logic v_temp;
@(posedge Clk_A) ($changed(A_in), v_temp = A_in) |=>
@(posedge Clk_B) 1'b1 ##[2:3]
($changed(B_out) && (B_out === v_temp));
endproperty:CDC_prop
//looks OK to me.  
// Comment: from a requirement point of view, is the 
// ($changed(B_out) necessary? 

Ben systemverilog.us

In reply to ben@SystemVerilog.us:

I think it works without $changed(B_out) too. I didnt had such requirement.

If i use $changed(B_out) I need to be more careful with the range i provide in the second part.
If i’ve given ##[3:6] as below and if the signal propagated in less than 3 cycles it will fail as it expects to change within the window. Correct ?
I only had to check if the signal propagates, window was not necessary.

property CDC_prop;
logic v_temp;
@(posedge Clk_A) ($changed(A_in), v_temp = A_in) |=>
@(posedge Clk_B) 1’b1 ##[3:6]
($changed(B_out) && (B_out === v_temp));
endproperty:CDC_prop

In reply to amitr5:

In reply to ben@SystemVerilog.us:
I think it works without $changed(B_out) too. I didnt had such requirement.
If i use $changed(B_out) I need to be more careful with the range i provide in the second part.

yes, if change occurs in 1 or 2 cycles, assertion will fail, unless there is another correct change in the range.

If i’ve given ##[3:6] as below and if the signal propagated in less than 3 cycles it will fail as it expects to change within the window. Correct ?

yes, as addressed above

I only had to check if the signal propagates, window was not necessary.

 // I would consider 
 property CDC_prop;
logic v_temp;
@(posedge Clk_A) ($changed(A_in), v_temp = A_in) |=>
@(posedge Clk_B) ##[1:6] // the 1'b1 is not needed 
      (B_out == v_temp); // any reason for the 3:6?
endproperty:CDC_prop 

Ben systemverilog.us