Module Definition
dashboard | hierarchy | modlist | groups | tests | asserts



Module Instance : tb.dut.u_reseed_ctrl.u_edn_req.u_prim_sync_reqack_data

Instance :
SCORELINECONDTOGGLEFSMBRANCHASSERT
100.00 100.00 100.00


Instance's subtree :
SCORELINECONDTOGGLEFSMBRANCHASSERT
95.83 100.00 83.33 100.00 100.00


Parent :
SCORELINECONDTOGGLEFSMBRANCHASSERTNAME
98.08 100.00 92.31 100.00 100.00 u_edn_req


Subtrees :
NAMESCORELINECONDTOGGLEFSMBRANCHASSERT
u_prim_sync_reqack 95.83 100.00 83.33 100.00 100.00


Since this is the module's only instance, the coverage report is the same as for the module.
Line Coverage for Module : prim_sync_reqack_data
Line No.TotalCoveredPercent
TOTAL11100.00
CONT_ASSIGN9311100.00
CONT_ASSIGN15300
CONT_ASSIGN15600
ALWAYS15900

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
TotalAttemptedPercentSucceeded/MatchedPercent
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

NameAttemptsReal SuccessesFailuresIncomplete
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA 21705443 92352 0 0
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB 21705443 92340 0 0


gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA
NameAttemptsReal SuccessesFailuresIncomplete
Total 21705443 92352 0 0
T1 5456 64 0 0
T2 18058 6 0 0
T3 17046 66 0 0
T4 5438 8 0 0
T13 1307 0 0 0
T14 4324 46 0 0
T15 4964 60 0 0
T16 4832 6 0 0
T17 9788 94 0 0
T18 11952 10 0 0
T35 0 18 0 0

gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB
NameAttemptsReal SuccessesFailuresIncomplete
Total 21705443 92340 0 0
T1 5456 64 0 0
T2 18058 6 0 0
T3 17046 66 0 0
T4 5438 8 0 0
T13 1307 0 0 0
T14 4324 46 0 0
T15 4964 60 0 0
T16 4832 6 0 0
T17 9788 94 0 0
T18 11952 10 0 0
T35 0 18 0 0

0% 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%