In reply to ben@SystemVerilog.us:
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.
@(posedge Clk_A) ($changed(A_in), v_temp = A_in) |=>
@(posedge Clk_B) 1'b1 ##[2:3]
($changed(B_out) && (B_out === v_temp));