[hmac, rtl] Increase coverage through minor RTL restructure

[andrea-caforio]

In light of the V3 signoff, this commits adapts certain RTL parts that induced uncoverable coverage holes. There are two types of changes:

1. Removal of dangling else branches that are impossible to cover.
2. Removal of uncoverable FSM default state assignments.

Both changes have no functional impact and are only cosmetic in nature in order to attain the demanded coverage thresholds. See #24692, for a detailed discussion of these changes.

[rswarbrick]

I'm not sure I understand this change: why couldn't this be part of the else if chain that's there already?

[andrea-caforio]

By writing it this way, an uncovered line and branch can be avoided in the else branch.

  always_comb begin: assign_sha_message_length
    sha_msg_len = '0;
    if (!hmac_en_i) begin
      // ...
    end else if (sel_msglen == SelIPadMsg) begin
      // ...
    end else if (sel_msglen == SelOPadMsg) begin
      // ...
    end else
      sha_msg_len = '0; // <===== uncovered line and branch
  end

[rswarbrick]

I agree, but I think started with something like this:

if A begin:
  ...
end else if B begin:
  ...
end else if C begin:
  ...
end else begin:
  ... // Not possible!
end

I'd agree with changing it to:

if A begin:
  ...
end else if B begin:
  ...
end else begin:
  ...
end

(and adding an assertion that says A || B || C somewhere).

But I think your change is turning it into:

if A begin:
  ...
end else begin
  if B begin:
    ...
  end else begin:
    ...
  end
end

(Or have I misunderstood something?)

[andrea-caforio]

You're right. I'll change it.

[rswarbrick]

I agree with this, but (again) it's probably worth sticking an assertion at the bottom that says the comment is always true :-)

[andrea-caforio]

Having added the assertion (looking at the new failing tests), I see now that the value of digest_size_i may not be SHA2_256, SHA2_384, or SHA2_512 when hmac_en_i is 1. It can also take the value SHA2_NONE. Checking with @martin-velay.

[rswarbrick]

This isn't really a review comment, but I'm interested! Why is this change needed?

[andrea-caforio]

Assigning a default state at the beginning of the FSM combinatorial block shows up as an uncovered FSM transition in the report.

[rswarbrick]

Ahah! That makes sense. Although don't we see the "transition" whenever we move to FifoIdle?

[andrea-caforio]

True, I don't understand why the default state assignment is marked as an uncovered transition.

[vogelpi]

IIRC the FSM transition is covered but the tool identifies the default case statement as having no effect.

[andrea-caforio]

To breathe some life into this, how about this strategy:

We only change one of the conditional SHA branches, SHA2_NONE can arise for the outer padding (see here).

 always_comb begin: assign_sha_message_length
    sha_msg_len = '0;
    if (!hmac_en_i) begin
      sha_msg_len = message_length_i;
    // HASH = (o_pad || HASH_INTERMEDIATE (i_pad || msg))
    // message length for HASH_INTERMEDIATE = block size (i_pad) + message length
    end else if (sel_msglen == SelIPadMsg) begin
        if (digest_size_i == SHA2_256) begin
          sha_msg_len = message_length_i + BlockSizeSHA256in64;
        end else if ((digest_size_i == SHA2_384) || (digest_size_i == SHA2_512)) begin
          sha_msg_len = message_length_i + BlockSizeSHA512in64;
        end else begin
          sha_msg_len = '0; // <== THIS LINE/BRANCH IS COVERED
        end
    end else begin // `SelOPadMsg`
      // message length for HASH = block size (o_pad) + HASH_INTERMEDIATE digest length
      if (digest_size_i == SHA2_256) begin
        sha_msg_len = BlockSizeSHA256in64 + 64'd256;
      end else if (digest_size_i == SHA2_384) begin
        sha_msg_len = BlockSizeSHA512in64 + 64'd384;
      end else begin // SHA512
        sha_msg_len = BlockSizeSHA512in64 + 64'd512;
      end
    end
  end

Keep the changes alongside assertions in prim_sha2.sv and prim_sha2_pad.sv. The digest size placeholder SHA2_NONE is never propagated down to the SHA2 primitive.

With this we have 100% line coverage. What's left are two exclusion agreed upon in #24692 for missing else branches in prim_sha2_pad.sv and the unreachability exclusions for the default FSM states (will be done by someone else). After that we'll have 100% line, branch and FSM coverage in compliance with the V3 milestone.

[andrea-caforio]

Can someone take a look at this?

There is one unrelated test sleep_pin_mio_dio_val_test_fpga_cw310_sival_rom_ext that keeps time-outing in the CI.

[vogelpi]

Thanks for the update @andrea-caforio. This looks mostly good but I have some comments regarding indentation and some of the assertions.

Also, what do you mean by:

the unreachability exclusions for the default FSM states

when talking about what's left? Can you elaborate on this please?

[vogelpi]

instead of sel_rdata != 2'b11 please write sel_rdata inside {SelIPad, SelOPad, SelFifo}. This more robust. The point of using an enum here is exactly to not care about the precise encoding.

[vogelpi]

The indentation is off here: it should be 2 spaces instead of 4.

[vogelpi]

I don't think this is really necessary as this is the default assignment (See line 208). Can you please confirm?

[andrea-caforio]

The tricky thing here is the fact that it is possible that digest_size_i == SHA2_NONE when hmac_en_i && sel_msglen == SelIPadMsg, which is incompatible with the assertion for the other branch sel_msglen == SelOPadMsg where digest_size_i == SHA2_NONE is an impossible value.
It's a rare occurrence but I've encountered it in some of the tests.

[vogelpi]

Ah now I understand. Thanks for explaining.

Can you please add a comment for that and correct the indentation?

[vogelpi]

This should be extended to also cover the case on Line 357. Because inc_txcount can be high without sel_data inside {Pad80, LenHi, LenLo}.

[andrea-caforio]

Thanks for the update @andrea-caforio. This looks mostly good but I have some comments regarding indentation and some of the assertions.

Also, what do you mean by:

the unreachability exclusions for the default FSM states

when talking about what's left? Can you elaborate on this please?

Thank you for the review @vogelpi. What I'm referring to here are uncovered branches with respect to the default FSM states. There are three of them:

1. opentitan/hw/ip/prim/rtl/prim_sha2.sv

   Line 378 in 140185f

   default: begin

2. opentitan/hw/ip/prim/rtl/prim_sha2_pad.sv

   Line 154 in 140185f

   default: begin

3. opentitan/hw/ip/prim/rtl/prim_sha2_pad.sv

   Line 335 in 140185f

   default: begin

All other FSM default states branches have been excluded in the hmac_unr_excl.el file. The three uncovered ones belong to FSMs that have been updated after the last time the hmac_unr_excl.el has been written, which made me think they will eventually also end up in there, once a new unreachability analysis is done.

[vogelpi]

Thanks for the update @andrea-caforio. This looks mostly good but I have some comments regarding indentation and some of the assertions.
Also, what do you mean by:

the unreachability exclusions for the default FSM states

when talking about what's left? Can you elaborate on this please?

Thank you for the review @vogelpi. What I'm referring to here are uncovered branches with respect to the default FSM states. There are three of them:

1. https://github.com/lowRISC/opentitan/blob/140185f6894b70fefa440d99c6e59d6b4a368676/hw/ip/prim/rtl/prim_sha2.sv#L378

2. https://github.com/lowRISC/opentitan/blob/140185f6894b70fefa440d99c6e59d6b4a368676/hw/ip/prim/rtl/prim_sha2_pad.sv#L154

3. https://github.com/lowRISC/opentitan/blob/140185f6894b70fefa440d99c6e59d6b4a368676/hw/ip/prim/rtl/prim_sha2_pad.sv#L335

All other FSM default states branches have been excluded in the hmac_unr_excl.el file. The three uncovered ones belong to FSMs that have been updated after the last time the hmac_unr_excl.el has been written, which made me think they will eventually also end up in there, once a new unreachability analysis is done.

Thanks this is now clear. For other and hardened modules/FSMs we trigger those default statements by injecting errors into the sparsely encoded FSM states. We don't do this here because the HMAC FSMs are not hardened. All clear now.