Unified Coverage Report :: Module :: prim_sync_reqack

Module : prim_sync_reqack_data

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
100.00	100.00					100.00

Source File(s) :
/workspaces/repo/scratch/os_regression_2024_10_02/alert_handler-sim-vcs/default/sim-vcs/../src/lowrisc_prim_all_0.1/rtl/prim_sync_reqack_data.sv

Module self-instances :

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
tb.dut.u_edn_req.u_prim_sync_reqack_data	100.00	100.00					100.00

Module Instance : tb.dut.u_edn_req.u_prim_sync_reqack_data

Instance :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
100.00	100.00					100.00

Instance's subtree :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
95.83	100.00	83.33			100.00	100.00

Parent :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT	NAME
96.15	100.00	84.62			100.00	100.00	u_edn_req

Subtrees :

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
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.	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

	Total	Attempted	Percent	Succeeded/Matched	Percent
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

Name	Attempts	Real Successes	Failures	Incomplete
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA	538552980	4719	0	0
gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB	538552980	4642	0	0

gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcA

Name	Attempts	Real Successes
Total	538552980	4719
T1	1561	1
T2	4616	1
T3	3651	1
T4	12866	104
T5	17765	134
T6	17214	93
T10	18028	1
T11	22732	1
T12	2597	1
T28	35331	1

gen_assert_data_dst2src.SyncReqAckDataHoldDst2SrcB

Name	Attempts	Real Successes
Total	538552980	4642
T1	1561	1
T2	4616	1
T3	3651	1
T4	12866	104
T5	17765	134
T6	17214	83
T10	18028	1
T11	22732	1
T12	2597	1
T28	35331	1