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 T3
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 |
942193710 |
4257 |
0 |
0 |
| T1 |
79194 |
1 |
0 |
0 |
| T2 |
59963 |
1 |
0 |
0 |
| T3 |
211087 |
1 |
0 |
0 |
| T4 |
123510 |
2 |
0 |
0 |
| T5 |
294721 |
2 |
0 |
0 |
| T6 |
96786 |
2 |
0 |
0 |
| T29 |
74935 |
2 |
0 |
0 |
| T33 |
96569 |
1 |
0 |
0 |
| T34 |
0 |
1 |
0 |
0 |
| T103 |
42263 |
0 |
0 |
0 |
| T104 |
63494 |
1 |
0 |
0 |
| T149 |
205572 |
0 |
0 |
0 |
| T152 |
214473 |
0 |
0 |
0 |
| T153 |
201574 |
0 |
0 |
0 |
| T165 |
234807 |
0 |
0 |
0 |
| T177 |
170646 |
0 |
0 |
0 |
| T211 |
85529 |
11 |
0 |
0 |
| T212 |
0 |
8 |
0 |
0 |
| T214 |
0 |
8 |
0 |
0 |
| T276 |
0 |
8 |
0 |
0 |
| T320 |
0 |
12 |
0 |
0 |
| T321 |
0 |
7 |
0 |
0 |
| T322 |
619083 |
0 |
0 |
0 |
| T323 |
398637 |
0 |
0 |
0 |
| T324 |
179316 |
0 |
0 |
0 |
| T325 |
643909 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
942193710 |
4257 |
0 |
0 |
| T1 |
79194 |
1 |
0 |
0 |
| T2 |
59963 |
1 |
0 |
0 |
| T3 |
211087 |
1 |
0 |
0 |
| T4 |
123510 |
2 |
0 |
0 |
| T5 |
294721 |
2 |
0 |
0 |
| T6 |
96786 |
2 |
0 |
0 |
| T29 |
74935 |
2 |
0 |
0 |
| T33 |
96569 |
1 |
0 |
0 |
| T34 |
0 |
1 |
0 |
0 |
| T103 |
42263 |
0 |
0 |
0 |
| T104 |
63494 |
1 |
0 |
0 |
| T149 |
205572 |
0 |
0 |
0 |
| T152 |
214473 |
0 |
0 |
0 |
| T153 |
201574 |
0 |
0 |
0 |
| T165 |
234807 |
0 |
0 |
0 |
| T177 |
170646 |
0 |
0 |
0 |
| T211 |
85529 |
11 |
0 |
0 |
| T212 |
0 |
8 |
0 |
0 |
| T214 |
0 |
8 |
0 |
0 |
| T276 |
0 |
8 |
0 |
0 |
| T320 |
0 |
12 |
0 |
0 |
| T321 |
0 |
7 |
0 |
0 |
| T322 |
619083 |
0 |
0 |
0 |
| T323 |
398637 |
0 |
0 |
0 |
| T324 |
179316 |
0 |
0 |
0 |
| T325 |
643909 |
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 T3
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 |
471096855 |
54 |
0 |
0 |
| T149 |
205572 |
0 |
0 |
0 |
| T152 |
214473 |
0 |
0 |
0 |
| T153 |
201574 |
0 |
0 |
0 |
| T165 |
234807 |
0 |
0 |
0 |
| T177 |
170646 |
0 |
0 |
0 |
| T211 |
85529 |
11 |
0 |
0 |
| T212 |
0 |
8 |
0 |
0 |
| T214 |
0 |
8 |
0 |
0 |
| T276 |
0 |
8 |
0 |
0 |
| T320 |
0 |
12 |
0 |
0 |
| T321 |
0 |
7 |
0 |
0 |
| T322 |
619083 |
0 |
0 |
0 |
| T323 |
398637 |
0 |
0 |
0 |
| T324 |
179316 |
0 |
0 |
0 |
| T325 |
643909 |
0 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
471096855 |
54 |
0 |
0 |
| T149 |
205572 |
0 |
0 |
0 |
| T152 |
214473 |
0 |
0 |
0 |
| T153 |
201574 |
0 |
0 |
0 |
| T165 |
234807 |
0 |
0 |
0 |
| T177 |
170646 |
0 |
0 |
0 |
| T211 |
85529 |
11 |
0 |
0 |
| T212 |
0 |
8 |
0 |
0 |
| T214 |
0 |
8 |
0 |
0 |
| T276 |
0 |
8 |
0 |
0 |
| T320 |
0 |
12 |
0 |
0 |
| T321 |
0 |
7 |
0 |
0 |
| T322 |
619083 |
0 |
0 |
0 |
| T323 |
398637 |
0 |
0 |
0 |
| T324 |
179316 |
0 |
0 |
0 |
| T325 |
643909 |
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 T3
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 |
471096855 |
4203 |
0 |
0 |
| T1 |
79194 |
1 |
0 |
0 |
| T2 |
59963 |
1 |
0 |
0 |
| T3 |
211087 |
1 |
0 |
0 |
| T4 |
123510 |
2 |
0 |
0 |
| T5 |
294721 |
2 |
0 |
0 |
| T6 |
96786 |
2 |
0 |
0 |
| T29 |
74935 |
2 |
0 |
0 |
| T33 |
96569 |
1 |
0 |
0 |
| T34 |
0 |
1 |
0 |
0 |
| T103 |
42263 |
0 |
0 |
0 |
| T104 |
63494 |
1 |
0 |
0 |
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
| Name | Attempts | Real Successes | Failures | Incomplete |
| Total |
471096855 |
4203 |
0 |
0 |
| T1 |
79194 |
1 |
0 |
0 |
| T2 |
59963 |
1 |
0 |
0 |
| T3 |
211087 |
1 |
0 |
0 |
| T4 |
123510 |
2 |
0 |
0 |
| T5 |
294721 |
2 |
0 |
0 |
| T6 |
96786 |
2 |
0 |
0 |
| T29 |
74935 |
2 |
0 |
0 |
| T33 |
96569 |
1 |
0 |
0 |
| T34 |
0 |
1 |
0 |
0 |
| T103 |
42263 |
0 |
0 |
0 |
| T104 |
63494 |
1 |
0 |
0 |
