IMPORTANT NOTICE: Please be advised that the Verification Academy Forums will be offline for scheduled maintenance on Sunday, April 6th at 2:00 US/Pacific.
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 ?
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:
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:
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.
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.
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?
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.
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