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 |
1040105906 |
4310 |
0 |
0 |
| T2 |
65997 |
1 |
0 |
0 |
| T3 |
71291 |
1 |
0 |
0 |
| T4 |
93260 |
1 |
0 |
0 |
| T5 |
96811 |
2 |
0 |
0 |
| T6 |
127653 |
2 |
0 |
0 |
| T7 |
104030 |
2 |
0 |
0 |
| T8 |
92025 |
2 |
0 |
0 |
| T25 |
193688 |
3 |
0 |
0 |
| T86 |
186119 |
0 |
0 |
0 |
| T102 |
66235 |
1 |
0 |
0 |
| T103 |
83457 |
1 |
0 |
0 |
| T166 |
419729 |
0 |
0 |
0 |
| T199 |
241114 |
0 |
0 |
0 |
| T207 |
118276 |
0 |
0 |
0 |
| T212 |
101329 |
8 |
0 |
0 |
| T213 |
89684 |
6 |
0 |
0 |
| T214 |
0 |
3 |
0 |
0 |
| T262 |
0 |
8 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T316 |
0 |
2 |
0 |
0 |
| T317 |
170195 |
0 |
0 |
0 |
| T318 |
219710 |
0 |
0 |
0 |
| T319 |
98031 |
0 |
0 |
0 |
| T320 |
63003 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
1040105906 |
4310 |
0 |
0 |
| T2 |
65997 |
1 |
0 |
0 |
| T3 |
71291 |
1 |
0 |
0 |
| T4 |
93260 |
1 |
0 |
0 |
| T5 |
96811 |
2 |
0 |
0 |
| T6 |
127653 |
2 |
0 |
0 |
| T7 |
104030 |
2 |
0 |
0 |
| T8 |
92025 |
2 |
0 |
0 |
| T25 |
193688 |
3 |
0 |
0 |
| T86 |
186119 |
0 |
0 |
0 |
| T102 |
66235 |
1 |
0 |
0 |
| T103 |
83457 |
1 |
0 |
0 |
| T166 |
419729 |
0 |
0 |
0 |
| T199 |
241114 |
0 |
0 |
0 |
| T207 |
118276 |
0 |
0 |
0 |
| T212 |
101329 |
8 |
0 |
0 |
| T213 |
89684 |
6 |
0 |
0 |
| T214 |
0 |
3 |
0 |
0 |
| T262 |
0 |
8 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T316 |
0 |
2 |
0 |
0 |
| T317 |
170195 |
0 |
0 |
0 |
| T318 |
219710 |
0 |
0 |
0 |
| T319 |
98031 |
0 |
0 |
0 |
| T320 |
63003 |
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 |
520052953 |
35 |
0 |
0 |
| T86 |
186119 |
0 |
0 |
0 |
| T166 |
419729 |
0 |
0 |
0 |
| T199 |
241114 |
0 |
0 |
0 |
| T207 |
118276 |
0 |
0 |
0 |
| T212 |
101329 |
8 |
0 |
0 |
| T213 |
89684 |
6 |
0 |
0 |
| T214 |
0 |
3 |
0 |
0 |
| T262 |
0 |
8 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T316 |
0 |
2 |
0 |
0 |
| T317 |
170195 |
0 |
0 |
0 |
| T318 |
219710 |
0 |
0 |
0 |
| T319 |
98031 |
0 |
0 |
0 |
| T320 |
63003 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
520052953 |
35 |
0 |
0 |
| T86 |
186119 |
0 |
0 |
0 |
| T166 |
419729 |
0 |
0 |
0 |
| T199 |
241114 |
0 |
0 |
0 |
| T207 |
118276 |
0 |
0 |
0 |
| T212 |
101329 |
8 |
0 |
0 |
| T213 |
89684 |
6 |
0 |
0 |
| T214 |
0 |
3 |
0 |
0 |
| T262 |
0 |
8 |
0 |
0 |
| T263 |
0 |
8 |
0 |
0 |
| T316 |
0 |
2 |
0 |
0 |
| T317 |
170195 |
0 |
0 |
0 |
| T318 |
219710 |
0 |
0 |
0 |
| T319 |
98031 |
0 |
0 |
0 |
| T320 |
63003 |
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 |
520052953 |
4275 |
0 |
0 |
| T2 |
65997 |
1 |
0 |
0 |
| T3 |
71291 |
1 |
0 |
0 |
| T4 |
93260 |
1 |
0 |
0 |
| T5 |
96811 |
2 |
0 |
0 |
| T6 |
127653 |
2 |
0 |
0 |
| T7 |
104030 |
2 |
0 |
0 |
| T8 |
92025 |
2 |
0 |
0 |
| T25 |
193688 |
3 |
0 |
0 |
| T102 |
66235 |
1 |
0 |
0 |
| T103 |
83457 |
1 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
520052953 |
4275 |
0 |
0 |
| T2 |
65997 |
1 |
0 |
0 |
| T3 |
71291 |
1 |
0 |
0 |
| T4 |
93260 |
1 |
0 |
0 |
| T5 |
96811 |
2 |
0 |
0 |
| T6 |
127653 |
2 |
0 |
0 |
| T7 |
104030 |
2 |
0 |
0 |
| T8 |
92025 |
2 |
0 |
0 |
| T25 |
193688 |
3 |
0 |
0 |
| T102 |
66235 |
1 |
0 |
0 |
| T103 |
83457 |
1 |
0 |
0 |
