Unified Coverage Report :: Module :: prim_alert_receiver

Module : prim_alert_receiver

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
95.18	100.00	100.00	100.00	80.00	95.83	95.24

Source File(s) :
/workspaces/repo/scratch/os_regression_2024_08_22/prim_alert-sim-vcs/default/sim-vcs/../src/lowrisc_prim_alert_0/rtl/prim_alert_receiver.sv

Module self-instances :

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
prim_alert_tb.i_alert_receiver	95.18	100.00	100.00	100.00	80.00	95.83	95.24

---

Module Instance : prim_alert_tb.i_alert_receiver

Instance :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
95.18	100.00	100.00	100.00	80.00	95.83	95.24

Instance's subtree :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
95.18	100.00	100.00	100.00	80.00	95.83	95.24

Parent :

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT	NAME
							prim_alert_tb

Subtrees :

NAME	SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT
no children

---

Since this is the module's only instance, the coverage report is the same as for the module.

Line Coverage for Module : prim_alert_receiver

	Line No.	Total	Covered	Percent
TOTAL		60	60	100.00
CONT_ASSIGN	105	1	1	100.00
CONT_ASSIGN	106	1	1	100.00
CONT_ASSIGN	107	1	1	100.00
CONT_ASSIGN	111	1	1	100.00
CONT_ASSIGN	112	1	1	100.00
CONT_ASSIGN	144	1	1	100.00
CONT_ASSIGN	147	1	1	100.00
CONT_ASSIGN	148	1	1	100.00
CONT_ASSIGN	150	1	1	100.00
CONT_ASSIGN	151	1	1	100.00
ALWAYS	159	43	43	100.00
ALWAYS	253	7	7	100.00

104                       // signalling is performed by a level change event on the diff output
105        1/1            assign ping_req_d  = ping_req_i;
           Tests:       T1 T2 T3 
106        1/1            assign ping_rise   = ping_req_d && !ping_req_q;
           Tests:       T1 T2 T3 
107        1/1            assign ping_tog_pd = (send_init) ? 1'b0         :
           Tests:       T1 T2 T3 
108                                            (send_ping) ? ~ping_tog_pq : ping_tog_pq;
109                     
110                       // in-band reset is performed by sending out an integrity error on purpose.
111        1/1            assign ack_dn      = (send_init) ? ack_pd : ~ack_pd;
           Tests:       T1 T2 T3 
112        1/1            assign ping_tog_dn = ~ping_tog_pd;
           Tests:       T1 T2 T3 
113                     
114                       // This prevents further tool optimizations of the differential signal.
115                       prim_sec_anchor_flop #(
116                         .Width     (2),
117                         .ResetValue(2'b10)
118                       ) u_prim_generic_flop_ack (
119                         .clk_i,
120                         .rst_ni,
121                         .d_i({ack_dn,
122                               ack_pd}),
123                         .q_o({ack_nq,
124                               ack_pq})
125                       );
126                     
127                       prim_sec_anchor_flop #(
128                         .Width     (2),
129                         .ResetValue(2'b10)
130                       ) u_prim_generic_flop_ping (
131                         .clk_i,
132                         .rst_ni,
133                         .d_i({ping_tog_dn,
134                               ping_tog_pd}),
135                         .q_o({ping_tog_nq,
136                               ping_tog_pq})
137                       );
138                     
139                       // the ping pending signal is used in the FSM to distinguish whether the
140                       // incoming handshake shall be treated as an alert or a ping response.
141                       // it is important that this is only set on a rising ping_en level change, since
142                       // otherwise the ping enable signal could be abused to "mask" all native alerts
143                       // as ping responses by constantly tying it to 1.
144        1/1            assign ping_pending_d = ping_rise | ((~ping_ok_o) & ping_req_i & ping_pending_q);
           Tests:       T1 T2 T3 
145                     
146                       // diff pair outputs
147        1/1            assign alert_rx_o.ack_p = ack_pq;
           Tests:       T1 T2 T3 
148        1/1            assign alert_rx_o.ack_n = ack_nq;
           Tests:       T1 T2 T3 
149                     
150        1/1            assign alert_rx_o.ping_p = ping_tog_pq;
           Tests:       T1 T2 T3 
151        1/1            assign alert_rx_o.ping_n = ping_tog_nq;
           Tests:       T1 T2 T3 
152                     
153                       // this FSM receives the four phase handshakes from the alert receiver
154                       // note that the latency of the alert_p/n input diff pair is at least one
155                       // cycle until it enters the receiver FSM. the same holds for the ack_* diff
156                       // pair outputs.
157                       always_comb begin : p_fsm
158                         // default
159        1/1              state_d      = state_q;
           Tests:       T1 T2 T3 
160        1/1              ack_pd       = 1'b0;
           Tests:       T1 T2 T3 
161        1/1              ping_ok_o    = 1'b0;
           Tests:       T1 T2 T3 
162        1/1              integ_fail_o = 1'b0;
           Tests:       T1 T2 T3 
163        1/1              alert_o      = 1'b0;
           Tests:       T1 T2 T3 
164        1/1              send_init    = 1'b0;
           Tests:       T1 T2 T3 
165                         // by default, a ping request leads to a toogle on the differential ping pair
166        1/1              send_ping    = ping_rise;
           Tests:       T1 T2 T3 
167                     
168        1/1              unique case (state_q)
           Tests:       T1 T2 T3 
169                           Idle: begin
170                             // wait for handshake to be initiated
171        1/1                  if (alert_level) begin
           Tests:       T1 T2 T3 
172        1/1                    state_d = HsAckWait;
           Tests:       T1 T2 T3 
173        1/1                    ack_pd  = 1'b1;
           Tests:       T1 T2 T3 
174                               // signal either an alert or ping received on the output
175        1/1                    if (ping_pending_q) begin
           Tests:       T1 T2 T3 
176        1/1                      ping_ok_o = 1'b1;
           Tests:       T1 T2 T3 
177                               end else begin
178        1/1                      alert_o   = 1'b1;
           Tests:       T1 T2 T3 
179                               end
180                             end
                        MISSING_ELSE
181                           end
182                           // waiting for deassertion of alert to complete HS
183                           HsAckWait: begin
184        1/1                  if (!alert_level) begin
           Tests:       T1 T2 T3 
185        1/1                    state_d  = Pause0;
           Tests:       T1 T2 T3 
186                             end else begin
187        1/1                    ack_pd = 1'b1;
           Tests:       T1 T2 T3 
188                             end
189                           end
190                           // pause cycles between back-to-back handshakes
191        1/1                Pause0: state_d = Pause1;
           Tests:       T1 T2 T3 
192        1/1                Pause1: state_d = Idle;
           Tests:       T1 T2 T3 
193                           // this state is only reached if an in-band reset is
194                           // requested via the low-power logic.
195                           InitReq: begin
196                             // we deliberately place a sigint error on the ack and ping lines in this case.
197        1/1                  send_init = 1'b1;
           Tests:       T1 T2 T3 
198                             // suppress any toggles on the ping line while we are in the init phase.
199        1/1                  send_ping = 1'b0;
           Tests:       T1 T2 T3 
200                             // As long as init req is asserted, we remain in this state and acknowledge all incoming
201                             // ping requests. As soon as the init request is dropped however, ping requests are not
202                             // acked anymore such that the ping mechanism can also flag alert channels that got stuck
203                             // in the initialization sequence.
204        1/1                  if (mubi4_test_true_strict(init_trig_i)) begin
           Tests:       T1 T2 T3 
205        1/1                    ping_ok_o = ping_pending_q;
           Tests:       T1 T2 T3 
206                             // the sender will respond to the sigint error above with a sigint error on the alert lines.
207                             // hence we treat the alert_sigint like an acknowledgement in this case.
208        1/1                  end else if (alert_sigint) begin
           Tests:       T1 T2 T3 
209        1/1                    state_d = InitAckWait;
           Tests:       T1 T2 T3 
210                             end
                        MISSING_ELSE
211                           end
212                           // We get here if the sender has responded with alert_sigint, and init_trig_i==lc_ctrl_pkg::On
213                           // has been deasserted. At this point, we need to wait for the alert_sigint to drop again
214                           // before resuming normal operation.
215                           InitAckWait: begin
216                             // suppress any toggles on the ping line while we are in the init phase.
217        1/1                  send_ping = 1'b0;
           Tests:       T1 T2 T3 
218        1/1                  if (!alert_sigint) begin
           Tests:       T1 T2 T3 
219        1/1                    state_d = Pause0;
           Tests:       T1 T2 T3 
220                               // If we get a ping request in this cycle, or if we realize that there is an unhandled
221                               // ping request that came in during initialization (but after init_trig_i has been
222                               // deasserted), we signal this to the alert sender by toggling the request line.
223        1/1                    send_ping = ping_rise || ping_pending_q;
           Tests:       T1 T2 T3 
224                             end
                        MISSING_ELSE
225                           end
226                           default: state_d = Idle;
227                         endcase
228                     
229                         // once the initialization sequence has been triggered,
230                         // overrides are not allowed anymore until the initialization has been completed.
231        1/1              if (!(state_q inside {InitReq, InitAckWait})) begin
           Tests:       T1 T2 T3 
232                           // in this case, abort and jump into the initialization sequence
233        1/1                if (mubi4_test_true_strict(init_trig_i)) begin
           Tests:       T1 T2 T3 
234        1/1                  state_d      = InitReq;
           Tests:       T1 T2 T3 
235        1/1                  ack_pd       = 1'b0;
           Tests:       T1 T2 T3 
236        1/1                  ping_ok_o    = 1'b0;
           Tests:       T1 T2 T3 
237        1/1                  integ_fail_o = 1'b0;
           Tests:       T1 T2 T3 
238        1/1                  alert_o      = 1'b0;
           Tests:       T1 T2 T3 
239        1/1                  send_init    = 1'b1;
           Tests:       T1 T2 T3 
240                           // if we're not busy with an init request, we clamp down all outputs
241                           // and indicate an integrity failure.
242        1/1                end else if (alert_sigint) begin
           Tests:       T1 T2 T3 
243        1/1                  state_d      = Idle;
           Tests:       T1 T2 T3 
244        1/1                  ack_pd       = 1'b0;
           Tests:       T1 T2 T3 
245        1/1                  ping_ok_o    = 1'b0;
           Tests:       T1 T2 T3 
246        1/1                  integ_fail_o = 1'b1;
           Tests:       T1 T2 T3 
247        1/1                  alert_o      = 1'b0;
           Tests:       T1 T2 T3 
248                           end
                        MISSING_ELSE
249                         end
                        MISSING_ELSE
250                       end
251                     
252                       always_ff @(posedge clk_i or negedge rst_ni) begin : p_reg
253        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
254                           // Reset into the init request so that an alert handler reset implicitly
255                           // triggers an in-band reset of all alert channels.
256        1/1                state_q        <= InitReq;
           Tests:       T1 T2 T3 
257        1/1                ping_req_q     <= 1'b0;
           Tests:       T1 T2 T3 
258        1/1                ping_pending_q <= 1'b0;
           Tests:       T1 T2 T3 
259                         end else begin
260        1/1                state_q        <= state_d;
           Tests:       T1 T2 T3 
261        1/1                ping_req_q     <= ping_req_d;
           Tests:       T1 T2 T3 
262        1/1                ping_pending_q <= ping_pending_d;
           Tests:       T1 T2 T3 

---

Cond Coverage for Module : prim_alert_receiver

	Total	Covered	Percent
Conditions	19	19	100.00
Logical	19	19	100.00
Non-Logical	0	0
Event	0	0

 LINE       106
 EXPRESSION (ping_req_d && ((!ping_req_q)))
             -----1----    -------2-------

-1-	-2-	Status	Tests
0	1	Covered	T1,T2,T3
1	0	Covered	T1,T2,T3
1	1	Covered	T1,T2,T3

 LINE       107
 EXPRESSION (send_init ? 1'b0 : (send_ping ? ((~ping_tog_pq)) : ping_tog_pq))
             ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       107
 SUB-EXPRESSION (send_ping ? ((~ping_tog_pq)) : ping_tog_pq)
                 ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       111
 EXPRESSION (send_init ? ack_pd : ((~ack_pd)))
             ----1----

-1-	Status	Tests
0	Covered	T1,T2,T3
1	Covered	T1,T2,T3

 LINE       144
 EXPRESSION (ping_rise | (((~ping_ok_o)) & ping_req_i & ping_pending_q))
             ----1----   -----------------------2----------------------

-1-	-2-	Status	Tests
0	0	Covered	T1,T2,T3
0	1	Covered	T1,T2,T3
1	0	Covered	T1,T2,T3

 LINE       144
 SUB-EXPRESSION (((~ping_ok_o)) & ping_req_i & ping_pending_q)
                 -------1------   -----2----   -------3------

-1-	-2-	-3-	Status	Tests
0	1	1	Covered	T4,T5,T6
1	0	1	Covered	T2,T7,T8
1	1	0	Covered	T1,T2,T3
1	1	1	Covered	T1,T2,T3

 LINE       223
 EXPRESSION (ping_rise || ping_pending_q)
             ----1----    -------2------

-1-	-2-	Status	Tests
0	0	Covered	T1,T2,T3
0	1	Covered	T1,T2,T3
1	0	Covered	T9,T10,T11

---

Toggle Coverage for Module : prim_alert_receiver

	Total	Covered	Percent
Totals	13	13	100.00
Total Bits	32	32	100.00
Total Bits 0->1	16	16	100.00
Total Bits 1->0	16	16	100.00

Ports	13	13	100.00
Port Bits	32	32	100.00
Port Bits 0->1	16	16	100.00
Port Bits 1->0	16	16	100.00

Port Details

Name	Toggle	Toggle 1->0	Tests	Toggle 0->1	Tests	Direction
clk_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
rst_ni	Yes	Yes	T12,T13,T8	Yes	T1,T2,T3	INPUT
init_trig_i[3:0]	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
ping_req_i	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
ping_ok_o	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
integ_fail_o	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
alert_o	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
alert_rx_o.ack_n	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
alert_rx_o.ack_p	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
alert_rx_o.ping_n	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
alert_rx_o.ping_p	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	OUTPUT
alert_tx_i.alert_n	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT
alert_tx_i.alert_p	Yes	Yes	T1,T2,T3	Yes	T1,T2,T3	INPUT

---

FSM Coverage for Module : prim_alert_receiver

Summary for FSM :: state_q

	Total	Covered	Percent
States	6	6	100.00	(Not included in score)
Transitions	15	12	80.00
Sequences	0	0

State, Transition and Sequence Details for FSM :: state_q

---

states	Line No.	Covered	Tests
HsAckWait	172	Covered	T1,T2,T3
Idle	192	Covered	T1,T2,T3
InitAckWait	209	Covered	T1,T2,T3
InitReq	234	Covered	T1,T2,T3
Pause0	185	Covered	T1,T2,T3
Pause1	191	Covered	T1,T2,T3

transitions	Line No.	Covered	Tests
HsAckWait->Idle	243	Covered	T1,T2,T3
HsAckWait->InitReq	234	Covered	T1,T2,T14
HsAckWait->Pause0	185	Covered	T1,T2,T3
Idle->HsAckWait	172	Covered	T1,T2,T3
Idle->InitReq	234	Covered	T1,T2,T3
InitAckWait->Idle	243	Not Covered
InitAckWait->InitReq	234	Covered	T15,T5,T16
InitAckWait->Pause0	219	Covered	T1,T2,T3
InitReq->Idle	243	Not Covered
InitReq->InitAckWait	209	Covered	T1,T2,T3
Pause0->Idle	243	Not Covered
Pause0->InitReq	234	Covered	T2,T17,T12
Pause0->Pause1	191	Covered	T1,T2,T3
Pause1->Idle	192	Covered	T1,T2,T3
Pause1->InitReq	234	Covered	T17,T18,T19

---

Branch Coverage for Module : prim_alert_receiver

	Line No.	Total	Covered	Percent
Branches		24	23	95.83
TERNARY	107	3	3	100.00
TERNARY	111	2	2	100.00
CASE	168	13	12	92.31
IF	231	4	4	100.00
IF	253	2	2	100.00

107          assign ping_tog_pd = (send_init) ? 1'b0         :
                                              -1-  
                                              ==>  
108                               (send_ping) ? ~ping_tog_pq : ping_tog_pq;
                                              -2-  
                                              ==>  
                                              ==>  

Branches:

-1-	-2-	Status	Tests
1	-	Covered	T1,T2,T3
0	1	Covered	T1,T2,T3
0	0	Covered	T1,T2,T3

111          assign ack_dn      = (send_init) ? ack_pd : ~ack_pd;
                                              -1-  
                                              ==>  
                                              ==>  

Branches:

-1-	Status	Tests
1	Covered	T1,T2,T3
0	Covered	T1,T2,T3

168            unique case (state_q)
                      -1-  
169              Idle: begin
170                // wait for handshake to be initiated
171                if (alert_level) begin
                   -2-  
172                  state_d = HsAckWait;
173                  ack_pd  = 1'b1;
174                  // signal either an alert or ping received on the output
175                  if (ping_pending_q) begin
                     -3-  
176                    ping_ok_o = 1'b1;
                       ==>
177                  end else begin
178                    alert_o   = 1'b1;
                       ==>
179                  end
180                end
                   MISSING_ELSE
                   ==>
181              end
182              // waiting for deassertion of alert to complete HS
183              HsAckWait: begin
184                if (!alert_level) begin
                   -4-  
185                  state_d  = Pause0;
                     ==>
186                end else begin
187                  ack_pd = 1'b1;
                     ==>
188                end
189              end
190              // pause cycles between back-to-back handshakes
191              Pause0: state_d = Pause1;
                 ==>
192              Pause1: state_d = Idle;
                 ==>
193              // this state is only reached if an in-band reset is
194              // requested via the low-power logic.
195              InitReq: begin
196                // we deliberately place a sigint error on the ack and ping lines in this case.
197                send_init = 1'b1;
198                // suppress any toggles on the ping line while we are in the init phase.
199                send_ping = 1'b0;
200                // As long as init req is asserted, we remain in this state and acknowledge all incoming
201                // ping requests. As soon as the init request is dropped however, ping requests are not
202                // acked anymore such that the ping mechanism can also flag alert channels that got stuck
203                // in the initialization sequence.
204                if (mubi4_test_true_strict(init_trig_i)) begin
                   -5-  
205                  ping_ok_o = ping_pending_q;
                     ==>
206                // the sender will respond to the sigint error above with a sigint error on the alert lines.
207                // hence we treat the alert_sigint like an acknowledgement in this case.
208                end else if (alert_sigint) begin
                            -6-  
209                  state_d = InitAckWait;
                     ==>
210                end
                   MISSING_ELSE
                   ==>
211              end
212              // We get here if the sender has responded with alert_sigint, and init_trig_i==lc_ctrl_pkg::On
213              // has been deasserted. At this point, we need to wait for the alert_sigint to drop again
214              // before resuming normal operation.
215              InitAckWait: begin
216                // suppress any toggles on the ping line while we are in the init phase.
217                send_ping = 1'b0;
218                if (!alert_sigint) begin
                   -7-  
219                  state_d = Pause0;
                     ==>
220                  // If we get a ping request in this cycle, or if we realize that there is an unhandled
221                  // ping request that came in during initialization (but after init_trig_i has been
222                  // deasserted), we signal this to the alert sender by toggling the request line.
223                  send_ping = ping_rise || ping_pending_q;
224                end
                   MISSING_ELSE
                   ==>
225              end
226              default: state_d = Idle;
                 ==>

Branches:

-1-	-2-	-3-	-4-	-5-	-6-	-7-	Status	Tests
Idle	1	1	-	-	-	-	Covered	T1,T2,T3
Idle	1	0	-	-	-	-	Covered	T1,T2,T3
Idle	0	-	-	-	-	-	Covered	T1,T2,T3
HsAckWait	-	-	1	-	-	-	Covered	T1,T2,T3
HsAckWait	-	-	0	-	-	-	Covered	T1,T2,T3
Pause0	-	-	-	-	-	-	Covered	T1,T2,T3
Pause1	-	-	-	-	-	-	Covered	T1,T2,T3
InitReq	-	-	-	1	-	-	Covered	T1,T2,T3
InitReq	-	-	-	0	1	-	Covered	T1,T2,T3
InitReq	-	-	-	0	0	-	Covered	T1,T2,T3
InitAckWait	-	-	-	-	-	1	Covered	T1,T2,T3
InitAckWait	-	-	-	-	-	0	Covered	T1,T2,T3
default	-	-	-	-	-	-	Not Covered

231            if (!(state_q inside {InitReq, InitAckWait})) begin
               -1-  
232              // in this case, abort and jump into the initialization sequence
233              if (mubi4_test_true_strict(init_trig_i)) begin
                 -2-  
234                state_d      = InitReq;
                   ==>
235                ack_pd       = 1'b0;
236                ping_ok_o    = 1'b0;
237                integ_fail_o = 1'b0;
238                alert_o      = 1'b0;
239                send_init    = 1'b1;
240              // if we're not busy with an init request, we clamp down all outputs
241              // and indicate an integrity failure.
242              end else if (alert_sigint) begin
                          -3-  
243                state_d      = Idle;
                   ==>
244                ack_pd       = 1'b0;
245                ping_ok_o    = 1'b0;
246                integ_fail_o = 1'b1;
247                alert_o      = 1'b0;
248              end
                 MISSING_ELSE
                 ==>
249            end
               MISSING_ELSE
               ==>

Branches:

-1-	-2-	-3-	Status	Tests
1	1	-	Covered	T1,T2,T3
1	0	1	Covered	T1,T2,T3
1	0	0	Covered	T1,T2,T3
0	-	-	Covered	T1,T2,T3

253            if (!rst_ni) begin
               -1-  
254              // Reset into the init request so that an alert handler reset implicitly
255              // triggers an in-band reset of all alert channels.
256              state_q        <= InitReq;
                 ==>
257              ping_req_q     <= 1'b0;
258              ping_pending_q <= 1'b0;
259            end else begin
260              state_q        <= state_d;
                 ==>

Branches:

-1-	Status	Tests
1	Covered	T1,T2,T3
0	Covered	T1,T2,T3

---

Assert Coverage for Module : prim_alert_receiver

	Total	Attempted	Percent	Succeeded/Matched	Percent
Assertions	21	21	100.00	20	95.24
Cover properties	0	0		0
Cover sequences	0	0		0
Total	21	21	100.00	20	95.24

---

Assertion Details

Name	Attempts	Real Successes	Failures	Incomplete
AckDiffOk_A	149872	112803	0	156
AlertKnownO_A	150542	114433	0	0
InBandInitRequest_A	150542	4026	0	0
InBandInitSequence_A	150542	430	0	0
InitReq_A	150542	753	0	0
IntegFailKnownO_A	150542	114433	0	0
NoSpuriousAlertsDuringInit_A	150542	15757	0	0
NoSpuriousPingOksDuringInit_A	150542	15443	0	0
PingDiffOk_A	149686	113577	0	0
PingOkBypassDuringInit_A	150542	50	0	41
PingOkKnownO_A	150542	114433	0	0
PingPKnownO_A	150542	114433	0	0
PingPending_A	150542	815	0	119
PingRequest0_A	150542	0	0	0
PingResponse0_A	150542	763	0	0
gen_async_assert.Alert_A	76991	1280	0	0
gen_async_assert.PingResponse1_A	76991	314	0	0
gen_async_assert.SigInt_A	76991	239	0	81
gen_sync_assert.Alert_A	73551	3110	0	0
gen_sync_assert.PingResponse1_A	73551	345	0	0
gen_sync_assert.SigInt_A	73551	40	0	0

AckDiffOk_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	149872	112803	0	156
T1	1043	984	0	2
T2	1090	1017	0	2
T3	1039	950	0	2
T7	1055	956	0	2
T8	1166	1053	0	2
T12	1239	1074	0	2
T13	1220	1056	0	2
T14	1059	1000	0	2
T17	1080	1028	0	2
T20	1062	975	0	2

AlertKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	114433	0	0
T1	1056	999	0	0
T2	1105	1034	0	0
T3	1053	966	0	0
T7	1069	972	0	0
T8	1181	1070	0	0
T12	1252	1091	0	0
T13	1234	1074	0	0
T14	1075	1018	0	0
T17	1095	1045	0	0
T20	1076	991	0	0

InBandInitRequest_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	4026	0	0
T1	1056	29	0	0
T2	1105	47	0	0
T3	1053	36	0	0
T7	1069	52	0	0
T8	1181	68	0	0
T12	1252	82	0	0
T13	1234	66	0	0
T14	1075	67	0	0
T17	1095	50	0	0
T20	1076	40	0	0

InBandInitSequence_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	430	0	0
T2	1105	3	0	0
T3	1053	0	0	0
T7	1069	4	0	0
T8	1181	5	0	0
T12	1252	6	0	0
T13	1234	3	0	0
T14	1075	4	0	0
T17	1095	1	0	0
T18	1128	2	0	0
T20	1076	2	0	0
T21	0	2	0	0

InitReq_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	753	0	0
T1	1056	9	0	0
T2	1105	10	0	0
T3	1053	7	0	0
T7	1069	9	0	0
T8	1181	10	0	0
T12	1252	11	0	0
T13	1234	10	0	0
T14	1075	9	0	0
T17	1095	10	0	0
T20	1076	7	0	0

IntegFailKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	114433	0	0
T1	1056	999	0	0
T2	1105	1034	0	0
T3	1053	966	0	0
T7	1069	972	0	0
T8	1181	1070	0	0
T12	1252	1091	0	0
T13	1234	1074	0	0
T14	1075	1018	0	0
T17	1095	1045	0	0
T20	1076	991	0	0

NoSpuriousAlertsDuringInit_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	15757	0	0
T1	1056	176	0	0
T2	1105	201	0	0
T3	1053	143	0	0
T7	1069	172	0	0
T8	1181	199	0	0
T12	1252	234	0	0
T13	1234	209	0	0
T14	1075	181	0	0
T17	1095	202	0	0
T20	1076	141	0	0

NoSpuriousPingOksDuringInit_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	15443	0	0
T1	1056	160	0	0
T2	1105	185	0	0
T3	1053	125	0	0
T7	1069	168	0	0
T8	1181	198	0	0
T12	1252	230	0	0
T13	1234	207	0	0
T14	1075	170	0	0
T17	1095	198	0	0
T20	1076	139	0	0

PingDiffOk_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	149686	113577	0	0
T1	1043	986	0	0
T2	1089	1018	0	0
T3	1040	953	0	0
T7	1055	958	0	0
T8	1165	1054	0	0
T12	1236	1075	0	0
T13	1216	1056	0	0
T14	1061	1004	0	0
T17	1077	1027	0	0
T20	1063	978	0	0

PingOkBypassDuringInit_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	50	0	41
T3	1053	1	0	0
T7	1069	2	0	0
T8	1181	0	0	0
T9	0	0	0	1
T12	1252	0	0	0
T13	1234	0	0	0
T14	1075	0	0	0
T15	0	1	0	0
T17	1095	2	0	0
T18	1128	1	0	0
T20	1076	0	0	0
T21	1114	0	0	0
T22	0	1	0	0
T23	0	1	0	0
T24	0	1	0	0
T25	0	1	0	0
T26	0	2	0	0
T27	0	0	0	1
T28	0	0	0	1
T29	0	0	0	1
T30	0	0	0	1
T31	0	0	0	1
T32	0	0	0	1
T33	0	0	0	1
T34	0	0	0	1
T35	0	0	0	1

PingOkKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	114433	0	0
T1	1056	999	0	0
T2	1105	1034	0	0
T3	1053	966	0	0
T7	1069	972	0	0
T8	1181	1070	0	0
T12	1252	1091	0	0
T13	1234	1074	0	0
T14	1075	1018	0	0
T17	1095	1045	0	0
T20	1076	991	0	0

PingPKnownO_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	114433	0	0
T1	1056	999	0	0
T2	1105	1034	0	0
T3	1053	966	0	0
T7	1069	972	0	0
T8	1181	1070	0	0
T12	1252	1091	0	0
T13	1234	1074	0	0
T14	1075	1018	0	0
T17	1095	1045	0	0
T20	1076	991	0	0

PingPending_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	815	0	119
T1	1056	11	0	1
T2	1105	11	0	1
T3	1053	11	0	1
T7	1069	11	0	1
T8	1181	11	0	1
T12	1252	11	0	1
T13	1234	11	0	1
T14	1075	11	0	1
T17	1095	11	0	1
T20	1076	11	0	1

PingRequest0_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	0	0	0

PingResponse0_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	150542	763	0	0
T1	1056	10	0	0
T2	1105	9	0	0
T3	1053	10	0	0
T7	1069	8	0	0
T8	1181	9	0	0
T12	1252	10	0	0
T13	1234	10	0	0
T14	1075	10	0	0
T17	1095	10	0	0
T20	1076	10	0	0

gen_async_assert.Alert_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	76991	1280	0	0
T1	1056	7	0	0
T2	1105	8	0	0
T3	1053	9	0	0
T7	1069	8	0	0
T8	1181	8	0	0
T12	1252	7	0	0
T13	1234	5	0	0
T14	1075	6	0	0
T17	1095	9	0	0
T20	1076	8	0	0

gen_async_assert.PingResponse1_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	76991	314	0	0
T1	1056	9	0	0
T2	1105	8	0	0
T3	1053	7	0	0
T7	1069	6	0	0
T8	1181	9	0	0
T12	1252	8	0	0
T13	1234	9	0	0
T14	1075	9	0	0
T17	1095	7	0	0
T20	1076	9	0	0

gen_async_assert.SigInt_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	76991	239	0	81
T1	1056	5	0	2
T2	1105	5	0	3
T3	1053	6	0	2
T7	1069	5	0	2
T8	1181	7	0	3
T12	1252	5	0	2
T13	1234	6	0	3
T14	1075	8	0	2
T17	1095	5	0	3
T20	1076	5	0	2

gen_sync_assert.Alert_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	73551	3110	0	0
T28	835	9	0	0
T29	905	10	0	0
T30	927	11	0	0
T31	909	7	0	0
T32	939	6	0	0
T36	992	8	0	0
T37	888	8	0	0
T38	956	8	0	0
T39	915	8	0	0
T40	1007	7	0	0

gen_sync_assert.PingResponse1_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	73551	345	0	0
T28	835	9	0	0
T29	905	9	0	0
T30	927	7	0	0
T31	909	9	0	0
T32	939	7	0	0
T36	992	10	0	0
T37	888	10	0	0
T38	956	8	0	0
T39	915	10	0	0
T40	1007	9	0	0

gen_sync_assert.SigInt_A

Name	Attempts	Real Successes	Failures	Incomplete
Total	73551	40	0	0
T28	835	1	0	0
T29	905	1	0	0
T30	927	1	0	0
T31	909	1	0	0
T32	939	1	0	0
T36	992	1	0	0
T37	888	1	0	0
T38	956	1	0	0
T39	915	1	0	0
T40	1007	1	0	0