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 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 |
983373876 |
4351 |
0 |
0 |
| T1 |
111924 |
2 |
0 |
0 |
| T2 |
78951 |
1 |
0 |
0 |
| T3 |
42255 |
0 |
0 |
0 |
| T4 |
103207 |
1 |
0 |
0 |
| T5 |
100889 |
2 |
0 |
0 |
| T6 |
100982 |
2 |
0 |
0 |
| T7 |
100472 |
2 |
0 |
0 |
| T19 |
994158 |
0 |
0 |
0 |
| T28 |
97609 |
2 |
0 |
0 |
| T46 |
0 |
4 |
0 |
0 |
| T90 |
163829 |
0 |
0 |
0 |
| T109 |
67839 |
1 |
0 |
0 |
| T110 |
68617 |
1 |
0 |
0 |
| T151 |
190262 |
0 |
0 |
0 |
| T214 |
106556 |
8 |
0 |
0 |
| T215 |
91563 |
4 |
0 |
0 |
| T216 |
0 |
11 |
0 |
0 |
| T257 |
430005 |
0 |
0 |
0 |
| T301 |
0 |
8 |
0 |
0 |
| T302 |
0 |
8 |
0 |
0 |
| T344 |
0 |
2 |
0 |
0 |
| T345 |
225161 |
0 |
0 |
0 |
| T346 |
595542 |
0 |
0 |
0 |
| T347 |
75054 |
0 |
0 |
0 |
| T348 |
541796 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
983373876 |
4351 |
0 |
0 |
| T1 |
111924 |
2 |
0 |
0 |
| T2 |
78951 |
1 |
0 |
0 |
| T3 |
42255 |
0 |
0 |
0 |
| T4 |
103207 |
1 |
0 |
0 |
| T5 |
100889 |
2 |
0 |
0 |
| T6 |
100982 |
2 |
0 |
0 |
| T7 |
100472 |
2 |
0 |
0 |
| T19 |
994158 |
0 |
0 |
0 |
| T28 |
97609 |
2 |
0 |
0 |
| T46 |
0 |
4 |
0 |
0 |
| T90 |
163829 |
0 |
0 |
0 |
| T109 |
67839 |
1 |
0 |
0 |
| T110 |
68617 |
1 |
0 |
0 |
| T151 |
190262 |
0 |
0 |
0 |
| T214 |
106556 |
8 |
0 |
0 |
| T215 |
91563 |
4 |
0 |
0 |
| T216 |
0 |
11 |
0 |
0 |
| T257 |
430005 |
0 |
0 |
0 |
| T301 |
0 |
8 |
0 |
0 |
| T302 |
0 |
8 |
0 |
0 |
| T344 |
0 |
2 |
0 |
0 |
| T345 |
225161 |
0 |
0 |
0 |
| T346 |
595542 |
0 |
0 |
0 |
| T347 |
75054 |
0 |
0 |
0 |
| T348 |
541796 |
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: T1 T2 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 |
491686938 |
41 |
0 |
0 |
| T19 |
994158 |
0 |
0 |
0 |
| T90 |
163829 |
0 |
0 |
0 |
| T151 |
190262 |
0 |
0 |
0 |
| T214 |
106556 |
8 |
0 |
0 |
| T215 |
91563 |
4 |
0 |
0 |
| T216 |
0 |
11 |
0 |
0 |
| T257 |
430005 |
0 |
0 |
0 |
| T301 |
0 |
8 |
0 |
0 |
| T302 |
0 |
8 |
0 |
0 |
| T344 |
0 |
2 |
0 |
0 |
| T345 |
225161 |
0 |
0 |
0 |
| T346 |
595542 |
0 |
0 |
0 |
| T347 |
75054 |
0 |
0 |
0 |
| T348 |
541796 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
491686938 |
41 |
0 |
0 |
| T19 |
994158 |
0 |
0 |
0 |
| T90 |
163829 |
0 |
0 |
0 |
| T151 |
190262 |
0 |
0 |
0 |
| T214 |
106556 |
8 |
0 |
0 |
| T215 |
91563 |
4 |
0 |
0 |
| T216 |
0 |
11 |
0 |
0 |
| T257 |
430005 |
0 |
0 |
0 |
| T301 |
0 |
8 |
0 |
0 |
| T302 |
0 |
8 |
0 |
0 |
| T344 |
0 |
2 |
0 |
0 |
| T345 |
225161 |
0 |
0 |
0 |
| T346 |
595542 |
0 |
0 |
0 |
| T347 |
75054 |
0 |
0 |
0 |
| T348 |
541796 |
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: T1 T2 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 |
491686938 |
4310 |
0 |
0 |
| T1 |
111924 |
2 |
0 |
0 |
| T2 |
78951 |
1 |
0 |
0 |
| T3 |
42255 |
0 |
0 |
0 |
| T4 |
103207 |
1 |
0 |
0 |
| T5 |
100889 |
2 |
0 |
0 |
| T6 |
100982 |
2 |
0 |
0 |
| T7 |
100472 |
2 |
0 |
0 |
| T28 |
97609 |
2 |
0 |
0 |
| T46 |
0 |
4 |
0 |
0 |
| T109 |
67839 |
1 |
0 |
0 |
| T110 |
68617 |
1 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
491686938 |
4310 |
0 |
0 |
| T1 |
111924 |
2 |
0 |
0 |
| T2 |
78951 |
1 |
0 |
0 |
| T3 |
42255 |
0 |
0 |
0 |
| T4 |
103207 |
1 |
0 |
0 |
| T5 |
100889 |
2 |
0 |
0 |
| T6 |
100982 |
2 |
0 |
0 |
| T7 |
100472 |
2 |
0 |
0 |
| T28 |
97609 |
2 |
0 |
0 |
| T46 |
0 |
4 |
0 |
0 |
| T109 |
67839 |
1 |
0 |
0 |
| T110 |
68617 |
1 |
0 |
0 |
