Sva CDC Paper Dvcon2006
Sva CDC Paper Dvcon2006
Sva CDC Paper Dvcon2006
Abstract
Recent advances in automated formal solutions
for verification of clock domain crossing signals go
far towards reducing the risk of clock related defects
in multi-clock system-on-chip devices. However the
vast majority of multiple clock-domain devices still
utilize a flow which does not involve these specialized
tools or formal verification techniques. This paper
presents a pragmatic alternative methodology, using
SystemVerilog Assertions in a simulation-based
verification flow, to validate the correct operation
and use of synchronizers while emulating the effects
of CDC jitter in order to stress the functional
operation of the rest of the device.
Introduction
-1-
Structural Analysis
DVCon 2006
Property Definitions
4.1
-2-
4.2
d_in
d_out
clk
Figure 2: 2-Flip-Flop Synchronizer
If no assumptions are made about the relationship
between the source and destination clock domains,
then the following property ensures that all input
signal values can be reliably transported to the
synchronizer output:
input data values must be stable for three
destination clock edges
There are three specific cases where input values
might not get transported to the synchronizer output;
values that are:
never sampled by the destination clock
sampled by only one clock edge
sampled by only two successive clocks
The timing diagram shown in Figure 3 illustrates
potential filtering due to metastability in each case.
The first high pulse on d_in is never sampled by the
clock and it is not propagated during simulation; note
however that if the rising edge of this pulse violated
the previous hold-time, or the falling edge violated
the current setup-time, then this value might get
propagated in real life. The second pulse on d_in is
sampled by the destination clock; but if the signal
changes just before the clock edge (a setup-time
violation) then the simulation will propagate the new
value, but the real circuit might become metastable
and decay to original low value. The third pulse on
d_in illustrates the case where even though the signal
is sampled by two successive clock edges, it can still
DVCon 2006
t
p_in
clk_i
p_out
EN
toggle
edge detect
clk_o
Figure 5: Pulse Synchronizer
In this case the data transfer is managed using a
pulse-based handshake synchronizer as shown in
Figure 6. The source requests a transfer of the
bundled data by asserting req_o high for a single
clock; this request is synchronized into the
destination domain as a req_i pulse, which is used to
latch the data. The destination responds by
generating an acknowledge pulse, ack_o, which is
synchronized back into the source domain to signal
the end of the transfer.
SOURCE
req_o
DESTINATION
req_i
dest_clk
ack_i
ack_o
src_clk
assert property(p_stability);
assert property(p_no_glitch);
data_o
data_i
4.3
-3-
DVCon 2006
sequence s_transfer;
@(posedge clk)
req ##1 !req [*1:max] ##0 ack;
endsequence : s_transfer
4.4
property p_req_gets_ack;
@(posedge clk)
req |-> s_transfer;
endproperty : p_req_gets_ack
property p_ack_had_req;
@(posedge clk)
ack |-> s_transfer.ended;
endproperty : p_ack_had_req
property p_data_stable;
@(posedge clk)
req |=> $stable(data) [*1:max] ##0 ack;
endproperty : p_data_stable
wclk
assert property(p_req_gets_ack);
assert property(p_ack_had_req);
assert property(p_data_stable);
wfull
winc
wdata
Write
Control
wptr
rptr
wa
ra
RAM
wen
wd
rd
Read
Control
rclk
rempty
rinc
rdata
-4-
DVCon 2006
Assertion Validation
random
assert property(p_bad_access(wclk,winc,wfull));
assert property(p_bad_access(rclk,rinc,rempty));
assert property(p_gray_code(wclk,wrst_n,wptr));
assert property(p_gray_code(rclk,rrst_n,rptr));
assert property (p_data_integrity);
@(m2 or m3)
random
d_out
d_in
m1
m2
m3
clk
Figure 11: Synchronizer with Jitter Emulation
-5-
DVCon 2006
-6-
Conclusion
References
DVCon 2006