[kmac] Revise incorrect Assertion
When process_latched asserted and it is not the end of the block, the
assertion is to check if internal padding logic to complete the block
size or not by checking keccak_valid_o signal. If the time is the end of
the block transfer, padding logic will trigger `run` first and will padd
th rest of the bits in next block.
Current assertion precondition was wrong. `!end_of_block ||
!sent_blocksize` is always 1 as `end_of_block` and `sent_blocksize` are
always one cycle apart.
WHy not detected earlier?:
In previous commits (PRs), FPV only tested SHA3-256 algorithm with
fixed data pattern (Empty, 1 Word, or 3 bytes). So there was no
chance to hit this corner case. However, in KMAC top-level test, it
doesn't bound the data pattern or algorithm mode/strength **yet**.
So, the FPV tool was able to catch this condition.
Signed-off-by: Eunchan Kim <eunchan@opentitan.org>
diff --git a/hw/ip/kmac/rtl/sha3pad.sv b/hw/ip/kmac/rtl/sha3pad.sv
index c78a9e2..102fbec 100644
--- a/hw/ip/kmac/rtl/sha3pad.sv
+++ b/hw/ip/kmac/rtl/sha3pad.sv
@@ -766,7 +766,7 @@
// If not full block is written, the pad shall send message to keccak_round
// If it is end of the message, the state moves to StPad and send the request
`ASSERT(CompleteBlockWhenProcess_A,
- $rose(process_latched) && (!end_of_block || !sent_blocksize )
+ $rose(process_latched) && (!end_of_block && !sent_blocksize )
&& !(st inside {StPrefixWait, StMessageWait}) |-> ##[1:5] keccak_valid_o)
// If `process_i` is asserted, eventually sha3pad trigger run signal
`ASSERT(ProcessToRun_A, process_i |-> strong(##[2:$] keccak_run_o))
