CDC SV Assertion

SystemVerilog
, , ,
1

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”

2

In reply to shahkavish77:

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
3

In reply to Rahulkumar Patel:

Hi Rahul,

Thanks for reply. As per my understanding, there are some flaws in idea of your assertion.

  1. $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.

  2. @(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.

Need to modify assertion for proper solution.

Thanks,
Kavish

4

Hi All,

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,
Kavish

5

In reply to shahkavish77:

as ##1 means whole clock period only.

ap: assert property(@ (clocking_event1) (start_exp) |-> 
   @ (clocking_event2) $stable(tx_data)[*3]);
Per 1800'2017 14.3 Clocking block declaration
clocking_event ::=
@ identifier
| @ ( event_expression )
Also, the $rose can include the clocking event. 
$rose ( expression [, [clocking_event] ] )  
Thus, the following is legal 
property tx_data_check;
  @(tx_clk)
  (start_exp) |-> (@(rx_clk) $stable(tx_data)[*3])
endproperty

My SVA Handbook 4th Edition addresses multiclocking and its various rules. The following link is 4 pages from my book; it may clarify several issues.

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

  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
6

In reply to ben@SystemVerilog.us:

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?

sequence seq;
@(posedge src_clk) $changed(data) ##1 @(edge dst_clk) (1)[*3];
endsequence
property p1;
int d;
@(posedge src_clk) $changed(data) |=> stable(data) [*1:] ##1 (seq.matched,$display(“t=%t\n”,$time));
endproperty
assert property (p1);

Thanks,
Kavish

7

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

8

In reply to 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.

9

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

Ben SystemVerilog.us