[entropy_src] Add SVA to ensure FIFOs are empty when triggering SHA

If any of the postht, distr or precon FIFOs are non-empty when
triggering the conditioner, there is risk of leaving entropy bits tested
as part of the current window inside the pipeline instead of absorbing
them into the current seed. This would be problematic.

This is related to #21855.

Signed-off-by: Pirmin Vogel <[email protected]>

hw/ip/entropy_src/rtl/entropy_src_core.sv

@@ -3465,6 +3465,20 @@ module entropy_src_core import entropy_src_pkg::*; #(
       precon_post_startup_exp_push_bit_cnt_q  <= precon_post_startup_exp_push_bit_cnt_d;
     end
   end
+
+  // When triggering the conditioner, the precon FIFO must be empty. The postht and distr FIFOs
+  // must have been empty in the cycle before. Otherwise, some entropy bits tested as part of the
+  // current window won't make into the corresponding seed.
+  //
+  // In Firmware Override: Extract & Insert mode, we don't care as firmware is responsible for
+  // filling the precon FIFO and for triggering the conditioner:
+  // - If the conditioner is triggered without the precon FIFO being empty, a recoverable alert is
+  //   signaled.
+  // - The fill levels of the postht and distr FIFOs are irrelevant for the conditioner in this
+  //   mode.
+  `ASSERT(FifosEmptyWhenShaProcess_A,
+      !fw_ov_mode_entropy_insert && $rose(sha3_process) |->
+      $past(!pfifo_postht_not_empty) && $past(!sfifo_distr_not_empty) && !pfifo_precon_not_empty)
 `endif
 
 endmodule