I want to write multi-clock CDC assertion for - three edge requirement. Data on tx side should remain unchanged for 3 edge of rx clock. Can you please help? My concern is how to get 3 rx clock (any) edge calculated to tx side for asserting data on tx side stable. Three edge requirement : “input data values must be stable for three destination clock edges”
Hi,
I want to write multi-clock CDC assertion for - three edge requirement. Data on tx side should remain unchanged for 3 edge of rx clock. Can you please help? My concern is how to get 3 rx clock (any) edge calculated to tx side for asserting data on tx side stable. Three edge requirement : “input data values must be stable for three destination clock edges”
//it should be something like this
property tx_data_check;
@(posedge tx_clk)
(start_exp) |-> (@(posedge rx_clk) $stable(tx_data)[*3])
endproperty
Thanks for reply. As per my understanding, there are some flaws in idea of your assertion.
$stable(tx_data) should be checked by tx_clk rather than rx_clk, as in case of fast-to-slow CDC, change of tx_data on tx_clk may get missed by slow rx_clk. And I think it’s wise to check tx_data stability with respect to tx_clk, as change of tx_data is sensitive to tx_clk.
@(posedge tx/rx_clk) $stable(tx_data)[*3] - here, stability is checked for 3 posedge of tx/rx_clk, but the three edge requirement is any edge, pos-neg-pos or neg-pos-neg.
If I think of @(edge rx_clk) for 3 edges of rx_clk, potential issue I see is use of ##1 in writing sequence after it will not help me as ##1 means whole clock period only.
I tried one solution on my end. It seems working, but not sure if any flaws. Can you please help finding any issue with it? Or better suggestions/other better solutions?
module m();
int data;
bit src_clk,dst_clk;
initial forever #5 src_clk=~src_clk;
initial forever #8 dst_clk=~dst_clk;
initial #10000 $finish();
initial begin : TB
@(posedge src_clk) data = 15;
repeat (1) @(posedge src_clk);
@(posedge src_clk) data = 24;
end
sequence seq; // Counts 3 edge of dst_clk after data changed on src_clk
@(posedge src_clk) $changed(data) ##1 @(edge dst_clk) (1) ##1 @(edge dst_clk)(1) ##1 @(edge dst_clk) (1);
endsequence
property p1; // checks data stability on src_clk until above seq gets completed.
int d;
@(posedge src_clk) $changed(data) |=> stable(data) [*1:] ##1 (seq.matched,$display(“t=%t\n”,$time));
endproperty
assert property (p1);
endmodule
Probable issue I see here is, display time t is in multiple of 5 (src_clk), I was expecting time t in multiple of 8(dst_clk), as seq.matched ends with @(edge dst_clk). Otherwise, I find this code working well for requirement.
Thanks, Ben. My concept of ##1 got clear w.r.t clocking event.
Now in case, I want to satisfy requirement of checking stability of tx_data on tx_clk, modification in my previously provided code and overall property is correct?
In reply to shahkavish77:
Your code looks ok, except that I would write
@(posedge src_clk) $changed(data) ##1 @(dst_clk) (1)[*3];
// Basically use @(dst_clk) instead of @(edge dst_clk) since
// @(dst_clk) are the edges of dest_clk.
You need to simulate this.
Ben SystemVerilog.us
Thanks, Ben. I simulated the code, I couldn’t understand why displayed time t is in multiple of 5 (src_clk), I was expecting time t in multiple of 8(dst_clk), as seq.matched ends with @(edge dst_clk). If you can help understanding it, it would be great help.
In reply to shahkavish77:
Without a test model and testbench, it is hard to say.
Write a testbench, add debugging events with sequence_matched_items. and debug it.
If this is of any help, I tune this generic model as a start to verify my assertions.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk, a, b;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// assertions here
initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb) with
{ va dist {1'b1:=1, 1'b0:=3};
vb dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
end
a <= va;
b <= vb;
$finish;
end
endmodule