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

Module : sha3pad
SCORELINECONDTOGGLEFSMBRANCHASSERT
92.89 99.41 88.37 80.95 95.70 100.00

Source File(s) :
/workspaces/repo/scratch/os_regression_2024_08_31/kmac_masked-sim-vcs/default/sim-vcs/../src/lowrisc_ip_sha3_0.1/rtl/sha3pad.sv

Module self-instances :
NAMESCORELINECONDTOGGLEFSMBRANCHASSERT
tb.dut.u_sha3.u_pad 95.59 99.41 88.37 94.44 95.70 100.00



Module Instance : tb.dut.u_sha3.u_pad

Instance :
SCORELINECONDTOGGLEFSMBRANCHASSERT
95.59 99.41 88.37 94.44 95.70 100.00


Instance's subtree :
SCORELINECONDTOGGLEFSMBRANCHASSERT
96.34 99.45 88.37 100.00 94.44 95.79 100.00


Parent :
SCORELINECONDTOGGLEFSMBRANCHASSERTNAME
95.96 97.56 88.89 100.00 93.33 100.00 u_sha3


Subtrees :
NAMESCORELINECONDTOGGLEFSMBRANCHASSERT
u_prefix_slicer 100.00 100.00 100.00
u_sentmsg_count 100.00 100.00
u_state_regs 100.00 100.00 100.00 100.00

Line Coverage for Module : sha3pad
Line No.TotalCoveredPercent
TOTAL17016999.41
ALWAYS15766100.00
CONT_ASSIGN20911100.00
CONT_ASSIGN21311100.00
CONT_ASSIGN23611100.00
CONT_ASSIGN24211100.00
CONT_ASSIGN24711100.00
CONT_ASSIGN25711100.00
ALWAYS26766100.00
ALWAYS27933100.00
CONT_ASSIGN28611100.00
ALWAYS29333100.00
ALWAYS298767598.68
CONT_ASSIGN50911100.00
CONT_ASSIGN52011100.00
CONT_ASSIGN53811100.00
ALWAYS55844100.00
CONT_ASSIGN57811100.00
CONT_ASSIGN58811100.00
ALWAYS59155100.00
ALWAYS60355100.00
ALWAYS61555100.00
ALWAYS6641010100.00
ALWAYS6801717100.00
ALWAYS77966100.00
ALWAYS78866100.00
ALWAYS79866100.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: T48 T60 T62  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: T47 T7 T8  162 1/1 L512: block_addr_limit = KeccakCountW'(KeccakRate[L512]); Tests: T44 T45 T60  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 T17  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 T17  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 T10  328 1/1 st_d = StPrefix; Tests: T1 T2 T17  329 end else begin 330 1/1 st_d = StMessage; Tests: T10 T44 T45  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 T17  346 347 1/1 if (sent_blocksize) begin Tests: T1 T2 T17  348 1/1 st_d = StPrefixWait; Tests: T1 T2 T17  349 350 1/1 keccak_run_o = 1'b 1; Tests: T1 T2 T17  351 1/1 fsm_keccak_valid = 1'b 0; Tests: T1 T2 T17  352 1/1 clr_sentmsg = 1'b 1; Tests: T1 T2 T17  353 end else begin 354 1/1 st_d = StPrefix; Tests: T1 T2 T17  355 356 1/1 fsm_keccak_valid = 1'b 1; Tests: T1 T2 T17  357 end 358 end 359 360 StPrefixWait: begin 361 1/1 sel_mux = MuxPrefix; Tests: T1 T2 T17  362 363 1/1 if (keccak_complete_i) begin Tests: T1 T2 T17  364 1/1 st_d = StMessage; Tests: T1 T2 T17  365 end else begin 366 1/1 st_d = StPrefixWait; Tests: T1 T2 T17  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 T10  376 377 1/1 if (msg_valid_i && msg_partial) begin Tests: T1 T2 T10  378 1/1 st_d = StMessage; Tests: T1 T2 T17  379 380 1/1 en_msgbuf = 1'b 1; Tests: T1 T2 T17  381 1/1 end else if (sent_blocksize) begin Tests: T1 T2 T10  382 // Check block completion first even process is set. 383 1/1 st_d = StMessageWait; Tests: T1 T2 T17  384 385 1/1 keccak_run_o = 1'b 1; Tests: T1 T2 T17  386 1/1 clr_sentmsg = 1'b 1; Tests: T1 T2 T17  387 1/1 hold_msg = 1'b 1; Tests: T1 T2 T17  388 1/1 end else if (process_latched || process_i) begin Tests: T1 T2 T10  389 1/1 st_d = StPad; Tests: T1 T2 T17  390 391 // Not asserting the msg_ready_o 392 1/1 hold_msg = 1'b 1; Tests: T1 T2 T17  393 end else begin 394 1/1 st_d = StMessage; Tests: T1 T2 T10  395 396 end 397 end 398 399 StMessageWait: begin 400 1/1 hold_msg = 1'b 1; Tests: T1 T2 T17  401 402 1/1 if (keccak_complete_i) begin Tests: T1 T2 T17  403 1/1 st_d = StMessage; Tests: T1 T2 T17  404 end else begin 405 1/1 st_d = StMessageWait; Tests: T1 T2 T17  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 T17  415 416 1/1 fsm_keccak_valid = 1'b 1; Tests: T1 T2 T17  417 418 1/1 if (keccak_ack && end_of_block) begin Tests: T1 T2 T17  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: T44 T4 T45  422 423 // always clear the latched msgbuf 424 1/1 clr_msgbuf = 1'b 1; Tests: T44 T4 T45  425 1/1 clr_sentmsg = 1'b 1; Tests: T44 T4 T45  426 1/1 end else if (keccak_ack) begin Tests: T1 T2 T17  427 1/1 st_d = StPad01; Tests: T1 T2 T17  428 1/1 clr_msgbuf = 1'b 1; Tests: T1 T2 T17  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: T44 T4 T45  436 437 1/1 keccak_run_o = 1'b 1; Tests: T44 T4 T45  438 1/1 clr_sentmsg = 1'b 1; Tests: T44 T4 T45  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 T17  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 T17  452 1/1 st_d = StPadFlush; Tests: T1 T2 T17  453 454 1/1 fsm_keccak_valid = 1'b 0; Tests: T1 T2 T17  455 1/1 keccak_run_o = 1'b 1; Tests: T1 T2 T17  456 1/1 clr_sentmsg = 1'b 1; Tests: T1 T2 T17  457 end else begin 458 1/1 st_d = StPad01; Tests: T1 T2 T17  459 460 1/1 fsm_keccak_valid = 1'b 1; Tests: T1 T2 T17  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 T17  467 1/1 clr_msgbuf = 1'b 1; Tests: T1 T2 T17  468 469 1/1 if (keccak_complete_i) begin Tests: T1 T2 T17  470 1/1 st_d = StPadIdle; Tests: T1 T2 T17  471 472 1/1 absorbed_d = prim_mubi_pkg::MuBi4True; Tests: T1 T2 T17  473 end else begin 474 1/1 st_d = StPadFlush; Tests: T1 T2 T17  475 end 476 end 477 478 StTerminalError: begin 479 // this state is terminal 480 1/1 st_d = st; Tests: T10 T9 T19  481 1/1 sparse_fsm_error_o = 1'b 1; Tests: T10 T9 T19  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: T10 T9 T19  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 1/1 assign prefix_data[1] = prefix_sliced; Tests: T1 T2 T3  539 end else begin : gen_prefix_unmasked 540 // If Unmasked, only one share exists. 541 assign prefix_data[0] = prefix_sliced; 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: T3 T47 T10  561 1/1 CShake: funcpad = 5'b 00100; Tests: T1 T2 T47  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 1/1 assign zero_with_endbit[1][MsgWidth-1] = end_of_block; Tests: T1 T2 T3  579 assign zero_with_endbit[1][MsgWidth-2:0] = '0; 580 end else begin : gen_zeroend_unmasked 581 assign zero_with_endbit[0][MsgWidth-1] = end_of_block; 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 T10  593 1/1 MuxPrefix: keccak_data_o = prefix_data; Tests: T1 T2 T17  594 1/1 MuxFuncPad: keccak_data_o = funcpad_data; Tests: T1 T2 T17  595 1/1 MuxZeroEnd: keccak_data_o = zero_with_endbit; Tests: T1 T2 T17  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 T10  605 1/1 MuxPrefix: keccak_valid_o = fsm_keccak_valid; Tests: T1 T2 T17  606 1/1 MuxFuncPad: keccak_valid_o = fsm_keccak_valid; Tests: T1 T2 T17  607 1/1 MuxZeroEnd: keccak_valid_o = fsm_keccak_valid; Tests: T1 T2 T17  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 T10  617 1/1 MuxPrefix: msg_ready_o = 1'b 0; Tests: T1 T2 T17  618 1/1 MuxFuncPad: msg_ready_o = 1'b 0; Tests: T1 T2 T17  619 1/1 MuxZeroEnd: msg_ready_o = 1'b 0; Tests: T1 T2 T17  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 T17  669 1/1 msg_buf[i] <= msg_data_i[i][0+:(MsgWidth-8)]; Tests: T1 T2 T17  670 end 671 1/1 msg_strb <= msg_strb_i[0+:(MsgStrbW-1)]; Tests: T1 T2 T17  672 1/1 end else if (clr_msgbuf) begin Tests: T1 T2 T3  673 1/1 msg_buf <= '{default:'0}; Tests: T1 T2 T17  674 1/1 msg_strb <= '0; Tests: T1 T2 T17  675 end MISSING_ELSE 676 end 677 678 if (EnMasking) begin : gen_funcpad_data_masked 679 always_comb begin 680 1/1 unique case (msg_strb) Tests: T1 T2 T3  681 7'b 000_0000: begin 682 1/1 funcpad_data[0] = '0; Tests: T1 T2 T3  683 1/1 funcpad_data[1] = {end_of_block, 63'(funcpad) }; Tests: T1 T2 T3  684 end 685 7'b 000_0001: begin 686 1/1 funcpad_data[0] = {56'h0, msg_buf[0][ 7:0]}; Tests: T44 T45 T53  687 1/1 funcpad_data[1] = {end_of_block, 55'(funcpad), msg_buf[1][ 7:0]}; Tests: T44 T45 T53  688 end 689 7'b 000_0011: begin 690 1/1 funcpad_data[0] = {48'h0, msg_buf[0][15:0]}; Tests: T1 T17 T51  691 1/1 funcpad_data[1] = {end_of_block, 47'(funcpad), msg_buf[1][15:0]}; Tests: T1 T17 T51  692 end 693 7'b 000_0111: begin 694 1/1 funcpad_data[0] = {40'h0, msg_buf[0][23:0]}; Tests: T2 T49 T52  695 1/1 funcpad_data[1] = {end_of_block, 39'(funcpad), msg_buf[1][23:0]}; Tests: T2 T49 T52  696 end 697 7'b 000_1111: begin 698 1/1 funcpad_data[0] = {32'h0, msg_buf[0][31:0]}; Tests: T44 T45 T53  699 1/1 funcpad_data[1] = {end_of_block, 31'(funcpad), msg_buf[1][31:0]}; Tests: T44 T45 T53  700 end 701 7'b 001_1111: begin 702 1/1 funcpad_data[0] = {24'h0, msg_buf[0][39:0]}; Tests: T44 T45 T53  703 1/1 funcpad_data[1] = {end_of_block, 23'(funcpad), msg_buf[1][39:0]}; Tests: T44 T45 T53  704 end 705 7'b 011_1111: begin 706 1/1 funcpad_data[0] = {16'h0, msg_buf[0][47:0]}; Tests: T1 T17 T51  707 1/1 funcpad_data[1] = {end_of_block, 15'(funcpad), msg_buf[1][47:0]}; Tests: T1 T17 T51  708 end 709 7'b 111_1111: begin 710 1/1 funcpad_data[0] = { 8'h0, msg_buf[0][55:0]}; Tests: T2 T49 T52  711 1/1 funcpad_data[1] = {end_of_block, 7'(funcpad), msg_buf[1][55:0]}; Tests: T2 T49 T52  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 unique case (msg_strb) 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}; 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 T10  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 T17  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 T10  792 1/1 end else if (process_i) begin Tests: T1 T2 T3  793 1/1 process_valid <= 1'b 0; Tests: T1 T2 T17  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 T17  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 T17  804 end MISSING_ELSE

Cond Coverage for Module : sha3pad
TotalCoveredPercent
Conditions433888.37
Logical433888.37
Non-Logical00
Event00

 LINE       209
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------
-1--2-StatusTests
01CoveredT1,T2,T3
10Not Covered
11CoveredT1,T2,T17

 LINE       213
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------
-1-StatusTests
0CoveredT1,T2,T17
1CoveredT1,T2,T3

 LINE       236
 EXPRESSION ((mode_i == CShake) ? 1'b1 : 1'b0)
             ---------1--------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T47

 LINE       236
 SUB-EXPRESSION (mode_i == CShake)
                ---------1--------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T47

 LINE       242
 EXPRESSION ((sent_message == block_addr_limit) ? 1'b1 : 1'b0)
             -----------------1----------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       242
 SUB-EXPRESSION (sent_message == block_addr_limit)
                -----------------1----------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       247
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------
-1--2-StatusTests
01CoveredT1,T2,T3
10Not Covered
11CoveredT1,T2,T17

 LINE       257
 EXPRESSION ((&msg_strb_i) != 1'b1)
            -----------1-----------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T3

 LINE       286
 EXPRESSION (((sent_message + 1'b1) == block_addr_limit) ? 1'b1 : 1'b0)
             ---------------------1---------------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       286
 SUB-EXPRESSION ((sent_message + 1'b1) == block_addr_limit)
                ---------------------1---------------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       377
 EXPRESSION (msg_valid_i && msg_partial)
             -----1-----    -----2-----
-1--2-StatusTests
01CoveredT1,T2,T10
10CoveredT1,T2,T17
11CoveredT1,T2,T17

 LINE       388
 EXPRESSION (process_latched || process_i)
             -------1-------    ----2----
-1--2-StatusTests
00CoveredT1,T2,T10
01CoveredT1,T2,T17
10CoveredT44,T4,T45

 LINE       418
 EXPRESSION (keccak_ack && end_of_block)
             -----1----    ------2-----
-1--2-StatusTests
01Not Covered
10CoveredT1,T2,T17
11CoveredT44,T4,T45

 LINE       588
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------
-1-StatusTests
0CoveredT1,T2,T17
1CoveredT1,T2,T3

 LINE       604
 EXPRESSION (msg_valid_i & ((~hold_msg)) & ((~en_msgbuf)))
             -----1-----   ------2------   -------3------
-1--2--3-StatusTests
011CoveredT1,T2,T10
101CoveredT4,T89,T80
110CoveredT1,T2,T17
111CoveredT1,T2,T17

 LINE       616
 EXPRESSION (en_msgbuf | (keccak_ready_i & ((~hold_msg))))
             ----1----   ----------------2---------------
-1--2-StatusTests
00CoveredT1,T2,T17
01CoveredT1,T2,T10
10Not Covered

 LINE       616
 SUB-EXPRESSION (keccak_ready_i & ((~hold_msg)))
                 -------1------   ------2------
-1--2-StatusTests
01Not Covered
10CoveredT1,T2,T17
11CoveredT1,T2,T10

FSM Coverage for Module : sha3pad
Summary for FSM :: st
TotalCoveredPercent
States 10 10 100.00 (Not included in score)
Transitions 21 17 80.95
Sequences 0 0

State, Transition and Sequence Details for FSM :: st
statesLine No.CoveredTests
StMessage 330 Covered T1,T2,T10
StMessageWait 383 Covered T1,T2,T17
StPad 389 Covered T1,T2,T17
StPad01 427 Covered T1,T2,T17
StPadFlush 435 Covered T1,T2,T17
StPadIdle 333 Covered T1,T2,T3
StPadRun 421 Covered T44,T4,T45
StPrefix 328 Covered T1,T2,T17
StPrefixWait 348 Covered T1,T2,T17
StTerminalError 495 Covered T10,T9,T19


transitionsLine No.CoveredTests
StMessage->StMessageWait 383 Covered T1,T2,T17
StMessage->StPad 389 Covered T1,T2,T17
StMessage->StTerminalError 495 Covered T10,T9,T38
StMessageWait->StMessage 403 Covered T1,T2,T17
StMessageWait->StTerminalError 495 Covered T43,T72,T68
StPad->StPad01 427 Covered T1,T2,T17
StPad->StPadRun 421 Covered T44,T4,T45
StPad->StTerminalError 495 Not Covered
StPad01->StPadFlush 452 Covered T1,T2,T17
StPad01->StTerminalError 495 Not Covered
StPadFlush->StPadIdle 470 Covered T1,T2,T17
StPadFlush->StTerminalError 495 Not Covered
StPadIdle->StMessage 330 Covered T10,T44,T45
StPadIdle->StPrefix 328 Covered T1,T2,T17
StPadIdle->StTerminalError 495 Covered T39,T40,T41
StPadRun->StPadFlush 435 Covered T44,T4,T45
StPadRun->StTerminalError 495 Not Covered
StPrefix->StPrefixWait 348 Covered T1,T2,T17
StPrefix->StTerminalError 495 Covered T93
StPrefixWait->StMessage 364 Covered T1,T2,T17
StPrefixWait->StTerminalError 495 Covered T19,T69,T70



Branch Coverage for Module : sha3pad
Line No.TotalCoveredPercent
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 680 9 8 88.89


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

Branches:
-1-StatusTests
1 Covered T1,T2,T3
0 Covered T1,T2,T17


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

Branches:
-1-StatusTests
1 Covered T1,T2,T47
0 Covered T1,T2,T3


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

Branches:
-1-StatusTests
1 Covered T1,T2,T17
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-StatusTests
1 Covered T1,T2,T17
0 Covered T1,T2,T3


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

Branches:
-1-StatusTests
1 Covered T1,T2,T3
0 Covered T1,T2,T17


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-StatusTests
L128 Covered T1,T2,T3
L224 Covered T48,T60,T62
L256 Covered T1,T2,T3
L384 Covered T47,T7,T8
L512 Covered T44,T45,T60
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T17
0 0 1 Covered T1,T2,T17
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-StatusTests
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-StatusTests
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-StatusTests
StPadIdle 1 1 - - - - - - - - - - Covered T1,T2,T17
StPadIdle 1 0 - - - - - - - - - - Covered T10,T44,T45
StPadIdle 0 - - - - - - - - - - - Covered T1,T2,T3
StPrefix - - 1 - - - - - - - - - Covered T1,T2,T17
StPrefix - - 0 - - - - - - - - - Covered T1,T2,T17
StPrefixWait - - - 1 - - - - - - - - Covered T1,T2,T17
StPrefixWait - - - 0 - - - - - - - - Covered T1,T2,T17
StMessage - - - - 1 - - - - - - - Covered T1,T2,T17
StMessage - - - - 0 1 - - - - - - Covered T1,T2,T17
StMessage - - - - 0 0 1 - - - - - Covered T1,T2,T17
StMessage - - - - 0 0 0 - - - - - Covered T1,T2,T10
StMessageWait - - - - - - - 1 - - - - Covered T1,T2,T17
StMessageWait - - - - - - - 0 - - - - Covered T1,T2,T17
StPad - - - - - - - - 1 - - - Covered T44,T4,T45
StPad - - - - - - - - 0 1 - - Covered T1,T2,T17
StPad - - - - - - - - 0 0 - - Not Covered
StPadRun - - - - - - - - - - - - Covered T44,T4,T45
StPad01 - - - - - - - - - - 1 - Covered T1,T2,T17
StPad01 - - - - - - - - - - 0 - Covered T1,T2,T17
StPadFlush - - - - - - - - - - - 1 Covered T1,T2,T17
StPadFlush - - - - - - - - - - - 0 Covered T1,T2,T17
StTerminalError - - - - - - - - - - - - Covered T10,T9,T19
default - - - - - - - - - - - - Covered T39,T40,T41


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-StatusTests
1 Covered T10,T9,T19
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-StatusTests
Sha3 Covered T1,T2,T3
Shake Covered T3,T47,T10
CShake Covered T1,T2,T47
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-StatusTests
MuxFifo Covered T1,T2,T10
MuxPrefix Covered T1,T2,T17
MuxFuncPad Covered T1,T2,T17
MuxZeroEnd Covered T1,T2,T17
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-StatusTests
MuxFifo Covered T1,T2,T10
MuxPrefix Covered T1,T2,T17
MuxFuncPad Covered T1,T2,T17
MuxZeroEnd Covered T1,T2,T17
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-StatusTests
MuxFifo Covered T1,T2,T10
MuxPrefix Covered T1,T2,T17
MuxFuncPad Covered T1,T2,T17
MuxZeroEnd Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T17
0 0 1 Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T10
0 0 1 Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T10
0 0 1 Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T17
0 0 1 Covered T1,T2,T17
0 0 0 Covered T1,T2,T3


680 unique case (msg_strb) -1- 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}; ==>

Branches:
-1-StatusTests
7'b0000000 Covered T1,T2,T3
7'b0000001 Covered T44,T45,T53
7'b0000011 Covered T1,T17,T51
7'b0000111 Covered T2,T49,T52
7'b0001111 Covered T44,T45,T53
7'b0011111 Covered T44,T45,T53
7'b0111111 Covered T1,T17,T51
7'b1111111 Covered T2,T49,T52
default Not Covered


Assert Coverage for Module : sha3pad
TotalAttemptedPercentSucceeded/MatchedPercent
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

NameAttemptsReal SuccessesFailuresIncomplete
AbsorbedPulse_A 596020898 54882 0 0
AlwaysPartialMsgBuf_M 596020898 42921 0 0
CompleteBlockWhenProcess_A 596020898 52424 0 0
DoneCondition_M 596020898 54880 0 0
DonePulse_A 596020898 54880 0 0
KeccakAddrInRange_A 596020898 12449766 0 0
KeccakRunPulse_A 596020898 672013 0 0
MessageCondition_M 596020898 11197853 0 0
ModeStableDuringOp_M 596020898 32515 0 0
MsgReadyCondition_A 596020898 393945752 0 0
MsgWidthidth_A 665 665 0 0
NoPartialMsgFifo_M 596020898 11154932 0 0
Pad01NotAttheEndOfBlock_A 596020898 52786 0 0
PartialEndOfMsg_M 596020898 42921 0 0
PrefixLessThanBlock_A 665 665 0 0
ProcessCondition_M 596020898 54901 0 0
ProcessPulse_A 596020898 54901 0 0
StartCondition_M 596020898 54952 0 0
StartProcessDoneMutex_a 596020898 595854729 0 0
StartPulse_A 596020898 54952 0 0
StrengthStableDuringOp_M 596020898 39115 0 0
u_state_regs_A 596020898 595854729 0 0


AbsorbedPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54882 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

AlwaysPartialMsgBuf_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 42921 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 63 0 0
T45 0 63 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0
T53 0 91 0 0
T94 0 3 0 0

CompleteBlockWhenProcess_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 52424 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 17 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 64 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

DoneCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54880 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

DonePulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54880 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

KeccakAddrInRange_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 12449766 0 0
T1 5111 210 0 0
T2 8662 210 0 0
T3 1316 0 0 0
T7 0 714 0 0
T8 0 459 0 0
T9 0 23 0 0
T10 2544 0 0 0
T17 7433 187 0 0
T44 0 666 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 187 0 0
T50 2893 0 0 0
T51 0 210 0 0
T52 0 210 0 0

KeccakRunPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 672013 0 0
T1 5111 10 0 0
T2 8662 10 0 0
T3 1316 0 0 0
T7 0 42 0 0
T8 0 27 0 0
T9 0 1 0 0
T10 2544 0 0 0
T17 7433 11 0 0
T44 0 74 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 11 0 0
T50 2893 0 0 0
T51 0 10 0 0
T52 0 10 0 0

MessageCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 11197853 0 0
T1 5111 91 0 0
T2 8662 91 0 0
T3 1316 0 0 0
T7 0 238 0 0
T8 0 153 0 0
T9 0 2 0 0
T10 2544 0 0 0
T17 7433 104 0 0
T44 0 360 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 104 0 0
T50 2893 0 0 0
T51 0 91 0 0
T52 0 91 0 0

ModeStableDuringOp_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 32515 0 0
T1 5111 1 0 0
T2 8662 1 0 0
T3 1316 1 0 0
T9 0 2 0 0
T10 2544 1 0 0
T17 7433 1 0 0
T46 770 0 0 0
T47 1595 4 0 0
T48 3326 12 0 0
T49 10758 1 0 0
T50 2893 10 0 0

MsgReadyCondition_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 393945752 0 0
T1 5111 1697 0 0
T2 8662 1175 0 0
T3 1316 0 0 0
T7 0 110824 0 0
T8 0 56628 0 0
T9 0 17 0 0
T10 2544 39 0 0
T17 7433 2346 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3452 0 0
T50 2893 0 0 0
T51 0 349 0 0
T52 0 1826 0 0

MsgWidthidth_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 665 665 0 0
T1 1 1 0 0
T2 1 1 0 0
T3 1 1 0 0
T10 1 1 0 0
T17 1 1 0 0
T46 1 1 0 0
T47 1 1 0 0
T48 1 1 0 0
T49 1 1 0 0
T50 1 1 0 0

NoPartialMsgFifo_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 11154932 0 0
T1 5111 88 0 0
T2 8662 88 0 0
T3 1316 0 0 0
T7 0 238 0 0
T8 0 153 0 0
T9 0 2 0 0
T10 2544 0 0 0
T17 7433 101 0 0
T44 0 297 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 101 0 0
T50 2893 0 0 0
T51 0 88 0 0
T52 0 88 0 0

Pad01NotAttheEndOfBlock_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 52786 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 18 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 65 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

PartialEndOfMsg_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 42921 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 63 0 0
T45 0 63 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0
T53 0 91 0 0
T94 0 3 0 0

PrefixLessThanBlock_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 665 665 0 0
T1 1 1 0 0
T2 1 1 0 0
T3 1 1 0 0
T10 1 1 0 0
T17 1 1 0 0
T46 1 1 0 0
T47 1 1 0 0
T48 1 1 0 0
T49 1 1 0 0
T50 1 1 0 0

ProcessCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54901 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

ProcessPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54901 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

StartCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54952 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T7 0 14 0 0
T8 0 9 0 0
T9 0 1 0 0
T10 2544 1 0 0
T17 7433 3 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

StartProcessDoneMutex_a
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 595854729 0 0
T1 5111 5061 0 0
T2 8662 8577 0 0
T3 1316 1242 0 0
T10 2544 2407 0 0
T17 7433 7344 0 0
T46 770 695 0 0
T47 1595 1526 0 0
T48 3326 3230 0 0
T49 10758 10708 0 0
T50 2893 2823 0 0

StartPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54952 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T7 0 14 0 0
T8 0 9 0 0
T9 0 1 0 0
T10 2544 1 0 0
T17 7433 3 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

StrengthStableDuringOp_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 39115 0 0
T1 5111 1 0 0
T2 8662 1 0 0
T3 1316 1 0 0
T10 2544 2 0 0
T17 7433 2 0 0
T46 770 1 0 0
T47 1595 5 0 0
T48 3326 13 0 0
T49 10758 2 0 0
T50 2893 7 0 0

u_state_regs_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 595854729 0 0
T1 5111 5061 0 0
T2 8662 8577 0 0
T3 1316 1242 0 0
T10 2544 2407 0 0
T17 7433 7344 0 0
T46 770 695 0 0
T47 1595 1526 0 0
T48 3326 3230 0 0
T49 10758 10708 0 0
T50 2893 2823 0 0



Cover Directives for Properties: Details

NameAttemptsMatchesIncomplete
StComplete_C 596020898 5325466 0
StMessageFeed_C 596020898 394582600 0
StPadSendMsg_C 596020898 580262 0
StPad_C 596020898 52786 0


StComplete_C
NameAttemptsMatchesIncomplete
Total 596020898 5325466 0
T1 5111 291 0
T2 8662 291 0
T3 1316 0 0
T4 0 1843 0
T7 0 1358 0
T8 0 873 0
T10 2544 0 0
T17 7433 291 0
T44 0 7081 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 291 0
T50 2893 0 0
T51 0 291 0
T52 0 291 0

StMessageFeed_C
NameAttemptsMatchesIncomplete
Total 596020898 394582600 0
T1 5111 1704 0
T2 8662 1182 0
T3 1316 0 0
T7 0 110852 0
T8 0 56646 0
T9 0 17 0
T10 2544 39 0
T17 7433 2354 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 3460 0
T50 2893 0 0
T51 0 356 0
T52 0 1833 0

StPadSendMsg_C
NameAttemptsMatchesIncomplete
Total 596020898 580262 0
T1 5111 56 0
T2 8662 56 0
T3 1316 0 0
T4 0 168 0
T7 0 224 0
T8 0 144 0
T10 2544 0 0
T17 7433 32 0
T44 0 296 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 32 0
T50 2893 0 0
T51 0 56 0
T52 0 56 0

StPad_C
NameAttemptsMatchesIncomplete
Total 596020898 52786 0
T1 5111 3 0
T2 8662 3 0
T3 1316 0 0
T4 0 18 0
T7 0 14 0
T8 0 9 0
T10 2544 0 0
T17 7433 3 0
T44 0 65 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 3 0
T50 2893 0 0
T51 0 3 0
T52 0 3 0

Line Coverage for Instance : tb.dut.u_sha3.u_pad
Line No.TotalCoveredPercent
TOTAL17016999.41
ALWAYS15766100.00
CONT_ASSIGN20911100.00
CONT_ASSIGN21311100.00
CONT_ASSIGN23611100.00
CONT_ASSIGN24211100.00
CONT_ASSIGN24711100.00
CONT_ASSIGN25711100.00
ALWAYS26766100.00
ALWAYS27933100.00
CONT_ASSIGN28611100.00
ALWAYS29333100.00
ALWAYS298767598.68
CONT_ASSIGN50911100.00
CONT_ASSIGN52011100.00
CONT_ASSIGN53811100.00
ALWAYS55844100.00
CONT_ASSIGN57811100.00
CONT_ASSIGN58811100.00
ALWAYS59155100.00
ALWAYS60355100.00
ALWAYS61555100.00
ALWAYS6641010100.00
ALWAYS6801717100.00
ALWAYS77966100.00
ALWAYS78866100.00
ALWAYS79866100.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: T48 T60 T62  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: T47 T7 T8  162 1/1 L512: block_addr_limit = KeccakCountW'(KeccakRate[L512]); Tests: T44 T45 T60  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 T17  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 T17  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 T10  328 1/1 st_d = StPrefix; Tests: T1 T2 T17  329 end else begin 330 1/1 st_d = StMessage; Tests: T10 T44 T45  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 T17  346 347 1/1 if (sent_blocksize) begin Tests: T1 T2 T17  348 1/1 st_d = StPrefixWait; Tests: T1 T2 T17  349 350 1/1 keccak_run_o = 1'b 1; Tests: T1 T2 T17  351 1/1 fsm_keccak_valid = 1'b 0; Tests: T1 T2 T17  352 1/1 clr_sentmsg = 1'b 1; Tests: T1 T2 T17  353 end else begin 354 1/1 st_d = StPrefix; Tests: T1 T2 T17  355 356 1/1 fsm_keccak_valid = 1'b 1; Tests: T1 T2 T17  357 end 358 end 359 360 StPrefixWait: begin 361 1/1 sel_mux = MuxPrefix; Tests: T1 T2 T17  362 363 1/1 if (keccak_complete_i) begin Tests: T1 T2 T17  364 1/1 st_d = StMessage; Tests: T1 T2 T17  365 end else begin 366 1/1 st_d = StPrefixWait; Tests: T1 T2 T17  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 T10  376 377 1/1 if (msg_valid_i && msg_partial) begin Tests: T1 T2 T10  378 1/1 st_d = StMessage; Tests: T1 T2 T17  379 380 1/1 en_msgbuf = 1'b 1; Tests: T1 T2 T17  381 1/1 end else if (sent_blocksize) begin Tests: T1 T2 T10  382 // Check block completion first even process is set. 383 1/1 st_d = StMessageWait; Tests: T1 T2 T17  384 385 1/1 keccak_run_o = 1'b 1; Tests: T1 T2 T17  386 1/1 clr_sentmsg = 1'b 1; Tests: T1 T2 T17  387 1/1 hold_msg = 1'b 1; Tests: T1 T2 T17  388 1/1 end else if (process_latched || process_i) begin Tests: T1 T2 T10  389 1/1 st_d = StPad; Tests: T1 T2 T17  390 391 // Not asserting the msg_ready_o 392 1/1 hold_msg = 1'b 1; Tests: T1 T2 T17  393 end else begin 394 1/1 st_d = StMessage; Tests: T1 T2 T10  395 396 end 397 end 398 399 StMessageWait: begin 400 1/1 hold_msg = 1'b 1; Tests: T1 T2 T17  401 402 1/1 if (keccak_complete_i) begin Tests: T1 T2 T17  403 1/1 st_d = StMessage; Tests: T1 T2 T17  404 end else begin 405 1/1 st_d = StMessageWait; Tests: T1 T2 T17  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 T17  415 416 1/1 fsm_keccak_valid = 1'b 1; Tests: T1 T2 T17  417 418 1/1 if (keccak_ack && end_of_block) begin Tests: T1 T2 T17  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: T44 T4 T45  422 423 // always clear the latched msgbuf 424 1/1 clr_msgbuf = 1'b 1; Tests: T44 T4 T45  425 1/1 clr_sentmsg = 1'b 1; Tests: T44 T4 T45  426 1/1 end else if (keccak_ack) begin Tests: T1 T2 T17  427 1/1 st_d = StPad01; Tests: T1 T2 T17  428 1/1 clr_msgbuf = 1'b 1; Tests: T1 T2 T17  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: T44 T4 T45  436 437 1/1 keccak_run_o = 1'b 1; Tests: T44 T4 T45  438 1/1 clr_sentmsg = 1'b 1; Tests: T44 T4 T45  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 T17  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 T17  452 1/1 st_d = StPadFlush; Tests: T1 T2 T17  453 454 1/1 fsm_keccak_valid = 1'b 0; Tests: T1 T2 T17  455 1/1 keccak_run_o = 1'b 1; Tests: T1 T2 T17  456 1/1 clr_sentmsg = 1'b 1; Tests: T1 T2 T17  457 end else begin 458 1/1 st_d = StPad01; Tests: T1 T2 T17  459 460 1/1 fsm_keccak_valid = 1'b 1; Tests: T1 T2 T17  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 T17  467 1/1 clr_msgbuf = 1'b 1; Tests: T1 T2 T17  468 469 1/1 if (keccak_complete_i) begin Tests: T1 T2 T17  470 1/1 st_d = StPadIdle; Tests: T1 T2 T17  471 472 1/1 absorbed_d = prim_mubi_pkg::MuBi4True; Tests: T1 T2 T17  473 end else begin 474 1/1 st_d = StPadFlush; Tests: T1 T2 T17  475 end 476 end 477 478 StTerminalError: begin 479 // this state is terminal 480 1/1 st_d = st; Tests: T10 T9 T19  481 1/1 sparse_fsm_error_o = 1'b 1; Tests: T10 T9 T19  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: T10 T9 T19  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 1/1 assign prefix_data[1] = prefix_sliced; Tests: T1 T2 T3  539 end else begin : gen_prefix_unmasked 540 // If Unmasked, only one share exists. 541 assign prefix_data[0] = prefix_sliced; 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: T3 T47 T10  561 1/1 CShake: funcpad = 5'b 00100; Tests: T1 T2 T47  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 1/1 assign zero_with_endbit[1][MsgWidth-1] = end_of_block; Tests: T1 T2 T3  579 assign zero_with_endbit[1][MsgWidth-2:0] = '0; 580 end else begin : gen_zeroend_unmasked 581 assign zero_with_endbit[0][MsgWidth-1] = end_of_block; 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 T10  593 1/1 MuxPrefix: keccak_data_o = prefix_data; Tests: T1 T2 T17  594 1/1 MuxFuncPad: keccak_data_o = funcpad_data; Tests: T1 T2 T17  595 1/1 MuxZeroEnd: keccak_data_o = zero_with_endbit; Tests: T1 T2 T17  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 T10  605 1/1 MuxPrefix: keccak_valid_o = fsm_keccak_valid; Tests: T1 T2 T17  606 1/1 MuxFuncPad: keccak_valid_o = fsm_keccak_valid; Tests: T1 T2 T17  607 1/1 MuxZeroEnd: keccak_valid_o = fsm_keccak_valid; Tests: T1 T2 T17  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 T10  617 1/1 MuxPrefix: msg_ready_o = 1'b 0; Tests: T1 T2 T17  618 1/1 MuxFuncPad: msg_ready_o = 1'b 0; Tests: T1 T2 T17  619 1/1 MuxZeroEnd: msg_ready_o = 1'b 0; Tests: T1 T2 T17  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 T17  669 1/1 msg_buf[i] <= msg_data_i[i][0+:(MsgWidth-8)]; Tests: T1 T2 T17  670 end 671 1/1 msg_strb <= msg_strb_i[0+:(MsgStrbW-1)]; Tests: T1 T2 T17  672 1/1 end else if (clr_msgbuf) begin Tests: T1 T2 T3  673 1/1 msg_buf <= '{default:'0}; Tests: T1 T2 T17  674 1/1 msg_strb <= '0; Tests: T1 T2 T17  675 end MISSING_ELSE 676 end 677 678 if (EnMasking) begin : gen_funcpad_data_masked 679 always_comb begin 680 1/1 unique case (msg_strb) Tests: T1 T2 T3  681 7'b 000_0000: begin 682 1/1 funcpad_data[0] = '0; Tests: T1 T2 T3  683 1/1 funcpad_data[1] = {end_of_block, 63'(funcpad) }; Tests: T1 T2 T3  684 end 685 7'b 000_0001: begin 686 1/1 funcpad_data[0] = {56'h0, msg_buf[0][ 7:0]}; Tests: T44 T45 T53  687 1/1 funcpad_data[1] = {end_of_block, 55'(funcpad), msg_buf[1][ 7:0]}; Tests: T44 T45 T53  688 end 689 7'b 000_0011: begin 690 1/1 funcpad_data[0] = {48'h0, msg_buf[0][15:0]}; Tests: T1 T17 T51  691 1/1 funcpad_data[1] = {end_of_block, 47'(funcpad), msg_buf[1][15:0]}; Tests: T1 T17 T51  692 end 693 7'b 000_0111: begin 694 1/1 funcpad_data[0] = {40'h0, msg_buf[0][23:0]}; Tests: T2 T49 T52  695 1/1 funcpad_data[1] = {end_of_block, 39'(funcpad), msg_buf[1][23:0]}; Tests: T2 T49 T52  696 end 697 7'b 000_1111: begin 698 1/1 funcpad_data[0] = {32'h0, msg_buf[0][31:0]}; Tests: T44 T45 T53  699 1/1 funcpad_data[1] = {end_of_block, 31'(funcpad), msg_buf[1][31:0]}; Tests: T44 T45 T53  700 end 701 7'b 001_1111: begin 702 1/1 funcpad_data[0] = {24'h0, msg_buf[0][39:0]}; Tests: T44 T45 T53  703 1/1 funcpad_data[1] = {end_of_block, 23'(funcpad), msg_buf[1][39:0]}; Tests: T44 T45 T53  704 end 705 7'b 011_1111: begin 706 1/1 funcpad_data[0] = {16'h0, msg_buf[0][47:0]}; Tests: T1 T17 T51  707 1/1 funcpad_data[1] = {end_of_block, 15'(funcpad), msg_buf[1][47:0]}; Tests: T1 T17 T51  708 end 709 7'b 111_1111: begin 710 1/1 funcpad_data[0] = { 8'h0, msg_buf[0][55:0]}; Tests: T2 T49 T52  711 1/1 funcpad_data[1] = {end_of_block, 7'(funcpad), msg_buf[1][55:0]}; Tests: T2 T49 T52  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 unique case (msg_strb) 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}; 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 T10  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 T17  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 T10  792 1/1 end else if (process_i) begin Tests: T1 T2 T3  793 1/1 process_valid <= 1'b 0; Tests: T1 T2 T17  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 T17  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 T17  804 end MISSING_ELSE

Cond Coverage for Instance : tb.dut.u_sha3.u_pad
TotalCoveredPercent
Conditions433888.37
Logical433888.37
Non-Logical00
Event00

 LINE       209
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------
-1--2-StatusTests
01CoveredT1,T2,T3
10Not Covered
11CoveredT1,T2,T17

 LINE       213
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------
-1-StatusTests
0CoveredT1,T2,T17
1CoveredT1,T2,T3

 LINE       236
 EXPRESSION ((mode_i == CShake) ? 1'b1 : 1'b0)
             ---------1--------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T47

 LINE       236
 SUB-EXPRESSION (mode_i == CShake)
                ---------1--------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T47

 LINE       242
 EXPRESSION ((sent_message == block_addr_limit) ? 1'b1 : 1'b0)
             -----------------1----------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       242
 SUB-EXPRESSION (sent_message == block_addr_limit)
                -----------------1----------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       247
 EXPRESSION (keccak_valid_o & keccak_ready_i)
             -------1------   -------2------
-1--2-StatusTests
01CoveredT1,T2,T3
10Not Covered
11CoveredT1,T2,T17

 LINE       257
 EXPRESSION ((&msg_strb_i) != 1'b1)
            -----------1-----------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T3

 LINE       286
 EXPRESSION (((sent_message + 1'b1) == block_addr_limit) ? 1'b1 : 1'b0)
             ---------------------1---------------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       286
 SUB-EXPRESSION ((sent_message + 1'b1) == block_addr_limit)
                ---------------------1---------------------
-1-StatusTests
0CoveredT1,T2,T3
1CoveredT1,T2,T17

 LINE       377
 EXPRESSION (msg_valid_i && msg_partial)
             -----1-----    -----2-----
-1--2-StatusTests
01CoveredT1,T2,T10
10CoveredT1,T2,T17
11CoveredT1,T2,T17

 LINE       388
 EXPRESSION (process_latched || process_i)
             -------1-------    ----2----
-1--2-StatusTests
00CoveredT1,T2,T10
01CoveredT1,T2,T17
10CoveredT44,T4,T45

 LINE       418
 EXPRESSION (keccak_ack && end_of_block)
             -----1----    ------2-----
-1--2-StatusTests
01Not Covered
10CoveredT1,T2,T17
11CoveredT44,T4,T45

 LINE       588
 EXPRESSION ((sent_message < block_addr_limit) ? sent_message : '0)
             ----------------1----------------
-1-StatusTests
0CoveredT1,T2,T17
1CoveredT1,T2,T3

 LINE       604
 EXPRESSION (msg_valid_i & ((~hold_msg)) & ((~en_msgbuf)))
             -----1-----   ------2------   -------3------
-1--2--3-StatusTests
011CoveredT1,T2,T10
101CoveredT4,T89,T80
110CoveredT1,T2,T17
111CoveredT1,T2,T17

 LINE       616
 EXPRESSION (en_msgbuf | (keccak_ready_i & ((~hold_msg))))
             ----1----   ----------------2---------------
-1--2-StatusTests
00CoveredT1,T2,T17
01CoveredT1,T2,T10
10Not Covered

 LINE       616
 SUB-EXPRESSION (keccak_ready_i & ((~hold_msg)))
                 -------1------   ------2------
-1--2-StatusTests
01Not Covered
10CoveredT1,T2,T17
11CoveredT1,T2,T10

FSM Coverage for Instance : tb.dut.u_sha3.u_pad
Summary for FSM :: st
TotalCoveredPercent
States 10 10 100.00 (Not included in score)
Transitions 18 17 94.44
Sequences 0 0

State, Transition and Sequence Details for FSM :: st
statesLine No.CoveredTests
StMessage 330 Covered T1,T2,T10
StMessageWait 383 Covered T1,T2,T17
StPad 389 Covered T1,T2,T17
StPad01 427 Covered T1,T2,T17
StPadFlush 435 Covered T1,T2,T17
StPadIdle 333 Covered T1,T2,T3
StPadRun 421 Covered T44,T4,T45
StPrefix 328 Covered T1,T2,T17
StPrefixWait 348 Covered T1,T2,T17
StTerminalError 495 Covered T10,T9,T19


transitionsLine No.CoveredTestsExclude Annotation
StMessage->StMessageWait 383 Covered T1,T2,T17
StMessage->StPad 389 Covered T1,T2,T17
StMessage->StTerminalError 495 Covered T10,T9,T38
StMessageWait->StMessage 403 Covered T1,T2,T17
StMessageWait->StTerminalError 495 Covered T43,T72,T68
StPad->StPad01 427 Covered T1,T2,T17
StPad->StPadRun 421 Covered T44,T4,T45
StPad->StTerminalError 495 Excluded [LOW_RISK] The transition from any state to error_terminal state is fully verified in FPV.
StPad01->StPadFlush 452 Covered T1,T2,T17
StPad01->StTerminalError 495 Excluded [LOW_RISK] The transition from any state to error_terminal state is fully verified in FPV.
StPadFlush->StPadIdle 470 Covered T1,T2,T17
StPadFlush->StTerminalError 495 Not Covered
StPadIdle->StMessage 330 Covered T10,T44,T45
StPadIdle->StPrefix 328 Covered T1,T2,T17
StPadIdle->StTerminalError 495 Covered T39,T40,T41
StPadRun->StPadFlush 435 Covered T44,T4,T45
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,T17
StPrefix->StTerminalError 495 Covered T93
StPrefixWait->StMessage 364 Covered T1,T2,T17
StPrefixWait->StTerminalError 495 Covered T19,T69,T70



Branch Coverage for Instance : tb.dut.u_sha3.u_pad
Line No.TotalCoveredPercent
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 680 9 8 88.89


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

Branches:
-1-StatusTests
1 Covered T1,T2,T3
0 Covered T1,T2,T17


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

Branches:
-1-StatusTests
1 Covered T1,T2,T47
0 Covered T1,T2,T3


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

Branches:
-1-StatusTests
1 Covered T1,T2,T17
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-StatusTests
1 Covered T1,T2,T17
0 Covered T1,T2,T3


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

Branches:
-1-StatusTests
1 Covered T1,T2,T3
0 Covered T1,T2,T17


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-StatusTests
L128 Covered T1,T2,T3
L224 Covered T48,T60,T62
L256 Covered T1,T2,T3
L384 Covered T47,T7,T8
L512 Covered T44,T45,T60
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T17
0 0 1 Covered T1,T2,T17
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-StatusTests
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-StatusTests
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-StatusTests
StPadIdle 1 1 - - - - - - - - - - Covered T1,T2,T17
StPadIdle 1 0 - - - - - - - - - - Covered T10,T44,T45
StPadIdle 0 - - - - - - - - - - - Covered T1,T2,T3
StPrefix - - 1 - - - - - - - - - Covered T1,T2,T17
StPrefix - - 0 - - - - - - - - - Covered T1,T2,T17
StPrefixWait - - - 1 - - - - - - - - Covered T1,T2,T17
StPrefixWait - - - 0 - - - - - - - - Covered T1,T2,T17
StMessage - - - - 1 - - - - - - - Covered T1,T2,T17
StMessage - - - - 0 1 - - - - - - Covered T1,T2,T17
StMessage - - - - 0 0 1 - - - - - Covered T1,T2,T17
StMessage - - - - 0 0 0 - - - - - Covered T1,T2,T10
StMessageWait - - - - - - - 1 - - - - Covered T1,T2,T17
StMessageWait - - - - - - - 0 - - - - Covered T1,T2,T17
StPad - - - - - - - - 1 - - - Covered T44,T4,T45
StPad - - - - - - - - 0 1 - - Covered T1,T2,T17
StPad - - - - - - - - 0 0 - - Not Covered
StPadRun - - - - - - - - - - - - Covered T44,T4,T45
StPad01 - - - - - - - - - - 1 - Covered T1,T2,T17
StPad01 - - - - - - - - - - 0 - Covered T1,T2,T17
StPadFlush - - - - - - - - - - - 1 Covered T1,T2,T17
StPadFlush - - - - - - - - - - - 0 Covered T1,T2,T17
StTerminalError - - - - - - - - - - - - Covered T10,T9,T19
default - - - - - - - - - - - - Covered T39,T40,T41


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-StatusTests
1 Covered T10,T9,T19
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-StatusTests
Sha3 Covered T1,T2,T3
Shake Covered T3,T47,T10
CShake Covered T1,T2,T47
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-StatusTests
MuxFifo Covered T1,T2,T10
MuxPrefix Covered T1,T2,T17
MuxFuncPad Covered T1,T2,T17
MuxZeroEnd Covered T1,T2,T17
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-StatusTests
MuxFifo Covered T1,T2,T10
MuxPrefix Covered T1,T2,T17
MuxFuncPad Covered T1,T2,T17
MuxZeroEnd Covered T1,T2,T17
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-StatusTests
MuxFifo Covered T1,T2,T10
MuxPrefix Covered T1,T2,T17
MuxFuncPad Covered T1,T2,T17
MuxZeroEnd Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T17
0 0 1 Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T10
0 0 1 Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T10
0 0 1 Covered T1,T2,T17
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-StatusTests
1 - - Covered T1,T2,T3
0 1 - Covered T1,T2,T17
0 0 1 Covered T1,T2,T17
0 0 0 Covered T1,T2,T3


680 unique case (msg_strb) -1- 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}; ==>

Branches:
-1-StatusTests
7'b0000000 Covered T1,T2,T3
7'b0000001 Covered T44,T45,T53
7'b0000011 Covered T1,T17,T51
7'b0000111 Covered T2,T49,T52
7'b0001111 Covered T44,T45,T53
7'b0011111 Covered T44,T45,T53
7'b0111111 Covered T1,T17,T51
7'b1111111 Covered T2,T49,T52
default Not Covered


Assert Coverage for Instance : tb.dut.u_sha3.u_pad
TotalAttemptedPercentSucceeded/MatchedPercent
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

NameAttemptsReal SuccessesFailuresIncomplete
AbsorbedPulse_A 596020898 54882 0 0
AlwaysPartialMsgBuf_M 596020898 42921 0 0
CompleteBlockWhenProcess_A 596020898 52424 0 0
DoneCondition_M 596020898 54880 0 0
DonePulse_A 596020898 54880 0 0
KeccakAddrInRange_A 596020898 12449766 0 0
KeccakRunPulse_A 596020898 672013 0 0
MessageCondition_M 596020898 11197853 0 0
ModeStableDuringOp_M 596020898 32515 0 0
MsgReadyCondition_A 596020898 393945752 0 0
MsgWidthidth_A 665 665 0 0
NoPartialMsgFifo_M 596020898 11154932 0 0
Pad01NotAttheEndOfBlock_A 596020898 52786 0 0
PartialEndOfMsg_M 596020898 42921 0 0
PrefixLessThanBlock_A 665 665 0 0
ProcessCondition_M 596020898 54901 0 0
ProcessPulse_A 596020898 54901 0 0
StartCondition_M 596020898 54952 0 0
StartProcessDoneMutex_a 596020898 595854729 0 0
StartPulse_A 596020898 54952 0 0
StrengthStableDuringOp_M 596020898 39115 0 0
u_state_regs_A 596020898 595854729 0 0


AbsorbedPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54882 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

AlwaysPartialMsgBuf_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 42921 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 63 0 0
T45 0 63 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0
T53 0 91 0 0
T94 0 3 0 0

CompleteBlockWhenProcess_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 52424 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 17 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 64 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

DoneCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54880 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

DonePulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54880 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

KeccakAddrInRange_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 12449766 0 0
T1 5111 210 0 0
T2 8662 210 0 0
T3 1316 0 0 0
T7 0 714 0 0
T8 0 459 0 0
T9 0 23 0 0
T10 2544 0 0 0
T17 7433 187 0 0
T44 0 666 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 187 0 0
T50 2893 0 0 0
T51 0 210 0 0
T52 0 210 0 0

KeccakRunPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 672013 0 0
T1 5111 10 0 0
T2 8662 10 0 0
T3 1316 0 0 0
T7 0 42 0 0
T8 0 27 0 0
T9 0 1 0 0
T10 2544 0 0 0
T17 7433 11 0 0
T44 0 74 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 11 0 0
T50 2893 0 0 0
T51 0 10 0 0
T52 0 10 0 0

MessageCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 11197853 0 0
T1 5111 91 0 0
T2 8662 91 0 0
T3 1316 0 0 0
T7 0 238 0 0
T8 0 153 0 0
T9 0 2 0 0
T10 2544 0 0 0
T17 7433 104 0 0
T44 0 360 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 104 0 0
T50 2893 0 0 0
T51 0 91 0 0
T52 0 91 0 0

ModeStableDuringOp_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 32515 0 0
T1 5111 1 0 0
T2 8662 1 0 0
T3 1316 1 0 0
T9 0 2 0 0
T10 2544 1 0 0
T17 7433 1 0 0
T46 770 0 0 0
T47 1595 4 0 0
T48 3326 12 0 0
T49 10758 1 0 0
T50 2893 10 0 0

MsgReadyCondition_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 393945752 0 0
T1 5111 1697 0 0
T2 8662 1175 0 0
T3 1316 0 0 0
T7 0 110824 0 0
T8 0 56628 0 0
T9 0 17 0 0
T10 2544 39 0 0
T17 7433 2346 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3452 0 0
T50 2893 0 0 0
T51 0 349 0 0
T52 0 1826 0 0

MsgWidthidth_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 665 665 0 0
T1 1 1 0 0
T2 1 1 0 0
T3 1 1 0 0
T10 1 1 0 0
T17 1 1 0 0
T46 1 1 0 0
T47 1 1 0 0
T48 1 1 0 0
T49 1 1 0 0
T50 1 1 0 0

NoPartialMsgFifo_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 11154932 0 0
T1 5111 88 0 0
T2 8662 88 0 0
T3 1316 0 0 0
T7 0 238 0 0
T8 0 153 0 0
T9 0 2 0 0
T10 2544 0 0 0
T17 7433 101 0 0
T44 0 297 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 101 0 0
T50 2893 0 0 0
T51 0 88 0 0
T52 0 88 0 0

Pad01NotAttheEndOfBlock_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 52786 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 18 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 65 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

PartialEndOfMsg_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 42921 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 63 0 0
T45 0 63 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0
T53 0 91 0 0
T94 0 3 0 0

PrefixLessThanBlock_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 665 665 0 0
T1 1 1 0 0
T2 1 1 0 0
T3 1 1 0 0
T10 1 1 0 0
T17 1 1 0 0
T46 1 1 0 0
T47 1 1 0 0
T48 1 1 0 0
T49 1 1 0 0
T50 1 1 0 0

ProcessCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54901 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

ProcessPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54901 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T4 0 19 0 0
T7 0 14 0 0
T8 0 9 0 0
T10 2544 0 0 0
T17 7433 3 0 0
T44 0 73 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

StartCondition_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54952 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T7 0 14 0 0
T8 0 9 0 0
T9 0 1 0 0
T10 2544 1 0 0
T17 7433 3 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

StartProcessDoneMutex_a
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 595854729 0 0
T1 5111 5061 0 0
T2 8662 8577 0 0
T3 1316 1242 0 0
T10 2544 2407 0 0
T17 7433 7344 0 0
T46 770 695 0 0
T47 1595 1526 0 0
T48 3326 3230 0 0
T49 10758 10708 0 0
T50 2893 2823 0 0

StartPulse_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 54952 0 0
T1 5111 3 0 0
T2 8662 3 0 0
T3 1316 0 0 0
T7 0 14 0 0
T8 0 9 0 0
T9 0 1 0 0
T10 2544 1 0 0
T17 7433 3 0 0
T46 770 0 0 0
T47 1595 0 0 0
T48 3326 0 0 0
T49 10758 3 0 0
T50 2893 0 0 0
T51 0 3 0 0
T52 0 3 0 0

StrengthStableDuringOp_M
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 39115 0 0
T1 5111 1 0 0
T2 8662 1 0 0
T3 1316 1 0 0
T10 2544 2 0 0
T17 7433 2 0 0
T46 770 1 0 0
T47 1595 5 0 0
T48 3326 13 0 0
T49 10758 2 0 0
T50 2893 7 0 0

u_state_regs_A
NameAttemptsReal SuccessesFailuresIncomplete
Total 596020898 595854729 0 0
T1 5111 5061 0 0
T2 8662 8577 0 0
T3 1316 1242 0 0
T10 2544 2407 0 0
T17 7433 7344 0 0
T46 770 695 0 0
T47 1595 1526 0 0
T48 3326 3230 0 0
T49 10758 10708 0 0
T50 2893 2823 0 0



Cover Directives for Properties: Details

NameAttemptsMatchesIncomplete
StComplete_C 596020898 5325466 0
StMessageFeed_C 596020898 394582600 0
StPadSendMsg_C 596020898 580262 0
StPad_C 596020898 52786 0


StComplete_C
NameAttemptsMatchesIncomplete
Total 596020898 5325466 0
T1 5111 291 0
T2 8662 291 0
T3 1316 0 0
T4 0 1843 0
T7 0 1358 0
T8 0 873 0
T10 2544 0 0
T17 7433 291 0
T44 0 7081 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 291 0
T50 2893 0 0
T51 0 291 0
T52 0 291 0

StMessageFeed_C
NameAttemptsMatchesIncomplete
Total 596020898 394582600 0
T1 5111 1704 0
T2 8662 1182 0
T3 1316 0 0
T7 0 110852 0
T8 0 56646 0
T9 0 17 0
T10 2544 39 0
T17 7433 2354 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 3460 0
T50 2893 0 0
T51 0 356 0
T52 0 1833 0

StPadSendMsg_C
NameAttemptsMatchesIncomplete
Total 596020898 580262 0
T1 5111 56 0
T2 8662 56 0
T3 1316 0 0
T4 0 168 0
T7 0 224 0
T8 0 144 0
T10 2544 0 0
T17 7433 32 0
T44 0 296 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 32 0
T50 2893 0 0
T51 0 56 0
T52 0 56 0

StPad_C
NameAttemptsMatchesIncomplete
Total 596020898 52786 0
T1 5111 3 0
T2 8662 3 0
T3 1316 0 0
T4 0 18 0
T7 0 14 0
T8 0 9 0
T10 2544 0 0
T17 7433 3 0
T44 0 65 0
T46 770 0 0
T47 1595 0 0
T48 3326 0 0
T49 10758 3 0
T50 2893 0 0
T51 0 3 0
T52 0 3 0

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