sha512_acc regression in c8aa4673b: cannot hash entire mailbox

[korran]

With the latest RTL, our driver test sha384acc::test_digest_max_mailbox_size fails with the incorrect result:

# Update hw/latest/rtl submodule to the latest caliptra-rtl main
# Edit hw/verilated/Makefile to use hw/latest/rtl
# Run the sha384acc driver tests under verilator
kor@kor0:~/git/caliptra-sw$ cargo test -p caliptra-drivers test_sha384acc --features=verilator
     Running tests/drivers_integration_tests/main.rs (target/debug/deps/drivers_integration_tests-29cac2bfc77cc073)
      6,155 ready_for_fuses is high
      6,341 writing to cptra_bootfsm_go
     23,080 UART: sha384acc::test_kat...        [ok]
test test_sha384acc has been running for over 60 seconds
     26,688 UART: sha384acc::test_digest_max_mailbox_size...    [failed]
    490,125 UART: Error: panicked at 'assertion failed: `(left == right)`
    492,837 UART:   left: `Array4xN([3038056548, 4080830715, 3832216042, 1374833880, 483189301, 3233208662, 3509884325, 285359514, 588886280, 3410515659, 2445653093, 4084006627])`,
    507,571 UART:  right: `Array4xN([3402733031, 3287462480, 3009070987, 397918962, 702624952, 1643303102, 364370260, 1769076830, 3225446718, 1512186248, 2037906922, 1871310830])`', drivers/test-fw/src/bin/sha384acc_tests.rs:219:9
    525,569 UART: 
* TESTCASE FAILED
test test_sha384acc ... FAILED

The problem goes away when I revert this "lint cleanup" from src/soc_ifc/rtl/sha512_acc_top.sv.

$ git log -p src/soc_ifc/rtl/sha512_acc_top.sv
commit c8aa4673b2564d952e51549ef93b6539d9c0a65f
Author: Michael Norris <108370498+Nitsirks@users.noreply.github.com>
Date:   Fri Apr 26 14:13:30 2024 -0700

    Additional round of lint cleanup (#483)
    
    <snip too many squashed commits>


diff --git a/src/soc_ifc/rtl/sha512_acc_top.sv b/src/soc_ifc/rtl/sha512_acc_top.sv
index 79b5241..fbad8aa 100644
--- a/src/soc_ifc/rtl/sha512_acc_top.sv
+++ b/src/soc_ifc/rtl/sha512_acc_top.sv
@@ -305,8 +305,8 @@ always_comb core_digest_valid_q = core_digest_valid & ~(init_reg | next_reg);
   always_comb mbox_start_addr = hwif_out.START_ADDRESS.ADDR.value[MBOX_ADDR_W+1:2];
   always_comb mbox_ptr_round_up = (|hwif_out.DLEN.LENGTH.value[1:0]);
   //detect overflow of end address to indicate we want to read to the end of the mailbox
-  always_comb {mbox_read_to_end, mbox_end_addr} = mbox_ptr_round_up ? mbox_start_addr + (hwif_out.DLEN.LENGTH.value>>2) + 'd1 : 
-                                                                      mbox_start_addr + (hwif_out.DLEN.LENGTH.value>>2);
+  always_comb {mbox_read_to_end, mbox_end_addr} = mbox_ptr_round_up ? mbox_start_addr + MBOX_ADDR_W'(hwif_out.DLEN.LENGTH.value>>2) + 1'b1 : 
+                                                                      mbox_start_addr + MBOX_ADDR_W'(hwif_out.DLEN.LENGTH.value>>2);
   always_comb mbox_read_done = (sha_fsm_ps == SHA_IDLE) | ~mailbox_mode | 
                                //If the DLEN overflowed our end address, just read to the end of the mailbox and stop
                                //Otherwise read until read pointer == end address

How did this regression not get caught by formal equivalency analysis?

[calebofearth]

Fix is merged to main