Unified Coverage Report :: Module

Line Coverage for Module : sha3pad

	Line No.	Total	Covered	Percent
TOTAL		162	161	99.38
ALWAYS	157	6	6	100.00
CONT_ASSIGN	209	1	1	100.00
CONT_ASSIGN	213	1	1	100.00
CONT_ASSIGN	236	1	1	100.00
CONT_ASSIGN	242	1	1	100.00
CONT_ASSIGN	247	1	1	100.00
CONT_ASSIGN	257	1	1	100.00
ALWAYS	267	6	6	100.00
ALWAYS	279	3	3	100.00
CONT_ASSIGN	286	1	1	100.00
ALWAYS	293	3	3	100.00
ALWAYS	298	76	75	98.68
CONT_ASSIGN	509	1	1	100.00
CONT_ASSIGN	520	1	1	100.00
CONT_ASSIGN	541	1	1	100.00
ALWAYS	558	4	4	100.00
CONT_ASSIGN	581	1	1	100.00
CONT_ASSIGN	588	1	1	100.00
ALWAYS	591	5	5	100.00
ALWAYS	603	5	5	100.00
ALWAYS	615	5	5	100.00
ALWAYS	664	10	10	100.00
ALWAYS	719	9	9	100.00
ALWAYS	779	6	6	100.00
ALWAYS	788	6	6	100.00
ALWAYS	798	6	6	100.00



156                       always_comb begin
157        1/1              unique case (strength_i)
           Tests:       T1 T2 T3 
158        1/1                L128: block_addr_limit = KeccakCountW'(KeccakRate[L128]);
           Tests:       T1 T2 T3 
159        1/1                L224: block_addr_limit = KeccakCountW'(KeccakRate[L224]);
           Tests:       T16 T62 T82 
160        1/1                L256: block_addr_limit = KeccakCountW'(KeccakRate[L256]);
           Tests:       T1 T2 T3 
161        1/1                L384: block_addr_limit = KeccakCountW'(KeccakRate[L384]);
           Tests:       T3 T13 T18 
162        1/1                L512: block_addr_limit = KeccakCountW'(KeccakRate[L512]);
           Tests:       T17 T62 T82 
163                     
164                           default: block_addr_limit = '0;
165                         endcase
166                       end
167                     
168                       /////////////////////
169                       // Control Signals //
170                       /////////////////////
171                     
172                       // `sel_mux` selects the output data among the incoming or internally generated data.
173                       // MuxFifo:    data from external (msg_data_i)
174                       // MuxPrefix:  bytepad(encode_string(N)||encode_string(S), )
175                       // MuxFuncPad: function_pad with end of message
176                       // MuxZeroEnd: all 0
177                       mux_sel_e sel_mux;
178                     
179                       // `sent_message` indicates the number of entries sent to keccak round per
180                       // block. The value shall be enough to cover Maximum entry of the Keccak
181                       // storage as defined in sha3_pkg, `$clog2(KeccakEntries+1)`. Logically,
182                       // it is not needed to have more than KeccakEntries but for safety in case of
183                       // SHA3 context switch resuming the SHA3 from the middle of sponge
184                       // construction. If needed, the software should be able to write whole 1600
185                       // bits. The `sent_message` is used to check sent_blocksize.
186                       logic [KeccakCountW-1:0] sent_message;
187                       logic inc_sentmsg, clr_sentmsg;
188                     
189                       // This primitive is used to place a hardened counter
190                       // SEC_CM: CTR.REDUN
191                       prim_count #(
192                         .Width(KeccakCountW)
193                       ) u_sentmsg_count (
194                         .clk_i,
195                         .rst_ni,
196                         .clr_i(clr_sentmsg),
197                         .set_i(1'b0),
198                         .set_cnt_i(KeccakCountW'(0)),
199                         .incr_en_i(inc_sentmsg),
200                         .decr_en_i(1'b0),
201                         .step_i(KeccakCountW'(1)),
202                         .commit_i(1'b1),
203                         .cnt_o(sent_message),
204                         .cnt_after_commit_o(),
205                         .err_o(msg_count_error_o)
206                       );
207                     
208                     
209        1/1            assign inc_sentmsg = keccak_valid_o & keccak_ready_i ;
           Tests:       T1 T2 T3 
210                     
211                       // Prefix index to slice the `prefix` n-bits into multiple of 64bit.
212                       logic [KeccakMsgAddrW-1:0] prefix_index;
213        1/1            assign prefix_index = (sent_message < block_addr_limit) ? sent_message : '0;
           Tests:       T1 T2 T3 
214                     
215                       // fsm_keccak_valid is an output signal from FSM which to send data generated
216                       // inside the pad logic to keccak_round
217                       logic fsm_keccak_valid;
218                     
219                       // hold_msg to prevent message from being forwarded into keccak_round and
220                       // acked. Mainly the usage is to hold the message and initiates the
221                       // keccak_round for current block.
222                       logic hold_msg;
223                     
224                       // latch the partial write. Latched data is used for funcpad_merged
225                       logic en_msgbuf;
226                       logic clr_msgbuf;
227                     
228                       ///////////////////
229                       // State Machine //
230                       ///////////////////
231                     
232                       // Inputs
233                     
234                       // FSM moves to StPrefix only when cSHAKE is enabled
235                       logic mode_eq_cshake;
236        1/1            assign mode_eq_cshake = (mode_i == CShake) ? 1'b 1 : 1'b 0;
           Tests:       T1 T2 T3 
237                     
238                       // `sent_blocksize` indicates the pad logic pushed block size data into
239                       // keccak round logic.
240                       logic sent_blocksize;
241                     
242        1/1            assign sent_blocksize = (sent_message == block_addr_limit) ? 1'b 1 : 1'b 0;
           Tests:       T1 T2 T3 
243                     
244                       // `keccak_ack` indicates the request is accepted in keccak_round
245                       logic keccak_ack;
246                     
247        1/1            assign keccak_ack = keccak_valid_o & keccak_ready_i ;
           Tests:       T1 T2 T3 
248                     
249                       // msg_partial indicates the incoming message is partial write or not.
250                       // This is used to check if the incoming message need to be latched inside or
251                       // not. If no partial message is at the end, msg_buf doesn't have to latch
252                       // msg_data_i. It is assumed that the partial message is permitted only at
253                       // the end of the message. So if (msg_valid_i && msg_partial && msg_ready_o),
254                       // there will be no msg_valid_i till process_latched.
255                       // Shall be used with msg_valid_i together.
256                       logic msg_partial;
257        1/1            assign msg_partial = (&msg_strb_i != 1'b 1);
           Tests:       T1 T2 T3 
258                     
259                     
260                       // `process_latched` latches the `process_i` input before it is seen in the
261                       // FSM. `process_i` may follow `start_i` too fast so that the FSM may not
262                       // see it fast enought in case of cSHAKE mode. cSHAKE needs to process the
263                       // prefix prior to see the process indicator.
264                       logic process_latched;
265                     
266                       always_ff @(posedge clk_i or negedge rst_ni) begin
267        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
268        1/1                process_latched <= 1'b 0;
           Tests:       T1 T2 T3 
269        1/1              end else if (process_i) begin
           Tests:       T1 T2 T3 
270        1/1                process_latched <= 1'b 1;
           Tests:       T1 T2 T3 
271        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
           Tests:       T1 T2 T3 
272        1/1                process_latched <= 1'b0;
           Tests:       T1 T2 T3 
273                         end
                        MISSING_ELSE
274                       end
275                     
276                       // State Register ===========================================================
277                       pad_st_e st, st_d;
278                     
279        3/3            `PRIM_FLOP_SPARSE_FSM(u_state_regs, st_d, st, pad_st_e, StPadIdle)
           Tests:       T1 T2 T3  | T1 T2 T3  | T1 T2 T3 
PRIM_FLOP_SPARSE_FSM(u_state_regs, st_d, st, pad_st_e, StPadIdle):
279.1                   `ifdef SIMULATION                                   
279.2                       prim_sparse_fsm_flop #(                           
279.3                         .StateEnumT(pad_st_e),                            
279.4                         .Width($bits(pad_st_e)),                          
279.5                         .ResetValue($bits(pad_st_e)'(StPadIdle)),          
279.6                         .EnableAlertTriggerSVA(1), 
279.7                         .CustomForceName("st")          
279.8                       ) u_state_regs (                                        
279.9                         .clk_i   ( clk_i   ),                           
279.10                        .rst_ni  ( rst_ni ),                           
279.11                        .state_i ( st_d     ),                           
279.12                        .state_o (         )                            
279.13                      );                                                
279.14                      always_ff @(posedge clk_i or negedge rst_ni) begin 
279.15     1/1              if (!rst_ni) begin                               
           Tests:       T1 T2 T3 
279.16     1/1                st <= StPadIdle;                                
           Tests:       T1 T2 T3 
279.17                      end else begin                                    
279.18     1/1                st <= st_d;                                     
           Tests:       T1 T2 T3 
279.19                      end                                               
279.20                    end  
279.21                      u_state_regs_A: assert property (@(posedge clk_i) disable iff ((!rst_ni) !== '0) (st === u_state_regs.state_o))       
279.22                      else begin                                                                           
279.23                        `ifdef UVM                                                                               
279.24                    uvm_pkg::uvm_report_error("ASSERT FAILED", "u_state_regs_A", uvm_pkg::UVM_NONE, 
279.25                                              "../src/lowrisc_ip_sha3_0.1/rtl/sha3pad.sv", 279, "", 1);                                
279.26                  `else                                                                                    
279.27                    $error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__,         
279.28                           `PRIM_STRINGIFY(u_state_regs_A));                                                       
279.29                  `endif                                                              
279.30                      end 
279.31                    `else                                               
279.32                      prim_sparse_fsm_flop #(                           
279.33                        .StateEnumT(pad_st_e),                            
279.34                        .Width($bits(pad_st_e)),                          
279.35                        .ResetValue($bits(pad_st_e)'(StPadIdle)),          
279.36                        .EnableAlertTriggerSVA(1)  
279.37                      ) u_state_regs (                                        
279.38                        .clk_i   ( `PRIM_FLOP_CLK   ),                           
279.39                        .rst_ni  ( `PRIM_FLOP_RST ),                           
279.40                        .state_i ( st_d     ),                           
279.41                        .state_o ( st     )                            
279.42                      );                                                
279.43                    `endif280                     
281                       // `end_of_block` indicates current beat is end of the block
282                       // It shall set when the address reaches to the end of the block. End address
283                       // is set by the strength_i, which is `block_addr_limit`.
284                       logic end_of_block;
285                     
286        1/1            assign end_of_block = ((sent_message + 1'b1) == block_addr_limit) ? 1'b 1 : 1'b 0;
           Tests:       T1 T2 T3 
287                     
288                     
289                       // Next logic and output logic ==============================================
290                       // SEC_CM: ABSORBED.CTRL.MUBI
291                       prim_mubi_pkg::mubi4_t absorbed_d;
292                       always_ff @(posedge clk_i or negedge rst_ni) begin
293        2/2              if (!rst_ni) absorbed_o <= prim_mubi_pkg::MuBi4False;
           Tests:       T1 T2 T3  | T1 T2 T3 
294        1/1              else         absorbed_o <= absorbed_d;
           Tests:       T1 T2 T3 
295                       end
296                     
297                       always_comb begin
298        1/1              st_d = st;
           Tests:       T1 T2 T3 
299                     
300                         // FSM output : default values
301        1/1              keccak_run_o = 1'b 0;
           Tests:       T1 T2 T3 
302        1/1              sel_mux      = MuxNone;
           Tests:       T1 T2 T3 
303                     
304        1/1              fsm_keccak_valid = 1'b 0;
           Tests:       T1 T2 T3 
305                     
306        1/1              hold_msg = 1'b 0;
           Tests:       T1 T2 T3 
307        1/1              clr_sentmsg = 1'b 0;
           Tests:       T1 T2 T3 
308                     
309        1/1              en_msgbuf = 1'b 0;
           Tests:       T1 T2 T3 
310        1/1              clr_msgbuf = 1'b 0;
           Tests:       T1 T2 T3 
311                     
312        1/1              absorbed_d = prim_mubi_pkg::MuBi4False;
           Tests:       T1 T2 T3 
313                     
314        1/1              sparse_fsm_error_o = 1'b 0;
           Tests:       T1 T2 T3 
315                     
316        1/1              unique case (st)
           Tests:       T1 T2 T3 
317                     
318                           // In Idle state, the FSM checks if the software (or upper FSM) initiates
319                           // the hash process. If `start_i` is asserted (assume it is pulse), FSM
320                           // starts to push the data into the keccak round logic. Depending on the
321                           // hashing mode, FSM may push additional prefex in front of the actual
322                           // message. It means, the message could be back-pressured until the first
323                           // prefix is processed.
324                           StPadIdle: begin
325        1/1                  if (start_i) begin
           Tests:       T1 T2 T3 
326                               // If cSHAKE, move to Prefix state
327        1/1                    if (mode_eq_cshake) begin
           Tests:       T1 T2 T3 
328        1/1                      st_d = StPrefix;
           Tests:       T1 T2 T3 
329                               end else begin
330        1/1                      st_d = StMessage;
           Tests:       T4 T13 T16 
331                               end
332                             end else begin
333        1/1                    st_d = StPadIdle;
           Tests:       T1 T2 T3 
334                             end
335                           end
336                     
337                           // At Prefix state, FSM pushes
338                           // `bytepad(encode_string(N)||encode_string(S), 168or136)`. The software
339                           // already prepared `encode_string(N) || encode_string(S)` in the regs.
340                           // So, the FSM adds 2Byte in front of ns_data_i, which is an encoded
341                           // block size (see `encoded_bytepad` below)
342                           // After pushing the prefix, it initiates the hash process and move to
343                           // Message state.
344                           StPrefix: begin
345        1/1                  sel_mux = MuxPrefix;
           Tests:       T1 T2 T3 
346                     
347        1/1                  if (sent_blocksize) begin
           Tests:       T1 T2 T3 
348        1/1                    st_d = StPrefixWait;
           Tests:       T1 T2 T3 
349                     
350        1/1                    keccak_run_o = 1'b 1;
           Tests:       T1 T2 T3 
351        1/1                    fsm_keccak_valid = 1'b 0;
           Tests:       T1 T2 T3 
352        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
353                             end else begin
354        1/1                    st_d = StPrefix;
           Tests:       T1 T2 T3 
355                     
356        1/1                    fsm_keccak_valid = 1'b 1;
           Tests:       T1 T2 T3 
357                             end
358                           end
359                     
360                           StPrefixWait: begin
361        1/1                  sel_mux = MuxPrefix;
           Tests:       T1 T2 T3 
362                     
363        1/1                  if (keccak_complete_i) begin
           Tests:       T1 T2 T3 
364        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
365                             end else begin
366        1/1                    st_d = StPrefixWait;
           Tests:       T1 T2 T3 
367                             end
368                           end
369                     
370                           // Message state pushes the incoming message into keccak round logic.
371                           // It forwards the message while counting the data and if it reaches
372                           // the block size, it triggers the keccak round to run. If `process` is
373                           // set, it moves to Pad state.
374                           StMessage: begin
375        1/1                  sel_mux = MuxFifo;
           Tests:       T1 T2 T3 
376                     
377        1/1                  if (msg_valid_i && msg_partial) begin
           Tests:       T1 T2 T3 
378        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
379                     
380        1/1                    en_msgbuf = 1'b 1;
           Tests:       T1 T2 T3 
381        1/1                  end else if (sent_blocksize) begin
           Tests:       T1 T2 T3 
382                               // Check block completion first even process is set.
383        1/1                    st_d = StMessageWait;
           Tests:       T1 T2 T3 
384                     
385        1/1                    keccak_run_o = 1'b 1;
           Tests:       T1 T2 T3 
386        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
387        1/1                    hold_msg = 1'b 1;
           Tests:       T1 T2 T3 
388        1/1                  end else if (process_latched || process_i) begin
           Tests:       T1 T2 T3 
389        1/1                    st_d = StPad;
           Tests:       T1 T2 T3 
390                     
391                               // Not asserting the msg_ready_o
392        1/1                    hold_msg = 1'b 1;
           Tests:       T1 T2 T3 
393                             end else begin
394        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
395                     
396                             end
397                           end
398                     
399                           StMessageWait: begin
400        1/1                  hold_msg = 1'b 1;
           Tests:       T1 T2 T3 
401                     
402        1/1                  if (keccak_complete_i) begin
           Tests:       T1 T2 T3 
403        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
404                             end else begin
405        1/1                    st_d = StMessageWait;
           Tests:       T1 T2 T3 
406                             end
407                           end
408                     
409                           // Pad state just pushes the ending suffix. Depending on the mode, the
410                           // padding value is unique. SHA3 adds 2'b10, SHAKE adds 4'b1111, and
411                           // cSHAKE adds 2'b 00. Refer `function_pad`. The signal has one more bit
412                           // defined to accomodate first 1 bit of `pad10*1()` function.
413                           StPad: begin
414        1/1                  sel_mux = MuxFuncPad;
           Tests:       T1 T2 T3 
415                     
416        1/1                  fsm_keccak_valid = 1'b 1;
           Tests:       T1 T2 T3 
417                     
418        1/1                  if (keccak_ack && end_of_block) begin
           Tests:       T1 T2 T3 
419                               // If padding is the last block, don't have to move to StPad01, just
420                               // run Keccak and complete
421        1/1                    st_d = StPadRun;
           Tests:       T13 T17 T18 
422                     
423                               // always clear the latched msgbuf
424        1/1                    clr_msgbuf = 1'b 1;
           Tests:       T13 T17 T18 
425        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T13 T17 T18 
426        1/1                  end else if (keccak_ack) begin
           Tests:       T1 T2 T3 
427        1/1                    st_d = StPad01;
           Tests:       T1 T2 T3 
428        1/1                    clr_msgbuf = 1'b 1;
           Tests:       T1 T2 T3 
429                             end else begin
430        0/1     ==>            st_d = StPad;
431                             end
432                           end
433                     
434                           StPadRun: begin
435        1/1                  st_d = StPadFlush;
           Tests:       T13 T17 T18 
436                     
437        1/1                  keccak_run_o = 1'b 1;
           Tests:       T13 T17 T18 
438        1/1                  clr_sentmsg = 1'b 1;
           Tests:       T13 T17 T18 
439                           end
440                     
441                           // Pad01 pushes the end bit of pad10*1() function. As keccak accepts byte
442                           // size only, StPad always pushes partial (5bits). So at this state, it
443                           // pushes rest of 3bits. If the data pushed in StPad is the last byte of
444                           // the block, then Pad01 pushes to the same byte, if not, it first
445                           // zero-fill the block then pad 1 to the end.
446                           StPad01: begin
447        1/1                  sel_mux = MuxZeroEnd;
           Tests:       T1 T2 T3 
448                     
449                             // There's no chance StPad01 can be a start of the block. So can be
450                             // discard that the sent_blocksize is set at the beginning.
451        1/1                  if (sent_blocksize) begin
           Tests:       T1 T2 T3 
452        1/1                    st_d = StPadFlush;
           Tests:       T1 T2 T3 
453                     
454        1/1                    fsm_keccak_valid = 1'b 0;
           Tests:       T1 T2 T3 
455        1/1                    keccak_run_o = 1'b 1;
           Tests:       T1 T2 T3 
456        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
457                             end else begin
458        1/1                    st_d = StPad01;
           Tests:       T1 T2 T3 
459                     
460        1/1                    fsm_keccak_valid = 1'b 1;
           Tests:       T1 T2 T3 
461                             end
462                           end
463                     
464                           StPadFlush: begin
465                             // Wait completion from keccak_round or wait SW indicator.
466        1/1                  clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
467        1/1                  clr_msgbuf = 1'b 1;
           Tests:       T1 T2 T3 
468                     
469        1/1                  if (keccak_complete_i) begin
           Tests:       T1 T2 T3 
470        1/1                    st_d = StPadIdle;
           Tests:       T1 T2 T3 
471                     
472        1/1                    absorbed_d = prim_mubi_pkg::MuBi4True;
           Tests:       T1 T2 T3 
473                             end else begin
474        1/1                    st_d = StPadFlush;
           Tests:       T1 T2 T3 
475                             end
476                           end
477                     
478                           StTerminalError: begin
479                             // this state is terminal
480        1/1                  st_d = st;
           Tests:       T4 T5 T6 
481        1/1                  sparse_fsm_error_o = 1'b 1;
           Tests:       T4 T5 T6 
482                           end
483                     
484                           default: begin
485                             // this state is terminal
486                             st_d = StTerminalError;
487                             sparse_fsm_error_o = 1'b 1;
488                           end
489                         endcase
490                     
491                         // SEC_CM: FSM.GLOBAL_ESC, FSM.LOCAL_ESC
492                         // Unconditionally jump into the terminal error state
493                         // if the life cycle controller triggers an escalation.
494        1/1              if (lc_ctrl_pkg::lc_tx_test_true_loose(lc_escalate_en_i)) begin
           Tests:       T1 T2 T3 
495        1/1                st_d = StTerminalError;
           Tests:       T4 T5 T6 
496                         end
                        MISSING_ELSE
497                       end
498                     
499                       //////////////
500                       // Datapath //
501                       //////////////
502                     
503                       // `encode_bytepad` represents the first two bytes of bytepad()
504                       // It depends on the block size. We can reuse KeccakRate
505                       // 10000000 || 00010101 // 168
506                       // 10000000 || 00010001 // 136
507                       logic [15:0] encode_bytepad;
508                     
509        1/1            assign encode_bytepad = encode_bytepad_len(strength_i);
           Tests:       T1 T2 T3 
510                     
511                       // Prefix size ==============================================================
512                       // Prefix represents bytepad(encode_string(N) || encode_string(S), 168 or 136)
513                       // encode_string(N) || encode_string(S) is prepared by the software and given
514                       // through `ns_data_i`. The first part of bytepad is determined by the
515                       // `strength_i` and stored into `encode_bytepad`.
516                     
517                       // It is assumed that the prefix always smaller than the block size.
518                       logic [PrefixSize*8-1:0] prefix;
519                     
520        1/1            assign prefix = {ns_data_i, encode_bytepad};
           Tests:       T1 T2 T3 
521                     
522                       logic [MsgWidth-1:0] prefix_sliced;
523                       logic [MsgWidth-1:0] prefix_data [Share];
524                     
525                       prim_slicer #(
526                         .InW (PrefixSize*8),
527                         .IndexW(KeccakMsgAddrW),
528                         .OutW(MsgWidth)
529                       ) u_prefix_slicer (
530                         .sel_i  (prefix_index),
531                         .data_i (prefix),
532                         .data_o (prefix_sliced)
533                       );
534                     
535                       if (EnMasking) begin : gen_prefix_masked
536                         // If Masking is enabled, prefix is two share.
537                         assign prefix_data[0] = '0;
538                         assign prefix_data[1] = prefix_sliced;
539                       end else begin : gen_prefix_unmasked
540                         // If Unmasked, only one share exists.
541        1/1              assign prefix_data[0] = prefix_sliced;
           Tests:       T1 T2 T3 
542                       end
543                     
544                       // ==========================================================================
545                       // function_pad is the unique value padded at the end of the message based on
546                       // the function among SHA3, SHAKE, cSHAKE. The standard mentioned that SHA3
547                       // pads `01` , SHAKE pads `1111`, and cSHAKE pads `00`.
548                       //
549                       // Then pad10*1() function follows. It adds `1` first then fill 0 until it
550                       // reaches the block size -1, then adds `1`.
551                       //
552                       // It means always `1` is followed by the function pad.
553                       logic [4:0] funcpad;
554                     
555                       logic [MsgWidth-1:0] funcpad_data [Share];
556                     
557                       always_comb begin
558        1/1              unique case (mode_i)
           Tests:       T1 T2 T3 
559        1/1                Sha3:   funcpad = 5'b 00110;
           Tests:       T1 T2 T3 
560        1/1                Shake:  funcpad = 5'b 11111;
           Tests:       T4 T15 T16 
561        1/1                CShake: funcpad = 5'b 00100;
           Tests:       T1 T2 T3 
562                     
563                           default: begin
564                             // Just create non-padding but pad10*1 only
565                             funcpad = 5'b 00001;
566                           end
567                         endcase
568                       end
569                     
570                       // ==========================================================================
571                       // `zero_with_endbit` contains all zero unless the message is for the last
572                       // MsgWidth beat in the block. If it is the end of the block, the last bit
573                       // will be set to complete pad10*1() functionality.
574                       logic [MsgWidth-1:0] zero_with_endbit [Share];
575                     
576                       if (EnMasking) begin : gen_zeroend_masked
577                         assign zero_with_endbit[0]               = '0;
578                         assign zero_with_endbit[1][MsgWidth-1]   = end_of_block;
579                         assign zero_with_endbit[1][MsgWidth-2:0] = '0;
580                       end else begin : gen_zeroend_unmasked
581        1/1              assign zero_with_endbit[0][MsgWidth-1]   = end_of_block;
           Tests:       T1 T2 T3 
582                         assign zero_with_endbit[0][MsgWidth-2:0] = '0;
583                       end
584                     
585                       // ==========================================================================
586                       // Data mux for output data
587                     
588        1/1            assign keccak_addr_o = (sent_message < block_addr_limit) ? sent_message : '0;
           Tests:       T1 T2 T3 
589                     
590                       always_comb begin
591        1/1              unique case (sel_mux)
           Tests:       T1 T2 T3 
592        1/1                MuxFifo:    keccak_data_o = msg_data_i;
           Tests:       T1 T2 T3 
593        1/1                MuxPrefix:  keccak_data_o = prefix_data;
           Tests:       T1 T2 T3 
594        1/1                MuxFuncPad: keccak_data_o = funcpad_data;
           Tests:       T1 T2 T3 
595        1/1                MuxZeroEnd: keccak_data_o = zero_with_endbit;
           Tests:       T1 T2 T3 
596                     
597                           // MuxNone
598                           default:  keccak_data_o = '{default:'0};
599                         endcase
600                       end
601                     
602                       always_comb begin
603        1/1              unique case (sel_mux)
           Tests:       T1 T2 T3 
604        1/1                MuxFifo:    keccak_valid_o = msg_valid_i & ~hold_msg & ~en_msgbuf;
           Tests:       T1 T2 T3 
605        1/1                MuxPrefix:  keccak_valid_o = fsm_keccak_valid;
           Tests:       T1 T2 T3 
606        1/1                MuxFuncPad: keccak_valid_o = fsm_keccak_valid;
           Tests:       T1 T2 T3 
607        1/1                MuxZeroEnd: keccak_valid_o = fsm_keccak_valid;
           Tests:       T1 T2 T3 
608                     
609                           // MuxNone
610                           default:  keccak_valid_o = 1'b 0;
611                         endcase
612                       end
613                     
614                       always_comb begin
615        1/1              unique case (sel_mux)
           Tests:       T1 T2 T3 
616        1/1                MuxFifo:    msg_ready_o = en_msgbuf | (keccak_ready_i & ~hold_msg);
           Tests:       T1 T2 T3 
617        1/1                MuxPrefix:  msg_ready_o = 1'b 0;
           Tests:       T1 T2 T3 
618        1/1                MuxFuncPad: msg_ready_o = 1'b 0;
           Tests:       T1 T2 T3 
619        1/1                MuxZeroEnd: msg_ready_o = 1'b 0;
           Tests:       T1 T2 T3 
620                     
621                           // MuxNone
622                           default: msg_ready_o = 1'b 0;
623                         endcase
624                       end
625                     
626                       // prim_packer : packing to 64bit to update keccak storage
627                       // two prim_packer in this module are used to pack the data received from
628                       // upper layer (KMAC core) and also the 5bit padding bits.
629                       // It is assumed that the message from upper layer could be partial at the
630                       // end of the message. Then the 2 or 4bit padding is required. It can be
631                       // handled by some custom logic or could be done by prim_packer.
632                       // If packer is used, the MSG_FIFO doesn't have to have another prim_packer
633                       // in front of the FIFO. This logic can handle the partial writes from the
634                       // software.
635                       //
636                       // If a custom logic is implemented here, prim_packer is necessary in front
637                       // of the FIFO, as this logic only appends at the end of the message when
638                       // `process_i` is asserted. Also, in this case, even prim_packer is not
639                       // needed, still 64bit registers to latch the partial write is required.
640                       // If not, the logic has to delay the acceptance of the incoming write
641                       // accesses. It may trigger the back-pressuring in some case which may result
642                       // that the software(or upper layer) may not set process_i.
643                       //
644                       // For custom logic, it could be implemented by the 8 mux selection.
645                       // for instance: (subject to be changed)
646                       //   unique case (sent_byte[2:0]) // generated from msg_strb_i
647                       //     3'b 000: funcpad_merged = {end_of_block, 63'(function_pad)                  };
648                       //     3'b 001: funcpad_merged = {end_of_block, 55'(function_pad), msg_data_i[ 7:0]};
649                       //     3'b 010: funcpad_merged = {end_of_block, 47'(function_pad), msg_data_i[15:0]};
650                       //     3'b 011: funcpad_merged = {end_of_block, 39'(function_pad), msg_data_i[23:0]};
651                       //     3'b 100: funcpad_merged = {end_of_block, 31'(function_pad), msg_data_i[31:0]};
652                       //     3'b 101: funcpad_merged = {end_of_block, 23'(function_pad), msg_data_i[39:0]};
653                       //     3'b 110: funcpad_merged = {end_of_block, 15'(function_pad), msg_data_i[47:0]};
654                       //     3'b 111: funcpad_merged = {end_of_block,  7'(function_pad), msg_data_i[55:0]};
655                       //     default: funcpad_merged = '0;
656                       //   endcase
657                     
658                       // internal buffer to store partial write. It doesn't have to store last byte as it
659                       // stores only when partial write.
660                       logic [MsgWidth-8-1:0] msg_buf [Share];
661                       logic [MsgStrbW-1-1:0] msg_strb;
662                     
663                       always_ff @(posedge clk_i or negedge rst_ni) begin
664        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
665        1/1                msg_buf  <= '{default:'0};
           Tests:       T1 T2 T3 
666        1/1                msg_strb <= '0;
           Tests:       T1 T2 T3 
667        1/1              end else if (en_msgbuf) begin
           Tests:       T1 T2 T3 
668        1/1                for (int i = 0 ; i < Share ; i++) begin
           Tests:       T1 T2 T3 
669        1/1                  msg_buf[i]  <= msg_data_i[i][0+:(MsgWidth-8)];
           Tests:       T1 T2 T3 
670                           end
671        1/1                msg_strb <= msg_strb_i[0+:(MsgStrbW-1)];
           Tests:       T1 T2 T3 
672        1/1              end else if (clr_msgbuf) begin
           Tests:       T1 T2 T3 
673        1/1                msg_buf  <= '{default:'0};
           Tests:       T1 T2 T3 
674        1/1                msg_strb <= '0;
           Tests:       T1 T2 T3 
675                         end
                        MISSING_ELSE
676                       end
677                     
678                       if (EnMasking) begin : gen_funcpad_data_masked
679                         always_comb begin
680                           unique case (msg_strb)
681                             7'b 000_0000: begin
682                               funcpad_data[0] = '0;
683                               funcpad_data[1] = {end_of_block, 63'(funcpad)                  };
684                             end
685                             7'b 000_0001: begin
686                               funcpad_data[0] = {56'h0,                      msg_buf[0][ 7:0]};
687                               funcpad_data[1] = {end_of_block, 55'(funcpad), msg_buf[1][ 7:0]};
688                             end
689                             7'b 000_0011: begin
690                               funcpad_data[0] = {48'h0,                      msg_buf[0][15:0]};
691                               funcpad_data[1] = {end_of_block, 47'(funcpad), msg_buf[1][15:0]};
692                             end
693                             7'b 000_0111: begin
694                               funcpad_data[0] = {40'h0,                      msg_buf[0][23:0]};
695                               funcpad_data[1] = {end_of_block, 39'(funcpad), msg_buf[1][23:0]};
696                             end
697                             7'b 000_1111: begin
698                               funcpad_data[0] = {32'h0,                      msg_buf[0][31:0]};
699                               funcpad_data[1] = {end_of_block, 31'(funcpad), msg_buf[1][31:0]};
700                             end
701                             7'b 001_1111: begin
702                               funcpad_data[0] = {24'h0,                      msg_buf[0][39:0]};
703                               funcpad_data[1] = {end_of_block, 23'(funcpad), msg_buf[1][39:0]};
704                             end
705                             7'b 011_1111: begin
706                               funcpad_data[0] = {16'h0,                      msg_buf[0][47:0]};
707                               funcpad_data[1] = {end_of_block, 15'(funcpad), msg_buf[1][47:0]};
708                             end
709                             7'b 111_1111: begin
710                               funcpad_data[0] = { 8'h0,                      msg_buf[0][55:0]};
711                               funcpad_data[1] = {end_of_block,  7'(funcpad), msg_buf[1][55:0]};
712                             end
713                     
714                             default: funcpad_data = '{default:'0};
715                           endcase
716                         end
717                       end else begin : gen_funcpad_data_unmasked
718                         always_comb begin
719        1/1                unique case (msg_strb)
           Tests:       T1 T2 T3 
720        1/1                  7'b 000_0000: funcpad_data[0] = {end_of_block, 63'(funcpad)                  };
           Tests:       T1 T2 T3 
721        1/1                  7'b 000_0001: funcpad_data[0] = {end_of_block, 55'(funcpad), msg_buf[0][ 7:0]};
           Tests:       T13 T16 T17 
722        1/1                  7'b 000_0011: funcpad_data[0] = {end_of_block, 47'(funcpad), msg_buf[0][15:0]};
           Tests:       T2 T3 T13 
723        1/1                  7'b 000_0111: funcpad_data[0] = {end_of_block, 39'(funcpad), msg_buf[0][23:0]};
           Tests:       T1 T12 T13 
724        1/1                  7'b 000_1111: funcpad_data[0] = {end_of_block, 31'(funcpad), msg_buf[0][31:0]};
           Tests:       T13 T16 T17 
725        1/1                  7'b 001_1111: funcpad_data[0] = {end_of_block, 23'(funcpad), msg_buf[0][39:0]};
           Tests:       T13 T16 T17 
726        1/1                  7'b 011_1111: funcpad_data[0] = {end_of_block, 15'(funcpad), msg_buf[0][47:0]};
           Tests:       T2 T3 T13 
727        1/1                  7'b 111_1111: funcpad_data[0] = {end_of_block,  7'(funcpad), msg_buf[0][55:0]};
           Tests:       T1 T12 T13 
728                     
729                             default: funcpad_data = '{default:'0};
730                           endcase
731                         end
732                       end
733                     
734                       ////////////////
735                       // Assertions //
736                       ////////////////
737                     
738                       // Prefix size is smaller than the smallest Keccak Block Size, which is 72 bytes.
739                       `ASSERT_INIT(PrefixLessThanBlock_A, PrefixSize/8 < KeccakRate[4])
740                     
741                       // Some part of datapath in sha3pad assumes Data width as 64bit.
742                       // If data width need to be changed, funcpad_data part should be changed too.
743                       // Also, The blocksize shall be divided by MsgWidth, which means, MsgWidth
744                       // can be {16, 32, 64} even funcpad_data mux is fully flexible.
745                       `ASSERT_INIT(MsgWidthidth_A, MsgWidth == 64)
746                     
747                       // Assume pulse signals: start, process, done
748                       `ASSUME(StartPulse_A, start_i |=> !start_i)
749                       `ASSUME(ProcessPulse_A, process_i |=> !process_i)
750                       `ASSUME(DonePulse_A,
751                         prim_mubi_pkg::mubi4_test_true_strict(done_i) |=>
752                           prim_mubi_pkg::mubi4_test_false_strict(done_i))
753                     
754                       // ASSERT output pulse signals: absorbed_o, keccak_run_o
755                       `ASSERT(AbsorbedPulse_A,
756                         prim_mubi_pkg::mubi4_test_true_strict(absorbed_o) |=>
757                           prim_mubi_pkg::mubi4_test_false_strict(absorbed_o))
758                       `ASSERT(KeccakRunPulse_A, keccak_run_o |=> !keccak_run_o)
759                     
760                       // start_i, done_i, process_i cannot set high at the same time
761                       `ASSUME(StartProcessDoneMutex_a,
762                         $onehot0({
763                           start_i,
764                           process_i,
765                           prim_mubi_pkg::mubi4_test_true_loose(done_i)
766                         }))
767                     
768                       // Sequence, start_i --> process_i --> absorbed_o --> done_i
769                       //`ASSUME(Sequence_a, start_i ##[1:$] process_i ##[1:$] ##[1:$] absorbed_o ##[1:$] done_i)
770                     
771                     `ifndef SYNTHESIS
772                       // Process only asserts after start and all message are fed.
773                       // These valid signals are qualifier of FPV to trigger the control signal
774                       // It is a little bit hard to specify these criteria in SVA property so creating
775                       // qualifiers in RTL form is easier.
776                       logic start_valid, process_valid, absorb_valid, done_valid;
777                     
778                       always_ff @(posedge clk_i or negedge rst_ni) begin
779        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
780        1/1                start_valid <= 1'b 1;
           Tests:       T1 T2 T3 
781        1/1              end else if (start_i) begin
           Tests:       T1 T2 T3 
782        1/1                start_valid <= 1'b 0;
           Tests:       T1 T2 T3 
783        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
           Tests:       T1 T2 T3 
784        1/1                start_valid <= 1'b 1;
           Tests:       T1 T2 T3 
785                         end
                        MISSING_ELSE
786                       end
787                       always_ff @(posedge clk_i or negedge rst_ni) begin
788        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
789        1/1                process_valid <= 1'b 0;
           Tests:       T1 T2 T3 
790        1/1              end else if (start_i) begin
           Tests:       T1 T2 T3 
791        1/1                process_valid <= 1'b 1;
           Tests:       T1 T2 T3 
792        1/1              end else if (process_i) begin
           Tests:       T1 T2 T3 
793        1/1                process_valid <= 1'b 0;
           Tests:       T1 T2 T3 
794                         end
                        MISSING_ELSE
795                       end
796                     
797                       always_ff @(posedge clk_i or negedge rst_ni) begin
798        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
799        1/1                done_valid <= 1'b 0;
           Tests:       T1 T2 T3 
800        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(absorbed_o)) begin
           Tests:       T1 T2 T3 
801        1/1                done_valid <= 1'b 1;
           Tests:       T1 T2 T3 
802        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
           Tests:       T1 T2 T3 
803        1/1                done_valid <= 1'b 0;
           Tests:       T1 T2 T3 
804                         end
                        MISSING_ELSE

Cond Coverage for Module : sha3pad

	Total	Covered	Percent
Conditions	43	38	88.37
Logical	43	38	88.37
Non-Logical	0	0
Event	0	0

 LINE       209
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------

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

 LINE       213
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------

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

 LINE       236
 EXPRESSION ((mode_i == CShake) ? 1'b1 : 1'b0)
             ---------1--------

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

 LINE       236
 SUB-EXPRESSION (mode_i == CShake)
                ---------1--------

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

 LINE       242
 EXPRESSION ((sent_message == block_addr_limit) ? 1'b1 : 1'b0)
             -----------------1----------------

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

 LINE       242
 SUB-EXPRESSION (sent_message == block_addr_limit)
                -----------------1----------------

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

 LINE       247
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------

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

 LINE       257
 EXPRESSION ((&msg_strb_i) != 1'b1)
            -----------1-----------

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

 LINE       286
 EXPRESSION (((sent_message + 1'b1) == block_addr_limit) ? 1'b1 : 1'b0)
             ---------------------1---------------------

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

 LINE       286
 SUB-EXPRESSION ((sent_message + 1'b1) == block_addr_limit)
                ---------------------1---------------------

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

 LINE       377
 EXPRESSION (msg_valid_i && msg_partial)
             -----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       388
 EXPRESSION (process_latched || process_i)
             -------1-------    ----2----

-1-	-2-	Status	Tests
0	0	Covered	T1,T2,T3
0	1	Covered	T1,T2,T3
1	0	Covered	T17,T18,T87

 LINE       418
 EXPRESSION (keccak_ack && end_of_block)
             -----1----    ------2-----

-1-	-2-	Status	Tests
0	1	Not Covered
1	0	Covered	T1,T2,T3
1	1	Covered	T13,T17,T18

 LINE       588
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------

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

 LINE       604
 EXPRESSION (msg_valid_i & ((~hold_msg)) & ((~en_msgbuf)))
             -----1-----   ------2------   -------3------

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

 LINE       616
 EXPRESSION (en_msgbuf | (keccak_ready_i & ((~hold_msg))))
             ----1----   ----------------2---------------

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

 LINE       616
 SUB-EXPRESSION (keccak_ready_i & ((~hold_msg)))
                 -------1------   ------2------

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

FSM Coverage for Module : sha3pad

**Summary for FSM :: st**
	Total	Covered	Percent
States	10	10	100.00	(Not included in score)
Transitions	21	19	90.48
Sequences	0	0

State, Transition and Sequence Details for FSM :: st

states	Line No.	Covered	Tests
StMessage	330	Covered	T1,T2,T3
StMessageWait	383	Covered	T1,T2,T3
StPad	389	Covered	T1,T2,T3
StPad01	427	Covered	T1,T2,T3
StPadFlush	435	Covered	T1,T2,T3
StPadIdle	333	Covered	T1,T2,T3
StPadRun	421	Covered	T13,T17,T18
StPrefix	328	Covered	T1,T2,T3
StPrefixWait	348	Covered	T1,T2,T3
StTerminalError	495	Covered	T4,T5,T6

transitions	Line No.	Covered	Tests
StMessage->StMessageWait	383	Covered	T1,T2,T3
StMessage->StPad	389	Covered	T1,T2,T3
StMessage->StTerminalError	495	Covered	T4,T5,T69
StMessageWait->StMessage	403	Covered	T1,T2,T3
StMessageWait->StTerminalError	495	Covered	T6,T7,T68
StPad->StPad01	427	Covered	T1,T2,T3
StPad->StPadRun	421	Covered	T13,T17,T18
StPad->StTerminalError	495	Covered	T47
StPad01->StPadFlush	452	Covered	T1,T2,T3
StPad01->StTerminalError	495	Not Covered
StPadFlush->StPadIdle	470	Covered	T1,T2,T3
StPadFlush->StTerminalError	495	Covered	T100
StPadIdle->StMessage	330	Covered	T4,T13,T16
StPadIdle->StPrefix	328	Covered	T1,T2,T3
StPadIdle->StTerminalError	495	Covered	T9,T10,T11
StPadRun->StPadFlush	435	Covered	T13,T17,T18
StPadRun->StTerminalError	495	Not Covered
StPrefix->StPrefixWait	348	Covered	T1,T2,T3
StPrefix->StTerminalError	495	Covered	T70,T71,T101
StPrefixWait->StMessage	364	Covered	T1,T2,T3
StPrefixWait->StTerminalError	495	Covered	T8,T102

Branch Coverage for Module : sha3pad

	Line No.	Total	Covered	Percent
Branches		93	89	95.70
TERNARY	213	2	2	100.00
TERNARY	236	2	2	100.00
TERNARY	242	2	2	100.00
TERNARY	286	2	2	100.00
TERNARY	588	2	2	100.00
CASE	157	6	5	83.33
IF	267	4	4	100.00
IF	279	2	2	100.00
IF	293	2	2	100.00
CASE	316	23	22	95.65
IF	494	2	2	100.00
CASE	558	4	3	75.00
CASE	591	5	5	100.00
CASE	603	5	5	100.00
CASE	615	5	5	100.00
IF	664	4	4	100.00
IF	779	4	4	100.00
IF	788	4	4	100.00
IF	798	4	4	100.00
CASE	719	9	8	88.89



213          assign prefix_index = (sent_message < block_addr_limit) ? sent_message : '0;
                                                                     -1-  
                                                                     ==>  
                                                                     ==>

Branches:

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



236          assign mode_eq_cshake = (mode_i == CShake) ? 1'b 1 : 1'b 0;
                                                        -1-  
                                                        ==>  
                                                        ==>

Branches:

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



242          assign sent_blocksize = (sent_message == block_addr_limit) ? 1'b 1 : 1'b 0;
                                                                        -1-  
                                                                        ==>  
                                                                        ==>

Branches:

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



286          assign end_of_block = ((sent_message + 1'b1) == block_addr_limit) ? 1'b 1 : 1'b 0;
                                                                               -1-  
                                                                               ==>  
                                                                               ==>

Branches:

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



588          assign keccak_addr_o = (sent_message < block_addr_limit) ? sent_message : '0;
                                                                      -1-  
                                                                      ==>  
                                                                      ==>

Branches:

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



157            unique case (strength_i)
                      -1-  
158              L128: block_addr_limit = KeccakCountW'(KeccakRate[L128]);
                 ==>
159              L224: block_addr_limit = KeccakCountW'(KeccakRate[L224]);
                 ==>
160              L256: block_addr_limit = KeccakCountW'(KeccakRate[L256]);
                 ==>
161              L384: block_addr_limit = KeccakCountW'(KeccakRate[L384]);
                 ==>
162              L512: block_addr_limit = KeccakCountW'(KeccakRate[L512]);
                 ==>
163        
164              default: block_addr_limit = '0;
                 ==>

Branches:

-1-	Status	Tests
L128	Covered	T1,T2,T3
L224	Covered	T16,T62,T82
L256	Covered	T1,T2,T3
L384	Covered	T3,T13,T18
L512	Covered	T17,T62,T82
default	Not Covered



267            if (!rst_ni) begin
               -1-  
268              process_latched <= 1'b 0;
                 ==>
269            end else if (process_i) begin
                        -2-  
270              process_latched <= 1'b 1;
                 ==>
271            end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
                        -3-  
272              process_latched <= 1'b0;
                 ==>
273            end
               MISSING_ELSE
               ==>

Branches:

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



279          `PRIM_FLOP_SPARSE_FSM(u_state_regs, st_d, st, pad_st_e, StPadIdle)
             -1-                                                                  
             ==>                                                                  
             ==>

Branches:

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



293            if (!rst_ni) absorbed_o <= prim_mubi_pkg::MuBi4False;
               -1-  
               ==>
294            else         absorbed_o <= absorbed_d;
               ==>

Branches:

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



316            unique case (st)
                      -1-  
317        
318              // In Idle state, the FSM checks if the software (or upper FSM) initiates
319              // the hash process. If `start_i` is asserted (assume it is pulse), FSM
320              // starts to push the data into the keccak round logic. Depending on the
321              // hashing mode, FSM may push additional prefex in front of the actual
322              // message. It means, the message could be back-pressured until the first
323              // prefix is processed.
324              StPadIdle: begin
325                if (start_i) begin
                   -2-  
326                  // If cSHAKE, move to Prefix state
327                  if (mode_eq_cshake) begin
                     -3-  
328                    st_d = StPrefix;
                       ==>
329                  end else begin
330                    st_d = StMessage;
                       ==>
331                  end
332                end else begin
333                  st_d = StPadIdle;
                     ==>
334                end
335              end
336        
337              // At Prefix state, FSM pushes
338              // `bytepad(encode_string(N)||encode_string(S), 168or136)`. The software
339              // already prepared `encode_string(N) || encode_string(S)` in the regs.
340              // So, the FSM adds 2Byte in front of ns_data_i, which is an encoded
341              // block size (see `encoded_bytepad` below)
342              // After pushing the prefix, it initiates the hash process and move to
343              // Message state.
344              StPrefix: begin
345                sel_mux = MuxPrefix;
346        
347                if (sent_blocksize) begin
                   -4-  
348                  st_d = StPrefixWait;
                     ==>
349        
350                  keccak_run_o = 1'b 1;
351                  fsm_keccak_valid = 1'b 0;
352                  clr_sentmsg = 1'b 1;
353                end else begin
354                  st_d = StPrefix;
                     ==>
355        
356                  fsm_keccak_valid = 1'b 1;
357                end
358              end
359        
360              StPrefixWait: begin
361                sel_mux = MuxPrefix;
362        
363                if (keccak_complete_i) begin
                   -5-  
364                  st_d = StMessage;
                     ==>
365                end else begin
366                  st_d = StPrefixWait;
                     ==>
367                end
368              end
369        
370              // Message state pushes the incoming message into keccak round logic.
371              // It forwards the message while counting the data and if it reaches
372              // the block size, it triggers the keccak round to run. If `process` is
373              // set, it moves to Pad state.
374              StMessage: begin
375                sel_mux = MuxFifo;
376        
377                if (msg_valid_i && msg_partial) begin
                   -6-  
378                  st_d = StMessage;
                     ==>
379        
380                  en_msgbuf = 1'b 1;
381                end else if (sent_blocksize) begin
                            -7-  
382                  // Check block completion first even process is set.
383                  st_d = StMessageWait;
                     ==>
384        
385                  keccak_run_o = 1'b 1;
386                  clr_sentmsg = 1'b 1;
387                  hold_msg = 1'b 1;
388                end else if (process_latched || process_i) begin
                            -8-  
389                  st_d = StPad;
                     ==>
390        
391                  // Not asserting the msg_ready_o
392                  hold_msg = 1'b 1;
393                end else begin
394                  st_d = StMessage;
                     ==>
395        
396                end
397              end
398        
399              StMessageWait: begin
400                hold_msg = 1'b 1;
401        
402                if (keccak_complete_i) begin
                   -9-  
403                  st_d = StMessage;
                     ==>
404                end else begin
405                  st_d = StMessageWait;
                     ==>
406                end
407              end
408        
409              // Pad state just pushes the ending suffix. Depending on the mode, the
410              // padding value is unique. SHA3 adds 2'b10, SHAKE adds 4'b1111, and
411              // cSHAKE adds 2'b 00. Refer `function_pad`. The signal has one more bit
412              // defined to accomodate first 1 bit of `pad10*1()` function.
413              StPad: begin
414                sel_mux = MuxFuncPad;
415        
416                fsm_keccak_valid = 1'b 1;
417        
418                if (keccak_ack && end_of_block) begin
                   -10-  
419                  // If padding is the last block, don't have to move to StPad01, just
420                  // run Keccak and complete
421                  st_d = StPadRun;
                     ==>
422        
423                  // always clear the latched msgbuf
424                  clr_msgbuf = 1'b 1;
425                  clr_sentmsg = 1'b 1;
426                end else if (keccak_ack) begin
                            -11-  
427                  st_d = StPad01;
                     ==>
428                  clr_msgbuf = 1'b 1;
429                end else begin
430                  st_d = StPad;
                     ==>
431                end
432              end
433        
434              StPadRun: begin
435                st_d = StPadFlush;
                   ==>
436        
437                keccak_run_o = 1'b 1;
438                clr_sentmsg = 1'b 1;
439              end
440        
441              // Pad01 pushes the end bit of pad10*1() function. As keccak accepts byte
442              // size only, StPad always pushes partial (5bits). So at this state, it
443              // pushes rest of 3bits. If the data pushed in StPad is the last byte of
444              // the block, then Pad01 pushes to the same byte, if not, it first
445              // zero-fill the block then pad 1 to the end.
446              StPad01: begin
447                sel_mux = MuxZeroEnd;
448        
449                // There's no chance StPad01 can be a start of the block. So can be
450                // discard that the sent_blocksize is set at the beginning.
451                if (sent_blocksize) begin
                   -12-  
452                  st_d = StPadFlush;
                     ==>
453        
454                  fsm_keccak_valid = 1'b 0;
455                  keccak_run_o = 1'b 1;
456                  clr_sentmsg = 1'b 1;
457                end else begin
458                  st_d = StPad01;
                     ==>
459        
460                  fsm_keccak_valid = 1'b 1;
461                end
462              end
463        
464              StPadFlush: begin
465                // Wait completion from keccak_round or wait SW indicator.
466                clr_sentmsg = 1'b 1;
467                clr_msgbuf = 1'b 1;
468        
469                if (keccak_complete_i) begin
                   -13-  
470                  st_d = StPadIdle;
                     ==>
471        
472                  absorbed_d = prim_mubi_pkg::MuBi4True;
473                end else begin
474                  st_d = StPadFlush;
                     ==>
475                end
476              end
477        
478              StTerminalError: begin
479                // this state is terminal
480                st_d = st;
                   ==>
481                sparse_fsm_error_o = 1'b 1;
482              end
483        
484              default: begin
485                // this state is terminal
486                st_d = StTerminalError;
                   ==>

Branches:

-1-	-2-	-3-	-4-	-5-	-6-	-7-	-8-	-9-	-10-	-11-	-12-	-13-	Status	Tests
StPadIdle	1	1	-	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPadIdle	1	0	-	-	-	-	-	-	-	-	-	-	Covered	T4,T13,T16
StPadIdle	0	-	-	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefix	-	-	1	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefix	-	-	0	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefixWait	-	-	-	1	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefixWait	-	-	-	0	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	1	-	-	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	0	1	-	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	0	0	1	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	0	0	0	-	-	-	-	-	Covered	T1,T2,T3
StMessageWait	-	-	-	-	-	-	-	1	-	-	-	-	Covered	T1,T2,T3
StMessageWait	-	-	-	-	-	-	-	0	-	-	-	-	Covered	T1,T2,T3
StPad	-	-	-	-	-	-	-	-	1	-	-	-	Covered	T13,T17,T18
StPad	-	-	-	-	-	-	-	-	0	1	-	-	Covered	T1,T2,T3
StPad	-	-	-	-	-	-	-	-	0	0	-	-	Not Covered
StPadRun	-	-	-	-	-	-	-	-	-	-	-	-	Covered	T13,T17,T18
StPad01	-	-	-	-	-	-	-	-	-	-	1	-	Covered	T1,T2,T3
StPad01	-	-	-	-	-	-	-	-	-	-	0	-	Covered	T1,T2,T3
StPadFlush	-	-	-	-	-	-	-	-	-	-	-	1	Covered	T1,T2,T3
StPadFlush	-	-	-	-	-	-	-	-	-	-	-	0	Covered	T1,T2,T3
StTerminalError	-	-	-	-	-	-	-	-	-	-	-	-	Covered	T4,T5,T6
default	-	-	-	-	-	-	-	-	-	-	-	-	Covered	T9,T10,T11



494            if (lc_ctrl_pkg::lc_tx_test_true_loose(lc_escalate_en_i)) begin
               -1-  
495              st_d = StTerminalError;
                 ==>
496            end
               MISSING_ELSE
               ==>

Branches:

-1-	Status	Tests
1	Covered	T4,T5,T6
0	Covered	T1,T2,T3



558            unique case (mode_i)
                      -1-  
559              Sha3:   funcpad = 5'b 00110;
                 ==>
560              Shake:  funcpad = 5'b 11111;
                 ==>
561              CShake: funcpad = 5'b 00100;
                 ==>
562        
563              default: begin
564                // Just create non-padding but pad10*1 only
565                funcpad = 5'b 00001;
                   ==>

Branches:

-1-	Status	Tests
Sha3	Covered	T1,T2,T3
Shake	Covered	T4,T15,T16
CShake	Covered	T1,T2,T3
default	Not Covered



591            unique case (sel_mux)
                      -1-  
592              MuxFifo:    keccak_data_o = msg_data_i;
                 ==>
593              MuxPrefix:  keccak_data_o = prefix_data;
                 ==>
594              MuxFuncPad: keccak_data_o = funcpad_data;
                 ==>
595              MuxZeroEnd: keccak_data_o = zero_with_endbit;
                 ==>
596        
597              // MuxNone
598              default:  keccak_data_o = '{default:'0};
                 ==>

Branches:

-1-	Status	Tests
MuxFifo	Covered	T1,T2,T3
MuxPrefix	Covered	T1,T2,T3
MuxFuncPad	Covered	T1,T2,T3
MuxZeroEnd	Covered	T1,T2,T3
default	Covered	T1,T2,T3



603            unique case (sel_mux)
                      -1-  
604              MuxFifo:    keccak_valid_o = msg_valid_i & ~hold_msg & ~en_msgbuf;
                 ==>
605              MuxPrefix:  keccak_valid_o = fsm_keccak_valid;
                 ==>
606              MuxFuncPad: keccak_valid_o = fsm_keccak_valid;
                 ==>
607              MuxZeroEnd: keccak_valid_o = fsm_keccak_valid;
                 ==>
608        
609              // MuxNone
610              default:  keccak_valid_o = 1'b 0;
                 ==>

Branches:

-1-	Status	Tests
MuxFifo	Covered	T1,T2,T3
MuxPrefix	Covered	T1,T2,T3
MuxFuncPad	Covered	T1,T2,T3
MuxZeroEnd	Covered	T1,T2,T3
default	Covered	T1,T2,T3



615            unique case (sel_mux)
                      -1-  
616              MuxFifo:    msg_ready_o = en_msgbuf | (keccak_ready_i & ~hold_msg);
                 ==>
617              MuxPrefix:  msg_ready_o = 1'b 0;
                 ==>
618              MuxFuncPad: msg_ready_o = 1'b 0;
                 ==>
619              MuxZeroEnd: msg_ready_o = 1'b 0;
                 ==>
620        
621              // MuxNone
622              default: msg_ready_o = 1'b 0;
                 ==>

Branches:

-1-	Status	Tests
MuxFifo	Covered	T1,T2,T3
MuxPrefix	Covered	T1,T2,T3
MuxFuncPad	Covered	T1,T2,T3
MuxZeroEnd	Covered	T1,T2,T3
default	Covered	T1,T2,T3



664            if (!rst_ni) begin
               -1-  
665              msg_buf  <= '{default:'0};
                 ==>
666              msg_strb <= '0;
667            end else if (en_msgbuf) begin
                        -2-  
668              for (int i = 0 ; i < Share ; i++) begin
                 ==>
669                msg_buf[i]  <= msg_data_i[i][0+:(MsgWidth-8)];
670              end
671              msg_strb <= msg_strb_i[0+:(MsgStrbW-1)];
672            end else if (clr_msgbuf) begin
                        -3-  
673              msg_buf  <= '{default:'0};
                 ==>
674              msg_strb <= '0;
675            end
               MISSING_ELSE
               ==>

Branches:

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



779            if (!rst_ni) begin
               -1-  
780              start_valid <= 1'b 1;
                 ==>
781            end else if (start_i) begin
                        -2-  
782              start_valid <= 1'b 0;
                 ==>
783            end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
                        -3-  
784              start_valid <= 1'b 1;
                 ==>
785            end
               MISSING_ELSE
               ==>

Branches:

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



788            if (!rst_ni) begin
               -1-  
789              process_valid <= 1'b 0;
                 ==>
790            end else if (start_i) begin
                        -2-  
791              process_valid <= 1'b 1;
                 ==>
792            end else if (process_i) begin
                        -3-  
793              process_valid <= 1'b 0;
                 ==>
794            end
               MISSING_ELSE
               ==>

Branches:

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



798            if (!rst_ni) begin
               -1-  
799              done_valid <= 1'b 0;
                 ==>
800            end else if (prim_mubi_pkg::mubi4_test_true_strict(absorbed_o)) begin
                        -2-  
801              done_valid <= 1'b 1;
                 ==>
802            end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
                        -3-  
803              done_valid <= 1'b 0;
                 ==>
804            end
               MISSING_ELSE
               ==>

Branches:

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



719              unique case (msg_strb)
                        -1-  
720                7'b 000_0000: funcpad_data[0] = {end_of_block, 63'(funcpad)                  };
                   ==>
721                7'b 000_0001: funcpad_data[0] = {end_of_block, 55'(funcpad), msg_buf[0][ 7:0]};
                   ==>
722                7'b 000_0011: funcpad_data[0] = {end_of_block, 47'(funcpad), msg_buf[0][15:0]};
                   ==>
723                7'b 000_0111: funcpad_data[0] = {end_of_block, 39'(funcpad), msg_buf[0][23:0]};
                   ==>
724                7'b 000_1111: funcpad_data[0] = {end_of_block, 31'(funcpad), msg_buf[0][31:0]};
                   ==>
725                7'b 001_1111: funcpad_data[0] = {end_of_block, 23'(funcpad), msg_buf[0][39:0]};
                   ==>
726                7'b 011_1111: funcpad_data[0] = {end_of_block, 15'(funcpad), msg_buf[0][47:0]};
                   ==>
727                7'b 111_1111: funcpad_data[0] = {end_of_block,  7'(funcpad), msg_buf[0][55:0]};
                   ==>
728        
729                default: funcpad_data = '{default:'0};
                   ==>

Branches:

-1-	Status	Tests
7'b0000000	Covered	T1,T2,T3
7'b0000001	Covered	T13,T16,T17
7'b0000011	Covered	T2,T3,T13
7'b0000111	Covered	T1,T12,T13
7'b0001111	Covered	T13,T16,T17
7'b0011111	Covered	T13,T16,T17
7'b0111111	Covered	T2,T3,T13
7'b1111111	Covered	T1,T12,T13
default	Not Covered

Assert Coverage for Module : sha3pad

	Total	Attempted	Percent	Succeeded/Matched	Percent
Assertions	22	22	100.00	22	100.00
Cover properties	4	4	100.00	4	100.00
Cover sequences	0	0		0
Total	26	26	100.00	26	100.00

Assertion Details

Name	Attempts	Real Successes	Failures	Incomplete
AbsorbedPulse_A	611077083	57058	0	0
AlwaysPartialMsgBuf_M	611077083	43666	0	0
CompleteBlockWhenProcess_A	611077083	54585	0	0
DoneCondition_M	611077083	57034	0	0
DonePulse_A	611077083	57034	0	0
KeccakAddrInRange_A	611077083	13860571	0	0
KeccakRunPulse_A	611077083	751060	0	0
MessageCondition_M	611077083	12579020	0	0
ModeStableDuringOp_M	611077083	32175	0	0
MsgReadyCondition_A	611077083	464791870	0	0
MsgWidthidth_A	665	665	0	0
NoPartialMsgFifo_M	611077083	12535354	0	0
Pad01NotAttheEndOfBlock_A	611077083	54847	0	0
PartialEndOfMsg_M	611077083	43666	0	0
PrefixLessThanBlock_A	665	665	0	0
ProcessCondition_M	611077083	57060	0	0
ProcessPulse_A	611077083	57060	0	0
StartCondition_M	611077083	57107	0	0
StartProcessDoneMutex_a	611077083	610944181	0	0
StartPulse_A	611077083	57107	0	0
StrengthStableDuringOp_M	611077083	38253	0	0
u_state_regs_A	611077083	610944181	0	0

AbsorbedPulse_A

Name	Attempts	Real Successes
Total	611077083	57058
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

AlwaysPartialMsgBuf_M

Name	Attempts	Real Successes
Total	611077083	43666
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	91
T14	5817	3
T15	46769	0
T16	0	49
T17	0	63
T18	0	43
T19	1332	0
T49	0	3

CompleteBlockWhenProcess_A

Name	Attempts	Real Successes
Total	611077083	54585
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	97
T14	5817	3
T15	46769	6
T16	0	57
T17	0	64
T18	0	76
T19	1332	0

DoneCondition_M

Name	Attempts	Real Successes
Total	611077083	57034
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

DonePulse_A

Name	Attempts	Real Successes
Total	611077083	57034
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

KeccakAddrInRange_A

Name	Attempts	Real Successes
Total	611077083	13860571
T1	7403	187
T2	7263	210
T3	16596	221
T4	2551	3
T5	3161	43
T12	2541	210
T13	117325	1378
T14	5817	210
T15	46769	306
T16	0	2744
T19	1332	0

KeccakRunPulse_A

Name	Attempts	Real Successes
Total	611077083	751060
T1	7403	11
T2	7263	10
T3	16596	13
T4	2551	0
T5	3161	2
T6	0	2
T12	2541	10
T13	117325	106
T14	5817	10
T15	46769	18
T16	0	143
T19	1332	0

MessageCondition_M

Name	Attempts	Real Successes
Total	611077083	12579020
T1	7403	104
T2	7263	91
T3	16596	182
T4	2551	3
T5	3161	22
T12	2541	91
T13	117325	728
T14	5817	91
T15	46769	102
T16	0	982
T19	1332	0

ModeStableDuringOp_M

Name	Attempts	Real Successes
Total	611077083	32175
T1	7403	1
T2	7263	1
T3	16596	3
T4	2551	1
T5	3161	1
T6	0	1
T12	2541	1
T13	117325	0
T14	5817	1
T15	46769	10
T16	0	21
T19	1332	0

MsgReadyCondition_A

Name	Attempts	Real Successes
Total	611077083	464791870
T1	7403	2865
T2	7263	2697
T3	16596	13827
T4	2551	198
T5	3161	52
T12	2541	369
T13	117325	50333
T14	5817	1473
T15	46769	43620
T16	0	15976
T19	1332	0

MsgWidthidth_A

Name	Attempts	Real Successes
Total	665	665
T1	1	1
T2	1	1
T3	1	1
T4	1	1
T5	1	1
T12	1	1
T13	1	1
T14	1	1
T15	1	1
T19	1	1

NoPartialMsgFifo_M

Name	Attempts	Real Successes
Total	611077083	12535354
T1	7403	101
T2	7263	88
T3	16596	180
T4	2551	3
T5	3161	22
T12	2541	88
T13	117325	637
T14	5817	88
T15	46769	102
T16	0	933
T19	1332	0

Pad01NotAttheEndOfBlock_A

Name	Attempts	Real Successes
Total	611077083	54847
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	97
T14	5817	3
T15	46769	6
T16	0	57
T17	0	65
T18	0	77
T19	1332	0

PartialEndOfMsg_M

Name	Attempts	Real Successes
Total	611077083	43666
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	91
T14	5817	3
T15	46769	0
T16	0	49
T17	0	63
T18	0	43
T19	1332	0
T49	0	3

PrefixLessThanBlock_A

Name	Attempts	Real Successes
Total	665	665
T1	1	1
T2	1	1
T3	1	1
T4	1	1
T5	1	1
T12	1	1
T13	1	1
T14	1	1
T15	1	1
T19	1	1

ProcessCondition_M

Name	Attempts	Real Successes
Total	611077083	57060
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

ProcessPulse_A

Name	Attempts	Real Successes
Total	611077083	57060
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

StartCondition_M

Name	Attempts	Real Successes
Total	611077083	57107
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	1
T5	3161	1
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T19	1332	0

StartProcessDoneMutex_a

Name	Attempts	Real Successes
Total	611077083	610944181
T1	7403	7342
T2	7263	7183
T3	16596	16499
T4	2551	2410
T5	3161	2979
T12	2541	2464
T13	117325	117237
T14	5817	5728
T15	46769	46681
T19	1332	1240

StartPulse_A

Name	Attempts	Real Successes
Total	611077083	57107
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	1
T5	3161	1
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T19	1332	0

StrengthStableDuringOp_M

Name	Attempts	Real Successes
Total	611077083	38253
T1	7403	2
T2	7263	1
T3	16596	5
T4	2551	2
T5	3161	2
T12	2541	1
T13	117325	2
T14	5817	1
T15	46769	9
T19	1332	1

u_state_regs_A

Name	Attempts	Real Successes
Total	611077083	610944181
T1	7403	7342
T2	7263	7183
T3	16596	16499
T4	2551	2410
T5	3161	2979
T12	2541	2464
T13	117325	117237
T14	5817	5728
T15	46769	46681
T19	1332	1240

Cover Directives for Properties: Details

Name	Attempts	Matches	Incomplete
StComplete_C	611077083	1426472	0
StMessageFeed_C	611077083	465507142	0
StPadSendMsg_C	611077083	597376	0
StPad_C	611077083	54847	0

StComplete_C

Name	Attempts	Matches
Total	611077083	1426472
T1	7403	75
T2	7263	75
T3	16596	50
T4	2551	0
T5	3161	0
T12	2541	75
T13	117325	2625
T14	5817	75
T15	46769	150
T16	0	1425
T17	0	1825
T18	0	2000
T19	1332	0

StMessageFeed_C

Name	Attempts	Matches
Total	611077083	465507142
T1	7403	2873
T2	7263	2704
T3	16596	13838
T4	2551	198
T5	3161	53
T12	2541	376
T13	117325	50439
T14	5817	1480
T15	46769	43632
T16	0	16076
T19	1332	0

StPadSendMsg_C

Name	Attempts	Matches
Total	611077083	597376
T1	7403	32
T2	7263	56
T3	16596	5
T4	2551	0
T5	3161	0
T12	2541	56
T13	117325	636
T14	5817	56
T15	46769	96
T16	0	923
T17	0	296
T18	0	673
T19	1332	0

StPad_C

Name	Attempts	Matches
Total	611077083	54847
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	97
T14	5817	3
T15	46769	6
T16	0	57
T17	0	65
T18	0	77
T19	1332	0

Line Coverage for Instance : tb.dut.u_sha3.u_pad

	Line No.	Total	Covered	Percent
TOTAL		162	161	99.38
ALWAYS	157	6	6	100.00
CONT_ASSIGN	209	1	1	100.00
CONT_ASSIGN	213	1	1	100.00
CONT_ASSIGN	236	1	1	100.00
CONT_ASSIGN	242	1	1	100.00
CONT_ASSIGN	247	1	1	100.00
CONT_ASSIGN	257	1	1	100.00
ALWAYS	267	6	6	100.00
ALWAYS	279	3	3	100.00
CONT_ASSIGN	286	1	1	100.00
ALWAYS	293	3	3	100.00
ALWAYS	298	76	75	98.68
CONT_ASSIGN	509	1	1	100.00
CONT_ASSIGN	520	1	1	100.00
CONT_ASSIGN	541	1	1	100.00
ALWAYS	558	4	4	100.00
CONT_ASSIGN	581	1	1	100.00
CONT_ASSIGN	588	1	1	100.00
ALWAYS	591	5	5	100.00
ALWAYS	603	5	5	100.00
ALWAYS	615	5	5	100.00
ALWAYS	664	10	10	100.00
ALWAYS	719	9	9	100.00
ALWAYS	779	6	6	100.00
ALWAYS	788	6	6	100.00
ALWAYS	798	6	6	100.00



156                       always_comb begin
157        1/1              unique case (strength_i)
           Tests:       T1 T2 T3 
158        1/1                L128: block_addr_limit = KeccakCountW'(KeccakRate[L128]);
           Tests:       T1 T2 T3 
159        1/1                L224: block_addr_limit = KeccakCountW'(KeccakRate[L224]);
           Tests:       T16 T62 T82 
160        1/1                L256: block_addr_limit = KeccakCountW'(KeccakRate[L256]);
           Tests:       T1 T2 T3 
161        1/1                L384: block_addr_limit = KeccakCountW'(KeccakRate[L384]);
           Tests:       T3 T13 T18 
162        1/1                L512: block_addr_limit = KeccakCountW'(KeccakRate[L512]);
           Tests:       T17 T62 T82 
163                     
164                           default: block_addr_limit = '0;
165                         endcase
166                       end
167                     
168                       /////////////////////
169                       // Control Signals //
170                       /////////////////////
171                     
172                       // `sel_mux` selects the output data among the incoming or internally generated data.
173                       // MuxFifo:    data from external (msg_data_i)
174                       // MuxPrefix:  bytepad(encode_string(N)||encode_string(S), )
175                       // MuxFuncPad: function_pad with end of message
176                       // MuxZeroEnd: all 0
177                       mux_sel_e sel_mux;
178                     
179                       // `sent_message` indicates the number of entries sent to keccak round per
180                       // block. The value shall be enough to cover Maximum entry of the Keccak
181                       // storage as defined in sha3_pkg, `$clog2(KeccakEntries+1)`. Logically,
182                       // it is not needed to have more than KeccakEntries but for safety in case of
183                       // SHA3 context switch resuming the SHA3 from the middle of sponge
184                       // construction. If needed, the software should be able to write whole 1600
185                       // bits. The `sent_message` is used to check sent_blocksize.
186                       logic [KeccakCountW-1:0] sent_message;
187                       logic inc_sentmsg, clr_sentmsg;
188                     
189                       // This primitive is used to place a hardened counter
190                       // SEC_CM: CTR.REDUN
191                       prim_count #(
192                         .Width(KeccakCountW)
193                       ) u_sentmsg_count (
194                         .clk_i,
195                         .rst_ni,
196                         .clr_i(clr_sentmsg),
197                         .set_i(1'b0),
198                         .set_cnt_i(KeccakCountW'(0)),
199                         .incr_en_i(inc_sentmsg),
200                         .decr_en_i(1'b0),
201                         .step_i(KeccakCountW'(1)),
202                         .commit_i(1'b1),
203                         .cnt_o(sent_message),
204                         .cnt_after_commit_o(),
205                         .err_o(msg_count_error_o)
206                       );
207                     
208                     
209        1/1            assign inc_sentmsg = keccak_valid_o & keccak_ready_i ;
           Tests:       T1 T2 T3 
210                     
211                       // Prefix index to slice the `prefix` n-bits into multiple of 64bit.
212                       logic [KeccakMsgAddrW-1:0] prefix_index;
213        1/1            assign prefix_index = (sent_message < block_addr_limit) ? sent_message : '0;
           Tests:       T1 T2 T3 
214                     
215                       // fsm_keccak_valid is an output signal from FSM which to send data generated
216                       // inside the pad logic to keccak_round
217                       logic fsm_keccak_valid;
218                     
219                       // hold_msg to prevent message from being forwarded into keccak_round and
220                       // acked. Mainly the usage is to hold the message and initiates the
221                       // keccak_round for current block.
222                       logic hold_msg;
223                     
224                       // latch the partial write. Latched data is used for funcpad_merged
225                       logic en_msgbuf;
226                       logic clr_msgbuf;
227                     
228                       ///////////////////
229                       // State Machine //
230                       ///////////////////
231                     
232                       // Inputs
233                     
234                       // FSM moves to StPrefix only when cSHAKE is enabled
235                       logic mode_eq_cshake;
236        1/1            assign mode_eq_cshake = (mode_i == CShake) ? 1'b 1 : 1'b 0;
           Tests:       T1 T2 T3 
237                     
238                       // `sent_blocksize` indicates the pad logic pushed block size data into
239                       // keccak round logic.
240                       logic sent_blocksize;
241                     
242        1/1            assign sent_blocksize = (sent_message == block_addr_limit) ? 1'b 1 : 1'b 0;
           Tests:       T1 T2 T3 
243                     
244                       // `keccak_ack` indicates the request is accepted in keccak_round
245                       logic keccak_ack;
246                     
247        1/1            assign keccak_ack = keccak_valid_o & keccak_ready_i ;
           Tests:       T1 T2 T3 
248                     
249                       // msg_partial indicates the incoming message is partial write or not.
250                       // This is used to check if the incoming message need to be latched inside or
251                       // not. If no partial message is at the end, msg_buf doesn't have to latch
252                       // msg_data_i. It is assumed that the partial message is permitted only at
253                       // the end of the message. So if (msg_valid_i && msg_partial && msg_ready_o),
254                       // there will be no msg_valid_i till process_latched.
255                       // Shall be used with msg_valid_i together.
256                       logic msg_partial;
257        1/1            assign msg_partial = (&msg_strb_i != 1'b 1);
           Tests:       T1 T2 T3 
258                     
259                     
260                       // `process_latched` latches the `process_i` input before it is seen in the
261                       // FSM. `process_i` may follow `start_i` too fast so that the FSM may not
262                       // see it fast enought in case of cSHAKE mode. cSHAKE needs to process the
263                       // prefix prior to see the process indicator.
264                       logic process_latched;
265                     
266                       always_ff @(posedge clk_i or negedge rst_ni) begin
267        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
268        1/1                process_latched <= 1'b 0;
           Tests:       T1 T2 T3 
269        1/1              end else if (process_i) begin
           Tests:       T1 T2 T3 
270        1/1                process_latched <= 1'b 1;
           Tests:       T1 T2 T3 
271        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
           Tests:       T1 T2 T3 
272        1/1                process_latched <= 1'b0;
           Tests:       T1 T2 T3 
273                         end
                        MISSING_ELSE
274                       end
275                     
276                       // State Register ===========================================================
277                       pad_st_e st, st_d;
278                     
279        3/3            `PRIM_FLOP_SPARSE_FSM(u_state_regs, st_d, st, pad_st_e, StPadIdle)
           Tests:       T1 T2 T3  | T1 T2 T3  | T1 T2 T3 
PRIM_FLOP_SPARSE_FSM(u_state_regs, st_d, st, pad_st_e, StPadIdle):
279.1                   `ifdef SIMULATION                                   
279.2                       prim_sparse_fsm_flop #(                           
279.3                         .StateEnumT(pad_st_e),                            
279.4                         .Width($bits(pad_st_e)),                          
279.5                         .ResetValue($bits(pad_st_e)'(StPadIdle)),          
279.6                         .EnableAlertTriggerSVA(1), 
279.7                         .CustomForceName("st")          
279.8                       ) u_state_regs (                                        
279.9                         .clk_i   ( clk_i   ),                           
279.10                        .rst_ni  ( rst_ni ),                           
279.11                        .state_i ( st_d     ),                           
279.12                        .state_o (         )                            
279.13                      );                                                
279.14                      always_ff @(posedge clk_i or negedge rst_ni) begin 
279.15     1/1              if (!rst_ni) begin                               
           Tests:       T1 T2 T3 
279.16     1/1                st <= StPadIdle;                                
           Tests:       T1 T2 T3 
279.17                      end else begin                                    
279.18     1/1                st <= st_d;                                     
           Tests:       T1 T2 T3 
279.19                      end                                               
279.20                    end  
279.21                      u_state_regs_A: assert property (@(posedge clk_i) disable iff ((!rst_ni) !== '0) (st === u_state_regs.state_o))       
279.22                      else begin                                                                           
279.23                        `ifdef UVM                                                                               
279.24                    uvm_pkg::uvm_report_error("ASSERT FAILED", "u_state_regs_A", uvm_pkg::UVM_NONE, 
279.25                                              "../src/lowrisc_ip_sha3_0.1/rtl/sha3pad.sv", 279, "", 1);                                
279.26                  `else                                                                                    
279.27                    $error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__,         
279.28                           `PRIM_STRINGIFY(u_state_regs_A));                                                       
279.29                  `endif                                                              
279.30                      end 
279.31                    `else                                               
279.32                      prim_sparse_fsm_flop #(                           
279.33                        .StateEnumT(pad_st_e),                            
279.34                        .Width($bits(pad_st_e)),                          
279.35                        .ResetValue($bits(pad_st_e)'(StPadIdle)),          
279.36                        .EnableAlertTriggerSVA(1)  
279.37                      ) u_state_regs (                                        
279.38                        .clk_i   ( `PRIM_FLOP_CLK   ),                           
279.39                        .rst_ni  ( `PRIM_FLOP_RST ),                           
279.40                        .state_i ( st_d     ),                           
279.41                        .state_o ( st     )                            
279.42                      );                                                
279.43                    `endif280                     
281                       // `end_of_block` indicates current beat is end of the block
282                       // It shall set when the address reaches to the end of the block. End address
283                       // is set by the strength_i, which is `block_addr_limit`.
284                       logic end_of_block;
285                     
286        1/1            assign end_of_block = ((sent_message + 1'b1) == block_addr_limit) ? 1'b 1 : 1'b 0;
           Tests:       T1 T2 T3 
287                     
288                     
289                       // Next logic and output logic ==============================================
290                       // SEC_CM: ABSORBED.CTRL.MUBI
291                       prim_mubi_pkg::mubi4_t absorbed_d;
292                       always_ff @(posedge clk_i or negedge rst_ni) begin
293        2/2              if (!rst_ni) absorbed_o <= prim_mubi_pkg::MuBi4False;
           Tests:       T1 T2 T3  | T1 T2 T3 
294        1/1              else         absorbed_o <= absorbed_d;
           Tests:       T1 T2 T3 
295                       end
296                     
297                       always_comb begin
298        1/1              st_d = st;
           Tests:       T1 T2 T3 
299                     
300                         // FSM output : default values
301        1/1              keccak_run_o = 1'b 0;
           Tests:       T1 T2 T3 
302        1/1              sel_mux      = MuxNone;
           Tests:       T1 T2 T3 
303                     
304        1/1              fsm_keccak_valid = 1'b 0;
           Tests:       T1 T2 T3 
305                     
306        1/1              hold_msg = 1'b 0;
           Tests:       T1 T2 T3 
307        1/1              clr_sentmsg = 1'b 0;
           Tests:       T1 T2 T3 
308                     
309        1/1              en_msgbuf = 1'b 0;
           Tests:       T1 T2 T3 
310        1/1              clr_msgbuf = 1'b 0;
           Tests:       T1 T2 T3 
311                     
312        1/1              absorbed_d = prim_mubi_pkg::MuBi4False;
           Tests:       T1 T2 T3 
313                     
314        1/1              sparse_fsm_error_o = 1'b 0;
           Tests:       T1 T2 T3 
315                     
316        1/1              unique case (st)
           Tests:       T1 T2 T3 
317                     
318                           // In Idle state, the FSM checks if the software (or upper FSM) initiates
319                           // the hash process. If `start_i` is asserted (assume it is pulse), FSM
320                           // starts to push the data into the keccak round logic. Depending on the
321                           // hashing mode, FSM may push additional prefex in front of the actual
322                           // message. It means, the message could be back-pressured until the first
323                           // prefix is processed.
324                           StPadIdle: begin
325        1/1                  if (start_i) begin
           Tests:       T1 T2 T3 
326                               // If cSHAKE, move to Prefix state
327        1/1                    if (mode_eq_cshake) begin
           Tests:       T1 T2 T3 
328        1/1                      st_d = StPrefix;
           Tests:       T1 T2 T3 
329                               end else begin
330        1/1                      st_d = StMessage;
           Tests:       T4 T13 T16 
331                               end
332                             end else begin
333        1/1                    st_d = StPadIdle;
           Tests:       T1 T2 T3 
334                             end
335                           end
336                     
337                           // At Prefix state, FSM pushes
338                           // `bytepad(encode_string(N)||encode_string(S), 168or136)`. The software
339                           // already prepared `encode_string(N) || encode_string(S)` in the regs.
340                           // So, the FSM adds 2Byte in front of ns_data_i, which is an encoded
341                           // block size (see `encoded_bytepad` below)
342                           // After pushing the prefix, it initiates the hash process and move to
343                           // Message state.
344                           StPrefix: begin
345        1/1                  sel_mux = MuxPrefix;
           Tests:       T1 T2 T3 
346                     
347        1/1                  if (sent_blocksize) begin
           Tests:       T1 T2 T3 
348        1/1                    st_d = StPrefixWait;
           Tests:       T1 T2 T3 
349                     
350        1/1                    keccak_run_o = 1'b 1;
           Tests:       T1 T2 T3 
351        1/1                    fsm_keccak_valid = 1'b 0;
           Tests:       T1 T2 T3 
352        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
353                             end else begin
354        1/1                    st_d = StPrefix;
           Tests:       T1 T2 T3 
355                     
356        1/1                    fsm_keccak_valid = 1'b 1;
           Tests:       T1 T2 T3 
357                             end
358                           end
359                     
360                           StPrefixWait: begin
361        1/1                  sel_mux = MuxPrefix;
           Tests:       T1 T2 T3 
362                     
363        1/1                  if (keccak_complete_i) begin
           Tests:       T1 T2 T3 
364        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
365                             end else begin
366        1/1                    st_d = StPrefixWait;
           Tests:       T1 T2 T3 
367                             end
368                           end
369                     
370                           // Message state pushes the incoming message into keccak round logic.
371                           // It forwards the message while counting the data and if it reaches
372                           // the block size, it triggers the keccak round to run. If `process` is
373                           // set, it moves to Pad state.
374                           StMessage: begin
375        1/1                  sel_mux = MuxFifo;
           Tests:       T1 T2 T3 
376                     
377        1/1                  if (msg_valid_i && msg_partial) begin
           Tests:       T1 T2 T3 
378        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
379                     
380        1/1                    en_msgbuf = 1'b 1;
           Tests:       T1 T2 T3 
381        1/1                  end else if (sent_blocksize) begin
           Tests:       T1 T2 T3 
382                               // Check block completion first even process is set.
383        1/1                    st_d = StMessageWait;
           Tests:       T1 T2 T3 
384                     
385        1/1                    keccak_run_o = 1'b 1;
           Tests:       T1 T2 T3 
386        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
387        1/1                    hold_msg = 1'b 1;
           Tests:       T1 T2 T3 
388        1/1                  end else if (process_latched || process_i) begin
           Tests:       T1 T2 T3 
389        1/1                    st_d = StPad;
           Tests:       T1 T2 T3 
390                     
391                               // Not asserting the msg_ready_o
392        1/1                    hold_msg = 1'b 1;
           Tests:       T1 T2 T3 
393                             end else begin
394        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
395                     
396                             end
397                           end
398                     
399                           StMessageWait: begin
400        1/1                  hold_msg = 1'b 1;
           Tests:       T1 T2 T3 
401                     
402        1/1                  if (keccak_complete_i) begin
           Tests:       T1 T2 T3 
403        1/1                    st_d = StMessage;
           Tests:       T1 T2 T3 
404                             end else begin
405        1/1                    st_d = StMessageWait;
           Tests:       T1 T2 T3 
406                             end
407                           end
408                     
409                           // Pad state just pushes the ending suffix. Depending on the mode, the
410                           // padding value is unique. SHA3 adds 2'b10, SHAKE adds 4'b1111, and
411                           // cSHAKE adds 2'b 00. Refer `function_pad`. The signal has one more bit
412                           // defined to accomodate first 1 bit of `pad10*1()` function.
413                           StPad: begin
414        1/1                  sel_mux = MuxFuncPad;
           Tests:       T1 T2 T3 
415                     
416        1/1                  fsm_keccak_valid = 1'b 1;
           Tests:       T1 T2 T3 
417                     
418        1/1                  if (keccak_ack && end_of_block) begin
           Tests:       T1 T2 T3 
419                               // If padding is the last block, don't have to move to StPad01, just
420                               // run Keccak and complete
421        1/1                    st_d = StPadRun;
           Tests:       T13 T17 T18 
422                     
423                               // always clear the latched msgbuf
424        1/1                    clr_msgbuf = 1'b 1;
           Tests:       T13 T17 T18 
425        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T13 T17 T18 
426        1/1                  end else if (keccak_ack) begin
           Tests:       T1 T2 T3 
427        1/1                    st_d = StPad01;
           Tests:       T1 T2 T3 
428        1/1                    clr_msgbuf = 1'b 1;
           Tests:       T1 T2 T3 
429                             end else begin
430        0/1     ==>            st_d = StPad;
431                             end
432                           end
433                     
434                           StPadRun: begin
435        1/1                  st_d = StPadFlush;
           Tests:       T13 T17 T18 
436                     
437        1/1                  keccak_run_o = 1'b 1;
           Tests:       T13 T17 T18 
438        1/1                  clr_sentmsg = 1'b 1;
           Tests:       T13 T17 T18 
439                           end
440                     
441                           // Pad01 pushes the end bit of pad10*1() function. As keccak accepts byte
442                           // size only, StPad always pushes partial (5bits). So at this state, it
443                           // pushes rest of 3bits. If the data pushed in StPad is the last byte of
444                           // the block, then Pad01 pushes to the same byte, if not, it first
445                           // zero-fill the block then pad 1 to the end.
446                           StPad01: begin
447        1/1                  sel_mux = MuxZeroEnd;
           Tests:       T1 T2 T3 
448                     
449                             // There's no chance StPad01 can be a start of the block. So can be
450                             // discard that the sent_blocksize is set at the beginning.
451        1/1                  if (sent_blocksize) begin
           Tests:       T1 T2 T3 
452        1/1                    st_d = StPadFlush;
           Tests:       T1 T2 T3 
453                     
454        1/1                    fsm_keccak_valid = 1'b 0;
           Tests:       T1 T2 T3 
455        1/1                    keccak_run_o = 1'b 1;
           Tests:       T1 T2 T3 
456        1/1                    clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
457                             end else begin
458        1/1                    st_d = StPad01;
           Tests:       T1 T2 T3 
459                     
460        1/1                    fsm_keccak_valid = 1'b 1;
           Tests:       T1 T2 T3 
461                             end
462                           end
463                     
464                           StPadFlush: begin
465                             // Wait completion from keccak_round or wait SW indicator.
466        1/1                  clr_sentmsg = 1'b 1;
           Tests:       T1 T2 T3 
467        1/1                  clr_msgbuf = 1'b 1;
           Tests:       T1 T2 T3 
468                     
469        1/1                  if (keccak_complete_i) begin
           Tests:       T1 T2 T3 
470        1/1                    st_d = StPadIdle;
           Tests:       T1 T2 T3 
471                     
472        1/1                    absorbed_d = prim_mubi_pkg::MuBi4True;
           Tests:       T1 T2 T3 
473                             end else begin
474        1/1                    st_d = StPadFlush;
           Tests:       T1 T2 T3 
475                             end
476                           end
477                     
478                           StTerminalError: begin
479                             // this state is terminal
480        1/1                  st_d = st;
           Tests:       T4 T5 T6 
481        1/1                  sparse_fsm_error_o = 1'b 1;
           Tests:       T4 T5 T6 
482                           end
483                     
484                           default: begin
485                             // this state is terminal
486                             st_d = StTerminalError;
487                             sparse_fsm_error_o = 1'b 1;
488                           end
489                         endcase
490                     
491                         // SEC_CM: FSM.GLOBAL_ESC, FSM.LOCAL_ESC
492                         // Unconditionally jump into the terminal error state
493                         // if the life cycle controller triggers an escalation.
494        1/1              if (lc_ctrl_pkg::lc_tx_test_true_loose(lc_escalate_en_i)) begin
           Tests:       T1 T2 T3 
495        1/1                st_d = StTerminalError;
           Tests:       T4 T5 T6 
496                         end
                        MISSING_ELSE
497                       end
498                     
499                       //////////////
500                       // Datapath //
501                       //////////////
502                     
503                       // `encode_bytepad` represents the first two bytes of bytepad()
504                       // It depends on the block size. We can reuse KeccakRate
505                       // 10000000 || 00010101 // 168
506                       // 10000000 || 00010001 // 136
507                       logic [15:0] encode_bytepad;
508                     
509        1/1            assign encode_bytepad = encode_bytepad_len(strength_i);
           Tests:       T1 T2 T3 
510                     
511                       // Prefix size ==============================================================
512                       // Prefix represents bytepad(encode_string(N) || encode_string(S), 168 or 136)
513                       // encode_string(N) || encode_string(S) is prepared by the software and given
514                       // through `ns_data_i`. The first part of bytepad is determined by the
515                       // `strength_i` and stored into `encode_bytepad`.
516                     
517                       // It is assumed that the prefix always smaller than the block size.
518                       logic [PrefixSize*8-1:0] prefix;
519                     
520        1/1            assign prefix = {ns_data_i, encode_bytepad};
           Tests:       T1 T2 T3 
521                     
522                       logic [MsgWidth-1:0] prefix_sliced;
523                       logic [MsgWidth-1:0] prefix_data [Share];
524                     
525                       prim_slicer #(
526                         .InW (PrefixSize*8),
527                         .IndexW(KeccakMsgAddrW),
528                         .OutW(MsgWidth)
529                       ) u_prefix_slicer (
530                         .sel_i  (prefix_index),
531                         .data_i (prefix),
532                         .data_o (prefix_sliced)
533                       );
534                     
535                       if (EnMasking) begin : gen_prefix_masked
536                         // If Masking is enabled, prefix is two share.
537                         assign prefix_data[0] = '0;
538                         assign prefix_data[1] = prefix_sliced;
539                       end else begin : gen_prefix_unmasked
540                         // If Unmasked, only one share exists.
541        1/1              assign prefix_data[0] = prefix_sliced;
           Tests:       T1 T2 T3 
542                       end
543                     
544                       // ==========================================================================
545                       // function_pad is the unique value padded at the end of the message based on
546                       // the function among SHA3, SHAKE, cSHAKE. The standard mentioned that SHA3
547                       // pads `01` , SHAKE pads `1111`, and cSHAKE pads `00`.
548                       //
549                       // Then pad10*1() function follows. It adds `1` first then fill 0 until it
550                       // reaches the block size -1, then adds `1`.
551                       //
552                       // It means always `1` is followed by the function pad.
553                       logic [4:0] funcpad;
554                     
555                       logic [MsgWidth-1:0] funcpad_data [Share];
556                     
557                       always_comb begin
558        1/1              unique case (mode_i)
           Tests:       T1 T2 T3 
559        1/1                Sha3:   funcpad = 5'b 00110;
           Tests:       T1 T2 T3 
560        1/1                Shake:  funcpad = 5'b 11111;
           Tests:       T4 T15 T16 
561        1/1                CShake: funcpad = 5'b 00100;
           Tests:       T1 T2 T3 
562                     
563                           default: begin
564                             // Just create non-padding but pad10*1 only
565                             funcpad = 5'b 00001;
566                           end
567                         endcase
568                       end
569                     
570                       // ==========================================================================
571                       // `zero_with_endbit` contains all zero unless the message is for the last
572                       // MsgWidth beat in the block. If it is the end of the block, the last bit
573                       // will be set to complete pad10*1() functionality.
574                       logic [MsgWidth-1:0] zero_with_endbit [Share];
575                     
576                       if (EnMasking) begin : gen_zeroend_masked
577                         assign zero_with_endbit[0]               = '0;
578                         assign zero_with_endbit[1][MsgWidth-1]   = end_of_block;
579                         assign zero_with_endbit[1][MsgWidth-2:0] = '0;
580                       end else begin : gen_zeroend_unmasked
581        1/1              assign zero_with_endbit[0][MsgWidth-1]   = end_of_block;
           Tests:       T1 T2 T3 
582                         assign zero_with_endbit[0][MsgWidth-2:0] = '0;
583                       end
584                     
585                       // ==========================================================================
586                       // Data mux for output data
587                     
588        1/1            assign keccak_addr_o = (sent_message < block_addr_limit) ? sent_message : '0;
           Tests:       T1 T2 T3 
589                     
590                       always_comb begin
591        1/1              unique case (sel_mux)
           Tests:       T1 T2 T3 
592        1/1                MuxFifo:    keccak_data_o = msg_data_i;
           Tests:       T1 T2 T3 
593        1/1                MuxPrefix:  keccak_data_o = prefix_data;
           Tests:       T1 T2 T3 
594        1/1                MuxFuncPad: keccak_data_o = funcpad_data;
           Tests:       T1 T2 T3 
595        1/1                MuxZeroEnd: keccak_data_o = zero_with_endbit;
           Tests:       T1 T2 T3 
596                     
597                           // MuxNone
598                           default:  keccak_data_o = '{default:'0};
599                         endcase
600                       end
601                     
602                       always_comb begin
603        1/1              unique case (sel_mux)
           Tests:       T1 T2 T3 
604        1/1                MuxFifo:    keccak_valid_o = msg_valid_i & ~hold_msg & ~en_msgbuf;
           Tests:       T1 T2 T3 
605        1/1                MuxPrefix:  keccak_valid_o = fsm_keccak_valid;
           Tests:       T1 T2 T3 
606        1/1                MuxFuncPad: keccak_valid_o = fsm_keccak_valid;
           Tests:       T1 T2 T3 
607        1/1                MuxZeroEnd: keccak_valid_o = fsm_keccak_valid;
           Tests:       T1 T2 T3 
608                     
609                           // MuxNone
610                           default:  keccak_valid_o = 1'b 0;
611                         endcase
612                       end
613                     
614                       always_comb begin
615        1/1              unique case (sel_mux)
           Tests:       T1 T2 T3 
616        1/1                MuxFifo:    msg_ready_o = en_msgbuf | (keccak_ready_i & ~hold_msg);
           Tests:       T1 T2 T3 
617        1/1                MuxPrefix:  msg_ready_o = 1'b 0;
           Tests:       T1 T2 T3 
618        1/1                MuxFuncPad: msg_ready_o = 1'b 0;
           Tests:       T1 T2 T3 
619        1/1                MuxZeroEnd: msg_ready_o = 1'b 0;
           Tests:       T1 T2 T3 
620                     
621                           // MuxNone
622                           default: msg_ready_o = 1'b 0;
623                         endcase
624                       end
625                     
626                       // prim_packer : packing to 64bit to update keccak storage
627                       // two prim_packer in this module are used to pack the data received from
628                       // upper layer (KMAC core) and also the 5bit padding bits.
629                       // It is assumed that the message from upper layer could be partial at the
630                       // end of the message. Then the 2 or 4bit padding is required. It can be
631                       // handled by some custom logic or could be done by prim_packer.
632                       // If packer is used, the MSG_FIFO doesn't have to have another prim_packer
633                       // in front of the FIFO. This logic can handle the partial writes from the
634                       // software.
635                       //
636                       // If a custom logic is implemented here, prim_packer is necessary in front
637                       // of the FIFO, as this logic only appends at the end of the message when
638                       // `process_i` is asserted. Also, in this case, even prim_packer is not
639                       // needed, still 64bit registers to latch the partial write is required.
640                       // If not, the logic has to delay the acceptance of the incoming write
641                       // accesses. It may trigger the back-pressuring in some case which may result
642                       // that the software(or upper layer) may not set process_i.
643                       //
644                       // For custom logic, it could be implemented by the 8 mux selection.
645                       // for instance: (subject to be changed)
646                       //   unique case (sent_byte[2:0]) // generated from msg_strb_i
647                       //     3'b 000: funcpad_merged = {end_of_block, 63'(function_pad)                  };
648                       //     3'b 001: funcpad_merged = {end_of_block, 55'(function_pad), msg_data_i[ 7:0]};
649                       //     3'b 010: funcpad_merged = {end_of_block, 47'(function_pad), msg_data_i[15:0]};
650                       //     3'b 011: funcpad_merged = {end_of_block, 39'(function_pad), msg_data_i[23:0]};
651                       //     3'b 100: funcpad_merged = {end_of_block, 31'(function_pad), msg_data_i[31:0]};
652                       //     3'b 101: funcpad_merged = {end_of_block, 23'(function_pad), msg_data_i[39:0]};
653                       //     3'b 110: funcpad_merged = {end_of_block, 15'(function_pad), msg_data_i[47:0]};
654                       //     3'b 111: funcpad_merged = {end_of_block,  7'(function_pad), msg_data_i[55:0]};
655                       //     default: funcpad_merged = '0;
656                       //   endcase
657                     
658                       // internal buffer to store partial write. It doesn't have to store last byte as it
659                       // stores only when partial write.
660                       logic [MsgWidth-8-1:0] msg_buf [Share];
661                       logic [MsgStrbW-1-1:0] msg_strb;
662                     
663                       always_ff @(posedge clk_i or negedge rst_ni) begin
664        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
665        1/1                msg_buf  <= '{default:'0};
           Tests:       T1 T2 T3 
666        1/1                msg_strb <= '0;
           Tests:       T1 T2 T3 
667        1/1              end else if (en_msgbuf) begin
           Tests:       T1 T2 T3 
668        1/1                for (int i = 0 ; i < Share ; i++) begin
           Tests:       T1 T2 T3 
669        1/1                  msg_buf[i]  <= msg_data_i[i][0+:(MsgWidth-8)];
           Tests:       T1 T2 T3 
670                           end
671        1/1                msg_strb <= msg_strb_i[0+:(MsgStrbW-1)];
           Tests:       T1 T2 T3 
672        1/1              end else if (clr_msgbuf) begin
           Tests:       T1 T2 T3 
673        1/1                msg_buf  <= '{default:'0};
           Tests:       T1 T2 T3 
674        1/1                msg_strb <= '0;
           Tests:       T1 T2 T3 
675                         end
                        MISSING_ELSE
676                       end
677                     
678                       if (EnMasking) begin : gen_funcpad_data_masked
679                         always_comb begin
680                           unique case (msg_strb)
681                             7'b 000_0000: begin
682                               funcpad_data[0] = '0;
683                               funcpad_data[1] = {end_of_block, 63'(funcpad)                  };
684                             end
685                             7'b 000_0001: begin
686                               funcpad_data[0] = {56'h0,                      msg_buf[0][ 7:0]};
687                               funcpad_data[1] = {end_of_block, 55'(funcpad), msg_buf[1][ 7:0]};
688                             end
689                             7'b 000_0011: begin
690                               funcpad_data[0] = {48'h0,                      msg_buf[0][15:0]};
691                               funcpad_data[1] = {end_of_block, 47'(funcpad), msg_buf[1][15:0]};
692                             end
693                             7'b 000_0111: begin
694                               funcpad_data[0] = {40'h0,                      msg_buf[0][23:0]};
695                               funcpad_data[1] = {end_of_block, 39'(funcpad), msg_buf[1][23:0]};
696                             end
697                             7'b 000_1111: begin
698                               funcpad_data[0] = {32'h0,                      msg_buf[0][31:0]};
699                               funcpad_data[1] = {end_of_block, 31'(funcpad), msg_buf[1][31:0]};
700                             end
701                             7'b 001_1111: begin
702                               funcpad_data[0] = {24'h0,                      msg_buf[0][39:0]};
703                               funcpad_data[1] = {end_of_block, 23'(funcpad), msg_buf[1][39:0]};
704                             end
705                             7'b 011_1111: begin
706                               funcpad_data[0] = {16'h0,                      msg_buf[0][47:0]};
707                               funcpad_data[1] = {end_of_block, 15'(funcpad), msg_buf[1][47:0]};
708                             end
709                             7'b 111_1111: begin
710                               funcpad_data[0] = { 8'h0,                      msg_buf[0][55:0]};
711                               funcpad_data[1] = {end_of_block,  7'(funcpad), msg_buf[1][55:0]};
712                             end
713                     
714                             default: funcpad_data = '{default:'0};
715                           endcase
716                         end
717                       end else begin : gen_funcpad_data_unmasked
718                         always_comb begin
719        1/1                unique case (msg_strb)
           Tests:       T1 T2 T3 
720        1/1                  7'b 000_0000: funcpad_data[0] = {end_of_block, 63'(funcpad)                  };
           Tests:       T1 T2 T3 
721        1/1                  7'b 000_0001: funcpad_data[0] = {end_of_block, 55'(funcpad), msg_buf[0][ 7:0]};
           Tests:       T13 T16 T17 
722        1/1                  7'b 000_0011: funcpad_data[0] = {end_of_block, 47'(funcpad), msg_buf[0][15:0]};
           Tests:       T2 T3 T13 
723        1/1                  7'b 000_0111: funcpad_data[0] = {end_of_block, 39'(funcpad), msg_buf[0][23:0]};
           Tests:       T1 T12 T13 
724        1/1                  7'b 000_1111: funcpad_data[0] = {end_of_block, 31'(funcpad), msg_buf[0][31:0]};
           Tests:       T13 T16 T17 
725        1/1                  7'b 001_1111: funcpad_data[0] = {end_of_block, 23'(funcpad), msg_buf[0][39:0]};
           Tests:       T13 T16 T17 
726        1/1                  7'b 011_1111: funcpad_data[0] = {end_of_block, 15'(funcpad), msg_buf[0][47:0]};
           Tests:       T2 T3 T13 
727        1/1                  7'b 111_1111: funcpad_data[0] = {end_of_block,  7'(funcpad), msg_buf[0][55:0]};
           Tests:       T1 T12 T13 
728                     
729                             default: funcpad_data = '{default:'0};
730                           endcase
731                         end
732                       end
733                     
734                       ////////////////
735                       // Assertions //
736                       ////////////////
737                     
738                       // Prefix size is smaller than the smallest Keccak Block Size, which is 72 bytes.
739                       `ASSERT_INIT(PrefixLessThanBlock_A, PrefixSize/8 < KeccakRate[4])
740                     
741                       // Some part of datapath in sha3pad assumes Data width as 64bit.
742                       // If data width need to be changed, funcpad_data part should be changed too.
743                       // Also, The blocksize shall be divided by MsgWidth, which means, MsgWidth
744                       // can be {16, 32, 64} even funcpad_data mux is fully flexible.
745                       `ASSERT_INIT(MsgWidthidth_A, MsgWidth == 64)
746                     
747                       // Assume pulse signals: start, process, done
748                       `ASSUME(StartPulse_A, start_i |=> !start_i)
749                       `ASSUME(ProcessPulse_A, process_i |=> !process_i)
750                       `ASSUME(DonePulse_A,
751                         prim_mubi_pkg::mubi4_test_true_strict(done_i) |=>
752                           prim_mubi_pkg::mubi4_test_false_strict(done_i))
753                     
754                       // ASSERT output pulse signals: absorbed_o, keccak_run_o
755                       `ASSERT(AbsorbedPulse_A,
756                         prim_mubi_pkg::mubi4_test_true_strict(absorbed_o) |=>
757                           prim_mubi_pkg::mubi4_test_false_strict(absorbed_o))
758                       `ASSERT(KeccakRunPulse_A, keccak_run_o |=> !keccak_run_o)
759                     
760                       // start_i, done_i, process_i cannot set high at the same time
761                       `ASSUME(StartProcessDoneMutex_a,
762                         $onehot0({
763                           start_i,
764                           process_i,
765                           prim_mubi_pkg::mubi4_test_true_loose(done_i)
766                         }))
767                     
768                       // Sequence, start_i --> process_i --> absorbed_o --> done_i
769                       //`ASSUME(Sequence_a, start_i ##[1:$] process_i ##[1:$] ##[1:$] absorbed_o ##[1:$] done_i)
770                     
771                     `ifndef SYNTHESIS
772                       // Process only asserts after start and all message are fed.
773                       // These valid signals are qualifier of FPV to trigger the control signal
774                       // It is a little bit hard to specify these criteria in SVA property so creating
775                       // qualifiers in RTL form is easier.
776                       logic start_valid, process_valid, absorb_valid, done_valid;
777                     
778                       always_ff @(posedge clk_i or negedge rst_ni) begin
779        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
780        1/1                start_valid <= 1'b 1;
           Tests:       T1 T2 T3 
781        1/1              end else if (start_i) begin
           Tests:       T1 T2 T3 
782        1/1                start_valid <= 1'b 0;
           Tests:       T1 T2 T3 
783        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
           Tests:       T1 T2 T3 
784        1/1                start_valid <= 1'b 1;
           Tests:       T1 T2 T3 
785                         end
                        MISSING_ELSE
786                       end
787                       always_ff @(posedge clk_i or negedge rst_ni) begin
788        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
789        1/1                process_valid <= 1'b 0;
           Tests:       T1 T2 T3 
790        1/1              end else if (start_i) begin
           Tests:       T1 T2 T3 
791        1/1                process_valid <= 1'b 1;
           Tests:       T1 T2 T3 
792        1/1              end else if (process_i) begin
           Tests:       T1 T2 T3 
793        1/1                process_valid <= 1'b 0;
           Tests:       T1 T2 T3 
794                         end
                        MISSING_ELSE
795                       end
796                     
797                       always_ff @(posedge clk_i or negedge rst_ni) begin
798        1/1              if (!rst_ni) begin
           Tests:       T1 T2 T3 
799        1/1                done_valid <= 1'b 0;
           Tests:       T1 T2 T3 
800        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(absorbed_o)) begin
           Tests:       T1 T2 T3 
801        1/1                done_valid <= 1'b 1;
           Tests:       T1 T2 T3 
802        1/1              end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
           Tests:       T1 T2 T3 
803        1/1                done_valid <= 1'b 0;
           Tests:       T1 T2 T3 
804                         end
                        MISSING_ELSE

Cond Coverage for Instance : tb.dut.u_sha3.u_pad

	Total	Covered	Percent
Conditions	43	38	88.37
Logical	43	38	88.37
Non-Logical	0	0
Event	0	0

 LINE       209
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------

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

 LINE       213
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------

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

 LINE       236
 EXPRESSION ((mode_i == CShake) ? 1'b1 : 1'b0)
             ---------1--------

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

 LINE       236
 SUB-EXPRESSION (mode_i == CShake)
                ---------1--------

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

 LINE       242
 EXPRESSION ((sent_message == block_addr_limit) ? 1'b1 : 1'b0)
             -----------------1----------------

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

 LINE       242
 SUB-EXPRESSION (sent_message == block_addr_limit)
                -----------------1----------------

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

 LINE       247
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------

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

 LINE       257
 EXPRESSION ((&msg_strb_i) != 1'b1)
            -----------1-----------

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

 LINE       286
 EXPRESSION (((sent_message + 1'b1) == block_addr_limit) ? 1'b1 : 1'b0)
             ---------------------1---------------------

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

 LINE       286
 SUB-EXPRESSION ((sent_message + 1'b1) == block_addr_limit)
                ---------------------1---------------------

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

 LINE       377
 EXPRESSION (msg_valid_i && msg_partial)
             -----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       388
 EXPRESSION (process_latched || process_i)
             -------1-------    ----2----

-1-	-2-	Status	Tests
0	0	Covered	T1,T2,T3
0	1	Covered	T1,T2,T3
1	0	Covered	T17,T18,T87

 LINE       418
 EXPRESSION (keccak_ack && end_of_block)
             -----1----    ------2-----

-1-	-2-	Status	Tests
0	1	Not Covered
1	0	Covered	T1,T2,T3
1	1	Covered	T13,T17,T18

 LINE       588
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------

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

 LINE       604
 EXPRESSION (msg_valid_i & ((~hold_msg)) & ((~en_msgbuf)))
             -----1-----   ------2------   -------3------

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

 LINE       616
 EXPRESSION (en_msgbuf | (keccak_ready_i & ((~hold_msg))))
             ----1----   ----------------2---------------

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

 LINE       616
 SUB-EXPRESSION (keccak_ready_i & ((~hold_msg)))
                 -------1------   ------2------

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

FSM Coverage for Instance : tb.dut.u_sha3.u_pad

**Summary for FSM :: st**
	Total	Covered	Percent
States	10	10	100.00	(Not included in score)
Transitions	17	16	94.12
Sequences	0	0

State, Transition and Sequence Details for FSM :: st

states	Line No.	Covered	Tests
StMessage	330	Covered	T1,T2,T3
StMessageWait	383	Covered	T1,T2,T3
StPad	389	Covered	T1,T2,T3
StPad01	427	Covered	T1,T2,T3
StPadFlush	435	Covered	T1,T2,T3
StPadIdle	333	Covered	T1,T2,T3
StPadRun	421	Covered	T13,T17,T18
StPrefix	328	Covered	T1,T2,T3
StPrefixWait	348	Covered	T1,T2,T3
StTerminalError	495	Covered	T4,T5,T6

transitions	Line No.	Covered	Tests	Exclude Annotation
StMessage->StMessageWait	383	Covered	T1,T2,T3
StMessage->StPad	389	Covered	T1,T2,T3
StMessage->StTerminalError	495	Covered	T4,T5,T69
StMessageWait->StMessage	403	Covered	T1,T2,T3
StMessageWait->StTerminalError	495	Covered	T6,T7,T68
StPad->StPad01	427	Covered	T1,T2,T3
StPad->StPadRun	421	Covered	T13,T17,T18
StPad->StTerminalError	495	Excluded	T47	[LOW_RISK] The transition from any state to error_terminal state is fully verified in FPV.
StPad01->StPadFlush	452	Covered	T1,T2,T3
StPad01->StTerminalError	495	Not Covered
StPadFlush->StPadIdle	470	Covered	T1,T2,T3
StPadFlush->StTerminalError	495	Excluded	T100	[LOW_RISK] The transition from any state to error_terminal state is fully verified in FPV.
StPadIdle->StMessage	330	Covered	T4,T13,T16
StPadIdle->StPrefix	328	Covered	T1,T2,T3
StPadIdle->StTerminalError	495	Covered	T9,T10,T11
StPadRun->StPadFlush	435	Covered	T13,T17,T18
StPadRun->StTerminalError	495	Excluded		[LOW_RISK] The transition from any state to error_terminal state is fully verified in FPV.
StPrefix->StPrefixWait	348	Covered	T1,T2,T3
StPrefix->StTerminalError	495	Excluded	T70,T71,T101	[LOW_RISK] The transition from any state to error_terminal state is fully verified in FPV.
StPrefixWait->StMessage	364	Covered	T1,T2,T3
StPrefixWait->StTerminalError	495	Covered	T8,T102

Branch Coverage for Instance : tb.dut.u_sha3.u_pad

	Line No.	Total	Covered	Percent
Branches		93	89	95.70
TERNARY	213	2	2	100.00
TERNARY	236	2	2	100.00
TERNARY	242	2	2	100.00
TERNARY	286	2	2	100.00
TERNARY	588	2	2	100.00
CASE	157	6	5	83.33
IF	267	4	4	100.00
IF	279	2	2	100.00
IF	293	2	2	100.00
CASE	316	23	22	95.65
IF	494	2	2	100.00
CASE	558	4	3	75.00
CASE	591	5	5	100.00
CASE	603	5	5	100.00
CASE	615	5	5	100.00
IF	664	4	4	100.00
IF	779	4	4	100.00
IF	788	4	4	100.00
IF	798	4	4	100.00
CASE	719	9	8	88.89



213          assign prefix_index = (sent_message < block_addr_limit) ? sent_message : '0;
                                                                     -1-  
                                                                     ==>  
                                                                     ==>

Branches:

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



236          assign mode_eq_cshake = (mode_i == CShake) ? 1'b 1 : 1'b 0;
                                                        -1-  
                                                        ==>  
                                                        ==>

Branches:

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



242          assign sent_blocksize = (sent_message == block_addr_limit) ? 1'b 1 : 1'b 0;
                                                                        -1-  
                                                                        ==>  
                                                                        ==>

Branches:

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



286          assign end_of_block = ((sent_message + 1'b1) == block_addr_limit) ? 1'b 1 : 1'b 0;
                                                                               -1-  
                                                                               ==>  
                                                                               ==>

Branches:

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



588          assign keccak_addr_o = (sent_message < block_addr_limit) ? sent_message : '0;
                                                                      -1-  
                                                                      ==>  
                                                                      ==>

Branches:

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



157            unique case (strength_i)
                      -1-  
158              L128: block_addr_limit = KeccakCountW'(KeccakRate[L128]);
                 ==>
159              L224: block_addr_limit = KeccakCountW'(KeccakRate[L224]);
                 ==>
160              L256: block_addr_limit = KeccakCountW'(KeccakRate[L256]);
                 ==>
161              L384: block_addr_limit = KeccakCountW'(KeccakRate[L384]);
                 ==>
162              L512: block_addr_limit = KeccakCountW'(KeccakRate[L512]);
                 ==>
163        
164              default: block_addr_limit = '0;
                 ==>

Branches:

-1-	Status	Tests
L128	Covered	T1,T2,T3
L224	Covered	T16,T62,T82
L256	Covered	T1,T2,T3
L384	Covered	T3,T13,T18
L512	Covered	T17,T62,T82
default	Not Covered



267            if (!rst_ni) begin
               -1-  
268              process_latched <= 1'b 0;
                 ==>
269            end else if (process_i) begin
                        -2-  
270              process_latched <= 1'b 1;
                 ==>
271            end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
                        -3-  
272              process_latched <= 1'b0;
                 ==>
273            end
               MISSING_ELSE
               ==>

Branches:

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



279          `PRIM_FLOP_SPARSE_FSM(u_state_regs, st_d, st, pad_st_e, StPadIdle)
             -1-                                                                  
             ==>                                                                  
             ==>

Branches:

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



293            if (!rst_ni) absorbed_o <= prim_mubi_pkg::MuBi4False;
               -1-  
               ==>
294            else         absorbed_o <= absorbed_d;
               ==>

Branches:

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



316            unique case (st)
                      -1-  
317        
318              // In Idle state, the FSM checks if the software (or upper FSM) initiates
319              // the hash process. If `start_i` is asserted (assume it is pulse), FSM
320              // starts to push the data into the keccak round logic. Depending on the
321              // hashing mode, FSM may push additional prefex in front of the actual
322              // message. It means, the message could be back-pressured until the first
323              // prefix is processed.
324              StPadIdle: begin
325                if (start_i) begin
                   -2-  
326                  // If cSHAKE, move to Prefix state
327                  if (mode_eq_cshake) begin
                     -3-  
328                    st_d = StPrefix;
                       ==>
329                  end else begin
330                    st_d = StMessage;
                       ==>
331                  end
332                end else begin
333                  st_d = StPadIdle;
                     ==>
334                end
335              end
336        
337              // At Prefix state, FSM pushes
338              // `bytepad(encode_string(N)||encode_string(S), 168or136)`. The software
339              // already prepared `encode_string(N) || encode_string(S)` in the regs.
340              // So, the FSM adds 2Byte in front of ns_data_i, which is an encoded
341              // block size (see `encoded_bytepad` below)
342              // After pushing the prefix, it initiates the hash process and move to
343              // Message state.
344              StPrefix: begin
345                sel_mux = MuxPrefix;
346        
347                if (sent_blocksize) begin
                   -4-  
348                  st_d = StPrefixWait;
                     ==>
349        
350                  keccak_run_o = 1'b 1;
351                  fsm_keccak_valid = 1'b 0;
352                  clr_sentmsg = 1'b 1;
353                end else begin
354                  st_d = StPrefix;
                     ==>
355        
356                  fsm_keccak_valid = 1'b 1;
357                end
358              end
359        
360              StPrefixWait: begin
361                sel_mux = MuxPrefix;
362        
363                if (keccak_complete_i) begin
                   -5-  
364                  st_d = StMessage;
                     ==>
365                end else begin
366                  st_d = StPrefixWait;
                     ==>
367                end
368              end
369        
370              // Message state pushes the incoming message into keccak round logic.
371              // It forwards the message while counting the data and if it reaches
372              // the block size, it triggers the keccak round to run. If `process` is
373              // set, it moves to Pad state.
374              StMessage: begin
375                sel_mux = MuxFifo;
376        
377                if (msg_valid_i && msg_partial) begin
                   -6-  
378                  st_d = StMessage;
                     ==>
379        
380                  en_msgbuf = 1'b 1;
381                end else if (sent_blocksize) begin
                            -7-  
382                  // Check block completion first even process is set.
383                  st_d = StMessageWait;
                     ==>
384        
385                  keccak_run_o = 1'b 1;
386                  clr_sentmsg = 1'b 1;
387                  hold_msg = 1'b 1;
388                end else if (process_latched || process_i) begin
                            -8-  
389                  st_d = StPad;
                     ==>
390        
391                  // Not asserting the msg_ready_o
392                  hold_msg = 1'b 1;
393                end else begin
394                  st_d = StMessage;
                     ==>
395        
396                end
397              end
398        
399              StMessageWait: begin
400                hold_msg = 1'b 1;
401        
402                if (keccak_complete_i) begin
                   -9-  
403                  st_d = StMessage;
                     ==>
404                end else begin
405                  st_d = StMessageWait;
                     ==>
406                end
407              end
408        
409              // Pad state just pushes the ending suffix. Depending on the mode, the
410              // padding value is unique. SHA3 adds 2'b10, SHAKE adds 4'b1111, and
411              // cSHAKE adds 2'b 00. Refer `function_pad`. The signal has one more bit
412              // defined to accomodate first 1 bit of `pad10*1()` function.
413              StPad: begin
414                sel_mux = MuxFuncPad;
415        
416                fsm_keccak_valid = 1'b 1;
417        
418                if (keccak_ack && end_of_block) begin
                   -10-  
419                  // If padding is the last block, don't have to move to StPad01, just
420                  // run Keccak and complete
421                  st_d = StPadRun;
                     ==>
422        
423                  // always clear the latched msgbuf
424                  clr_msgbuf = 1'b 1;
425                  clr_sentmsg = 1'b 1;
426                end else if (keccak_ack) begin
                            -11-  
427                  st_d = StPad01;
                     ==>
428                  clr_msgbuf = 1'b 1;
429                end else begin
430                  st_d = StPad;
                     ==>
431                end
432              end
433        
434              StPadRun: begin
435                st_d = StPadFlush;
                   ==>
436        
437                keccak_run_o = 1'b 1;
438                clr_sentmsg = 1'b 1;
439              end
440        
441              // Pad01 pushes the end bit of pad10*1() function. As keccak accepts byte
442              // size only, StPad always pushes partial (5bits). So at this state, it
443              // pushes rest of 3bits. If the data pushed in StPad is the last byte of
444              // the block, then Pad01 pushes to the same byte, if not, it first
445              // zero-fill the block then pad 1 to the end.
446              StPad01: begin
447                sel_mux = MuxZeroEnd;
448        
449                // There's no chance StPad01 can be a start of the block. So can be
450                // discard that the sent_blocksize is set at the beginning.
451                if (sent_blocksize) begin
                   -12-  
452                  st_d = StPadFlush;
                     ==>
453        
454                  fsm_keccak_valid = 1'b 0;
455                  keccak_run_o = 1'b 1;
456                  clr_sentmsg = 1'b 1;
457                end else begin
458                  st_d = StPad01;
                     ==>
459        
460                  fsm_keccak_valid = 1'b 1;
461                end
462              end
463        
464              StPadFlush: begin
465                // Wait completion from keccak_round or wait SW indicator.
466                clr_sentmsg = 1'b 1;
467                clr_msgbuf = 1'b 1;
468        
469                if (keccak_complete_i) begin
                   -13-  
470                  st_d = StPadIdle;
                     ==>
471        
472                  absorbed_d = prim_mubi_pkg::MuBi4True;
473                end else begin
474                  st_d = StPadFlush;
                     ==>
475                end
476              end
477        
478              StTerminalError: begin
479                // this state is terminal
480                st_d = st;
                   ==>
481                sparse_fsm_error_o = 1'b 1;
482              end
483        
484              default: begin
485                // this state is terminal
486                st_d = StTerminalError;
                   ==>

Branches:

-1-	-2-	-3-	-4-	-5-	-6-	-7-	-8-	-9-	-10-	-11-	-12-	-13-	Status	Tests
StPadIdle	1	1	-	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPadIdle	1	0	-	-	-	-	-	-	-	-	-	-	Covered	T4,T13,T16
StPadIdle	0	-	-	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefix	-	-	1	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefix	-	-	0	-	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefixWait	-	-	-	1	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StPrefixWait	-	-	-	0	-	-	-	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	1	-	-	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	0	1	-	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	0	0	1	-	-	-	-	-	Covered	T1,T2,T3
StMessage	-	-	-	-	0	0	0	-	-	-	-	-	Covered	T1,T2,T3
StMessageWait	-	-	-	-	-	-	-	1	-	-	-	-	Covered	T1,T2,T3
StMessageWait	-	-	-	-	-	-	-	0	-	-	-	-	Covered	T1,T2,T3
StPad	-	-	-	-	-	-	-	-	1	-	-	-	Covered	T13,T17,T18
StPad	-	-	-	-	-	-	-	-	0	1	-	-	Covered	T1,T2,T3
StPad	-	-	-	-	-	-	-	-	0	0	-	-	Not Covered
StPadRun	-	-	-	-	-	-	-	-	-	-	-	-	Covered	T13,T17,T18
StPad01	-	-	-	-	-	-	-	-	-	-	1	-	Covered	T1,T2,T3
StPad01	-	-	-	-	-	-	-	-	-	-	0	-	Covered	T1,T2,T3
StPadFlush	-	-	-	-	-	-	-	-	-	-	-	1	Covered	T1,T2,T3
StPadFlush	-	-	-	-	-	-	-	-	-	-	-	0	Covered	T1,T2,T3
StTerminalError	-	-	-	-	-	-	-	-	-	-	-	-	Covered	T4,T5,T6
default	-	-	-	-	-	-	-	-	-	-	-	-	Covered	T9,T10,T11



494            if (lc_ctrl_pkg::lc_tx_test_true_loose(lc_escalate_en_i)) begin
               -1-  
495              st_d = StTerminalError;
                 ==>
496            end
               MISSING_ELSE
               ==>

Branches:

-1-	Status	Tests
1	Covered	T4,T5,T6
0	Covered	T1,T2,T3



558            unique case (mode_i)
                      -1-  
559              Sha3:   funcpad = 5'b 00110;
                 ==>
560              Shake:  funcpad = 5'b 11111;
                 ==>
561              CShake: funcpad = 5'b 00100;
                 ==>
562        
563              default: begin
564                // Just create non-padding but pad10*1 only
565                funcpad = 5'b 00001;
                   ==>

Branches:

-1-	Status	Tests
Sha3	Covered	T1,T2,T3
Shake	Covered	T4,T15,T16
CShake	Covered	T1,T2,T3
default	Not Covered



591            unique case (sel_mux)
                      -1-  
592              MuxFifo:    keccak_data_o = msg_data_i;
                 ==>
593              MuxPrefix:  keccak_data_o = prefix_data;
                 ==>
594              MuxFuncPad: keccak_data_o = funcpad_data;
                 ==>
595              MuxZeroEnd: keccak_data_o = zero_with_endbit;
                 ==>
596        
597              // MuxNone
598              default:  keccak_data_o = '{default:'0};
                 ==>

Branches:

-1-	Status	Tests
MuxFifo	Covered	T1,T2,T3
MuxPrefix	Covered	T1,T2,T3
MuxFuncPad	Covered	T1,T2,T3
MuxZeroEnd	Covered	T1,T2,T3
default	Covered	T1,T2,T3



603            unique case (sel_mux)
                      -1-  
604              MuxFifo:    keccak_valid_o = msg_valid_i & ~hold_msg & ~en_msgbuf;
                 ==>
605              MuxPrefix:  keccak_valid_o = fsm_keccak_valid;
                 ==>
606              MuxFuncPad: keccak_valid_o = fsm_keccak_valid;
                 ==>
607              MuxZeroEnd: keccak_valid_o = fsm_keccak_valid;
                 ==>
608        
609              // MuxNone
610              default:  keccak_valid_o = 1'b 0;
                 ==>

Branches:

-1-	Status	Tests
MuxFifo	Covered	T1,T2,T3
MuxPrefix	Covered	T1,T2,T3
MuxFuncPad	Covered	T1,T2,T3
MuxZeroEnd	Covered	T1,T2,T3
default	Covered	T1,T2,T3



615            unique case (sel_mux)
                      -1-  
616              MuxFifo:    msg_ready_o = en_msgbuf | (keccak_ready_i & ~hold_msg);
                 ==>
617              MuxPrefix:  msg_ready_o = 1'b 0;
                 ==>
618              MuxFuncPad: msg_ready_o = 1'b 0;
                 ==>
619              MuxZeroEnd: msg_ready_o = 1'b 0;
                 ==>
620        
621              // MuxNone
622              default: msg_ready_o = 1'b 0;
                 ==>

Branches:

-1-	Status	Tests
MuxFifo	Covered	T1,T2,T3
MuxPrefix	Covered	T1,T2,T3
MuxFuncPad	Covered	T1,T2,T3
MuxZeroEnd	Covered	T1,T2,T3
default	Covered	T1,T2,T3



664            if (!rst_ni) begin
               -1-  
665              msg_buf  <= '{default:'0};
                 ==>
666              msg_strb <= '0;
667            end else if (en_msgbuf) begin
                        -2-  
668              for (int i = 0 ; i < Share ; i++) begin
                 ==>
669                msg_buf[i]  <= msg_data_i[i][0+:(MsgWidth-8)];
670              end
671              msg_strb <= msg_strb_i[0+:(MsgStrbW-1)];
672            end else if (clr_msgbuf) begin
                        -3-  
673              msg_buf  <= '{default:'0};
                 ==>
674              msg_strb <= '0;
675            end
               MISSING_ELSE
               ==>

Branches:

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



779            if (!rst_ni) begin
               -1-  
780              start_valid <= 1'b 1;
                 ==>
781            end else if (start_i) begin
                        -2-  
782              start_valid <= 1'b 0;
                 ==>
783            end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
                        -3-  
784              start_valid <= 1'b 1;
                 ==>
785            end
               MISSING_ELSE
               ==>

Branches:

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



788            if (!rst_ni) begin
               -1-  
789              process_valid <= 1'b 0;
                 ==>
790            end else if (start_i) begin
                        -2-  
791              process_valid <= 1'b 1;
                 ==>
792            end else if (process_i) begin
                        -3-  
793              process_valid <= 1'b 0;
                 ==>
794            end
               MISSING_ELSE
               ==>

Branches:

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



798            if (!rst_ni) begin
               -1-  
799              done_valid <= 1'b 0;
                 ==>
800            end else if (prim_mubi_pkg::mubi4_test_true_strict(absorbed_o)) begin
                        -2-  
801              done_valid <= 1'b 1;
                 ==>
802            end else if (prim_mubi_pkg::mubi4_test_true_strict(done_i)) begin
                        -3-  
803              done_valid <= 1'b 0;
                 ==>
804            end
               MISSING_ELSE
               ==>

Branches:

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



719              unique case (msg_strb)
                        -1-  
720                7'b 000_0000: funcpad_data[0] = {end_of_block, 63'(funcpad)                  };
                   ==>
721                7'b 000_0001: funcpad_data[0] = {end_of_block, 55'(funcpad), msg_buf[0][ 7:0]};
                   ==>
722                7'b 000_0011: funcpad_data[0] = {end_of_block, 47'(funcpad), msg_buf[0][15:0]};
                   ==>
723                7'b 000_0111: funcpad_data[0] = {end_of_block, 39'(funcpad), msg_buf[0][23:0]};
                   ==>
724                7'b 000_1111: funcpad_data[0] = {end_of_block, 31'(funcpad), msg_buf[0][31:0]};
                   ==>
725                7'b 001_1111: funcpad_data[0] = {end_of_block, 23'(funcpad), msg_buf[0][39:0]};
                   ==>
726                7'b 011_1111: funcpad_data[0] = {end_of_block, 15'(funcpad), msg_buf[0][47:0]};
                   ==>
727                7'b 111_1111: funcpad_data[0] = {end_of_block,  7'(funcpad), msg_buf[0][55:0]};
                   ==>
728        
729                default: funcpad_data = '{default:'0};
                   ==>

Branches:

-1-	Status	Tests
7'b0000000	Covered	T1,T2,T3
7'b0000001	Covered	T13,T16,T17
7'b0000011	Covered	T2,T3,T13
7'b0000111	Covered	T1,T12,T13
7'b0001111	Covered	T13,T16,T17
7'b0011111	Covered	T13,T16,T17
7'b0111111	Covered	T2,T3,T13
7'b1111111	Covered	T1,T12,T13
default	Not Covered

Assert Coverage for Instance : tb.dut.u_sha3.u_pad

	Total	Attempted	Percent	Succeeded/Matched	Percent
Assertions	22	22	100.00	22	100.00
Cover properties	4	4	100.00	4	100.00
Cover sequences	0	0		0
Total	26	26	100.00	26	100.00

Assertion Details

Name	Attempts	Real Successes	Failures	Incomplete
AbsorbedPulse_A	611077083	57058	0	0
AlwaysPartialMsgBuf_M	611077083	43666	0	0
CompleteBlockWhenProcess_A	611077083	54585	0	0
DoneCondition_M	611077083	57034	0	0
DonePulse_A	611077083	57034	0	0
KeccakAddrInRange_A	611077083	13860571	0	0
KeccakRunPulse_A	611077083	751060	0	0
MessageCondition_M	611077083	12579020	0	0
ModeStableDuringOp_M	611077083	32175	0	0
MsgReadyCondition_A	611077083	464791870	0	0
MsgWidthidth_A	665	665	0	0
NoPartialMsgFifo_M	611077083	12535354	0	0
Pad01NotAttheEndOfBlock_A	611077083	54847	0	0
PartialEndOfMsg_M	611077083	43666	0	0
PrefixLessThanBlock_A	665	665	0	0
ProcessCondition_M	611077083	57060	0	0
ProcessPulse_A	611077083	57060	0	0
StartCondition_M	611077083	57107	0	0
StartProcessDoneMutex_a	611077083	610944181	0	0
StartPulse_A	611077083	57107	0	0
StrengthStableDuringOp_M	611077083	38253	0	0
u_state_regs_A	611077083	610944181	0	0

AbsorbedPulse_A

Name	Attempts	Real Successes
Total	611077083	57058
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

AlwaysPartialMsgBuf_M

Name	Attempts	Real Successes
Total	611077083	43666
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	91
T14	5817	3
T15	46769	0
T16	0	49
T17	0	63
T18	0	43
T19	1332	0
T49	0	3

CompleteBlockWhenProcess_A

Name	Attempts	Real Successes
Total	611077083	54585
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	97
T14	5817	3
T15	46769	6
T16	0	57
T17	0	64
T18	0	76
T19	1332	0

DoneCondition_M

Name	Attempts	Real Successes
Total	611077083	57034
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

DonePulse_A

Name	Attempts	Real Successes
Total	611077083	57034
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

KeccakAddrInRange_A

Name	Attempts	Real Successes
Total	611077083	13860571
T1	7403	187
T2	7263	210
T3	16596	221
T4	2551	3
T5	3161	43
T12	2541	210
T13	117325	1378
T14	5817	210
T15	46769	306
T16	0	2744
T19	1332	0

KeccakRunPulse_A

Name	Attempts	Real Successes
Total	611077083	751060
T1	7403	11
T2	7263	10
T3	16596	13
T4	2551	0
T5	3161	2
T6	0	2
T12	2541	10
T13	117325	106
T14	5817	10
T15	46769	18
T16	0	143
T19	1332	0

MessageCondition_M

Name	Attempts	Real Successes
Total	611077083	12579020
T1	7403	104
T2	7263	91
T3	16596	182
T4	2551	3
T5	3161	22
T12	2541	91
T13	117325	728
T14	5817	91
T15	46769	102
T16	0	982
T19	1332	0

ModeStableDuringOp_M

Name	Attempts	Real Successes
Total	611077083	32175
T1	7403	1
T2	7263	1
T3	16596	3
T4	2551	1
T5	3161	1
T6	0	1
T12	2541	1
T13	117325	0
T14	5817	1
T15	46769	10
T16	0	21
T19	1332	0

MsgReadyCondition_A

Name	Attempts	Real Successes
Total	611077083	464791870
T1	7403	2865
T2	7263	2697
T3	16596	13827
T4	2551	198
T5	3161	52
T12	2541	369
T13	117325	50333
T14	5817	1473
T15	46769	43620
T16	0	15976
T19	1332	0

MsgWidthidth_A

Name	Attempts	Real Successes
Total	665	665
T1	1	1
T2	1	1
T3	1	1
T4	1	1
T5	1	1
T12	1	1
T13	1	1
T14	1	1
T15	1	1
T19	1	1

NoPartialMsgFifo_M

Name	Attempts	Real Successes
Total	611077083	12535354
T1	7403	101
T2	7263	88
T3	16596	180
T4	2551	3
T5	3161	22
T12	2541	88
T13	117325	637
T14	5817	88
T15	46769	102
T16	0	933
T19	1332	0

Pad01NotAttheEndOfBlock_A

Name	Attempts	Real Successes
Total	611077083	54847
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	97
T14	5817	3
T15	46769	6
T16	0	57
T17	0	65
T18	0	77
T19	1332	0

PartialEndOfMsg_M

Name	Attempts	Real Successes
Total	611077083	43666
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	91
T14	5817	3
T15	46769	0
T16	0	49
T17	0	63
T18	0	43
T19	1332	0
T49	0	3

PrefixLessThanBlock_A

Name	Attempts	Real Successes
Total	665	665
T1	1	1
T2	1	1
T3	1	1
T4	1	1
T5	1	1
T12	1	1
T13	1	1
T14	1	1
T15	1	1
T19	1	1

ProcessCondition_M

Name	Attempts	Real Successes
Total	611077083	57060
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

ProcessPulse_A

Name	Attempts	Real Successes
Total	611077083	57060
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T17	0	73
T18	0	80
T19	1332	0

StartCondition_M

Name	Attempts	Real Successes
Total	611077083	57107
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	1
T5	3161	1
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T19	1332	0

StartProcessDoneMutex_a

Name	Attempts	Real Successes
Total	611077083	610944181
T1	7403	7342
T2	7263	7183
T3	16596	16499
T4	2551	2410
T5	3161	2979
T12	2541	2464
T13	117325	117237
T14	5817	5728
T15	46769	46681
T19	1332	1240

StartPulse_A

Name	Attempts	Real Successes
Total	611077083	57107
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	1
T5	3161	1
T12	2541	3
T13	117325	105
T14	5817	3
T15	46769	6
T16	0	57
T19	1332	0

StrengthStableDuringOp_M

Name	Attempts	Real Successes
Total	611077083	38253
T1	7403	2
T2	7263	1
T3	16596	5
T4	2551	2
T5	3161	2
T12	2541	1
T13	117325	2
T14	5817	1
T15	46769	9
T19	1332	1

u_state_regs_A

Name	Attempts	Real Successes
Total	611077083	610944181
T1	7403	7342
T2	7263	7183
T3	16596	16499
T4	2551	2410
T5	3161	2979
T12	2541	2464
T13	117325	117237
T14	5817	5728
T15	46769	46681
T19	1332	1240

Cover Directives for Properties: Details

Name	Attempts	Matches	Incomplete
StComplete_C	611077083	1426472	0
StMessageFeed_C	611077083	465507142	0
StPadSendMsg_C	611077083	597376	0
StPad_C	611077083	54847	0

StComplete_C

Name	Attempts	Matches
Total	611077083	1426472
T1	7403	75
T2	7263	75
T3	16596	50
T4	2551	0
T5	3161	0
T12	2541	75
T13	117325	2625
T14	5817	75
T15	46769	150
T16	0	1425
T17	0	1825
T18	0	2000
T19	1332	0

StMessageFeed_C

Name	Attempts	Matches
Total	611077083	465507142
T1	7403	2873
T2	7263	2704
T3	16596	13838
T4	2551	198
T5	3161	53
T12	2541	376
T13	117325	50439
T14	5817	1480
T15	46769	43632
T16	0	16076
T19	1332	0

StPadSendMsg_C

Name	Attempts	Matches
Total	611077083	597376
T1	7403	32
T2	7263	56
T3	16596	5
T4	2551	0
T5	3161	0
T12	2541	56
T13	117325	636
T14	5817	56
T15	46769	96
T16	0	923
T17	0	296
T18	0	673
T19	1332	0

StPad_C

Name	Attempts	Matches
Total	611077083	54847
T1	7403	3
T2	7263	3
T3	16596	2
T4	2551	0
T5	3161	0
T12	2541	3
T13	117325	97
T14	5817	3
T15	46769	6
T16	0	57
T17	0	65
T18	0	77
T19	1332	0

SCORE	LINE	COND	TOGGLE	FSM	BRANCH	ASSERT	NAME
95.96	97.56	88.89		100.00	93.33	100.00	u_sha3