Unified Coverage Report :: Module :: prim_sync_reqack

Line Coverage for Module : prim_sync_reqack_data

	Line No.	Total	Covered	Percent
TOTAL		1	1	100.00
CONT_ASSIGN	93	1	1	100.00
CONT_ASSIGN	153	0	0
CONT_ASSIGN	156	0	0
ALWAYS	159	0	0



92                          // Just feed through the data.
93         1/1              assign data_o = data_i;
           Tests:       T1 T2 T5 
94                        end
95                      
96                        ////////////////
97                        // Assertions //
98                        ////////////////
99                        if (DataSrc2Dst == 1'b1) begin : gen_assert_data_src2dst
100                     `ifdef INC_ASSERT
101                         //VCS coverage off
102                         // pragma coverage off
103                         logic effective_rst_n;
104                         assign effective_rst_n = rst_src_ni && rst_dst_ni;
105                     
106                         logic chk_flag_d, chk_flag_q;
107                         assign chk_flag_d = src_req_i && !chk_flag_q ? 1'b1 : chk_flag_q;
108                     
109                         always_ff @(posedge clk_src_i or negedge effective_rst_n) begin
110                           if (!effective_rst_n) begin
111                             chk_flag_q <= '0;
112                           end else begin
113                             chk_flag_q <= chk_flag_d;
114                           end
115                         end
116                         //VCS coverage on
117                         // pragma coverage on
118                     
119                         // SRC domain cannot change data while waiting for ACK.
120                         `ASSERT(SyncReqAckDataHoldSrc2Dst, !$stable(data_i) && chk_flag_q |->
121                             (!src_req_i || (src_req_i && src_ack_o)),
122                             clk_src_i, !rst_src_ni || !rst_dst_ni || !chk_flag_q)
123                     
124                         // Register stage cannot be used.
125                         `ASSERT_INIT(SyncReqAckDataReg, DataSrc2Dst && !DataReg)
126                     `endif
127                       end else if (DataSrc2Dst == 1'b0 && DataReg == 1'b0) begin : gen_assert_data_dst2src
128                         // DST domain shall not change data while waiting for SRC domain to latch it (together with
129                         // receiving ACK). It takes 2 SRC cycles for ACK to cross over from DST to SRC, and 1 SRC cycle
130                         // for the next REQ to cross over from SRC to DST.
131                         //
132                         // Denote the src clock where REQ & ACK as time zero. The data flowing through the CDC could be
133                         // corrupted if data_o was not stable over the previous 2 clock cycles (so we want to check time
134                         // points -2, -1 and 0). Moreover, the DST domain cannot know that it is allowed to change value
135                         // until at least one more SRC cycle (the time taken for REQ to cross back from SRC to DST).
136                         //
137                         // To make this assertion, we will sample at each of 4 time points (-2, -1, 0 and +1), asserting
138                         // that data_o is equal at each of these times. Note this won't detect glitches at intermediate
139                         // timepoints.
140                         //
141                         // The SVAs below are designed not to consume time, which means that they can be disabled with
142                         // an $assertoff(..) and won't linger to fail later. This wouldn't work properly if we used
143                         // something like |=> instead of the $past(...) function. That means that we have to trigger at
144                         // the "end" of the window. To make sure we don't miss a situation where the value changed at
145                         // time -1 (causing corruption), but reset was asserted between time 0 and 1, we split the
146                         // assertion into two pieces. The first (SyncReqAckDataHoldDst2SrcA) checks that data doesn't
147                         // change in a way that could cause data corruption. The second (SyncReqAckDataHoldDst2SrcB)
148                         // checks that the DST side doesn't do anything that it shouldn't know is safe.
149                     `ifdef INC_ASSERT
150                         //VCS coverage off
151                         // pragma coverage off
152                         logic effective_rst_n;
153        unreachable      assign effective_rst_n = rst_src_ni && rst_dst_ni;
154                     
155                         logic chk_flag_d, chk_flag_q;
156        unreachable      assign chk_flag_d = src_req_i && !chk_flag_q ? 1'b1 : chk_flag_q;
157                     
158                         always_ff @(posedge clk_src_i or negedge effective_rst_n) begin
159        unreachable        if (!effective_rst_n) begin
160        unreachable          chk_flag_q <= '0;
161                           end else begin
162        unreachable          chk_flag_q <= chk_flag_d;

Assert Coverage for Module : prim_sync_reqack_data

	Total	Attempted	Percent	Succeeded/Matched	Percent
Assertions	2	2	100.00	2	100.00
Cover properties	0	0		0
Cover sequences	0	0		0
Total	2	2	100.00	2	100.00

Assertion Details

Name	Attempts	Real Successes	Failures	Incomplete
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA	314156745	9280	0	0
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB	314156745	9278	0	0

gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA

Name	Attempts	Real Successes
Total	314156745	9280
T1	13331	6
T2	2443	1
T3	746	0
T4	8701	0
T5	5906	1
T6	55020	34
T7	57520	0
T9	23629	2
T10	23968	2
T11	1873	1
T31	0	2
T35	0	1
T36	0	2

gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB

Name	Attempts	Real Successes
Total	314156745	9278
T1	13331	6
T2	2443	1
T3	746	0
T4	8701	0
T5	5906	1
T6	55020	34
T7	57520	0
T9	23629	2
T10	23968	2
T11	1873	1
T31	0	2
T35	0	1
T36	0	2

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
100.00	100.00					100.00

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
tb.dut.u_prim_sync_reqack_data	100.00	100.00					100.00

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
100.00	100.00					100.00

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT	NAME
91.90	100.00	88.89	100.00		100.00	70.59	dut

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
u_prim_sync_reqack	100.00	100.00	100.00			100.00	100.00