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: T2 T3 T4
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
Assertion Details
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
981530332 |
4300 |
0 |
0 |
| T2 |
65307 |
1 |
0 |
0 |
| T3 |
76232 |
1 |
0 |
0 |
| T4 |
83391 |
2 |
0 |
0 |
| T5 |
102036 |
2 |
0 |
0 |
| T6 |
96790 |
2 |
0 |
0 |
| T7 |
82758 |
1 |
0 |
0 |
| T10 |
110267 |
2 |
0 |
0 |
| T13 |
86437 |
2 |
0 |
0 |
| T76 |
138074 |
0 |
0 |
0 |
| T88 |
163199 |
0 |
0 |
0 |
| T89 |
142691 |
0 |
0 |
0 |
| T106 |
87384 |
1 |
0 |
0 |
| T107 |
82198 |
1 |
0 |
0 |
| T205 |
87989 |
8 |
0 |
0 |
| T206 |
90439 |
8 |
0 |
0 |
| T207 |
0 |
7 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T264 |
0 |
8 |
0 |
0 |
| T294 |
0 |
10 |
0 |
0 |
| T295 |
202705 |
0 |
0 |
0 |
| T296 |
56839 |
0 |
0 |
0 |
| T297 |
164353 |
0 |
0 |
0 |
| T298 |
417830 |
0 |
0 |
0 |
| T299 |
123327 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
981530332 |
4300 |
0 |
0 |
| T2 |
65307 |
1 |
0 |
0 |
| T3 |
76232 |
1 |
0 |
0 |
| T4 |
83391 |
2 |
0 |
0 |
| T5 |
102036 |
2 |
0 |
0 |
| T6 |
96790 |
2 |
0 |
0 |
| T7 |
82758 |
1 |
0 |
0 |
| T10 |
110267 |
2 |
0 |
0 |
| T13 |
86437 |
2 |
0 |
0 |
| T76 |
138074 |
0 |
0 |
0 |
| T88 |
163199 |
0 |
0 |
0 |
| T89 |
142691 |
0 |
0 |
0 |
| T106 |
87384 |
1 |
0 |
0 |
| T107 |
82198 |
1 |
0 |
0 |
| T205 |
87989 |
8 |
0 |
0 |
| T206 |
90439 |
8 |
0 |
0 |
| T207 |
0 |
7 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T264 |
0 |
8 |
0 |
0 |
| T294 |
0 |
10 |
0 |
0 |
| T295 |
202705 |
0 |
0 |
0 |
| T296 |
56839 |
0 |
0 |
0 |
| T297 |
164353 |
0 |
0 |
0 |
| T298 |
417830 |
0 |
0 |
0 |
| T299 |
123327 |
0 |
0 |
0 |
Line Coverage for Instance : tb.dut.top_earlgrey.u_rv_core_ibex.u_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: T2 T3 T4
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 Instance : tb.dut.top_earlgrey.u_rv_core_ibex.u_prim_sync_reqack_data
Assertion Details
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
490765166 |
49 |
0 |
0 |
| T76 |
138074 |
0 |
0 |
0 |
| T88 |
163199 |
0 |
0 |
0 |
| T89 |
142691 |
0 |
0 |
0 |
| T205 |
87989 |
8 |
0 |
0 |
| T206 |
90439 |
8 |
0 |
0 |
| T207 |
0 |
7 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T264 |
0 |
8 |
0 |
0 |
| T294 |
0 |
10 |
0 |
0 |
| T295 |
202705 |
0 |
0 |
0 |
| T296 |
56839 |
0 |
0 |
0 |
| T297 |
164353 |
0 |
0 |
0 |
| T298 |
417830 |
0 |
0 |
0 |
| T299 |
123327 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
490765166 |
49 |
0 |
0 |
| T76 |
138074 |
0 |
0 |
0 |
| T88 |
163199 |
0 |
0 |
0 |
| T89 |
142691 |
0 |
0 |
0 |
| T205 |
87989 |
8 |
0 |
0 |
| T206 |
90439 |
8 |
0 |
0 |
| T207 |
0 |
7 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T264 |
0 |
8 |
0 |
0 |
| T294 |
0 |
10 |
0 |
0 |
| T295 |
202705 |
0 |
0 |
0 |
| T296 |
56839 |
0 |
0 |
0 |
| T297 |
164353 |
0 |
0 |
0 |
| T298 |
417830 |
0 |
0 |
0 |
| T299 |
123327 |
0 |
0 |
0 |
Line Coverage for Instance : tb.dut.top_earlgrey.u_rv_core_ibex.u_edn_if.u_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: T2 T3 T4
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 Instance : tb.dut.top_earlgrey.u_rv_core_ibex.u_edn_if.u_prim_sync_reqack_data
Assertion Details
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
490765166 |
4251 |
0 |
0 |
| T2 |
65307 |
1 |
0 |
0 |
| T3 |
76232 |
1 |
0 |
0 |
| T4 |
83391 |
2 |
0 |
0 |
| T5 |
102036 |
2 |
0 |
0 |
| T6 |
96790 |
2 |
0 |
0 |
| T7 |
82758 |
1 |
0 |
0 |
| T10 |
110267 |
2 |
0 |
0 |
| T13 |
86437 |
2 |
0 |
0 |
| T106 |
87384 |
1 |
0 |
0 |
| T107 |
82198 |
1 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
490765166 |
4251 |
0 |
0 |
| T2 |
65307 |
1 |
0 |
0 |
| T3 |
76232 |
1 |
0 |
0 |
| T4 |
83391 |
2 |
0 |
0 |
| T5 |
102036 |
2 |
0 |
0 |
| T6 |
96790 |
2 |
0 |
0 |
| T7 |
82758 |
1 |
0 |
0 |
| T10 |
110267 |
2 |
0 |
0 |
| T13 |
86437 |
2 |
0 |
0 |
| T106 |
87384 |
1 |
0 |
0 |
| T107 |
82198 |
1 |
0 |
0 |
