// Copyright lowRISC contributors (OpenTitan project).
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
//
// SECDED FPV assertion file generated by util/design/secded_gen.py

module prim_secded_inv_39_32_assert_fpv (
  input        clk_i,
  input        rst_ni,
  input [31:0] data_i,
  input [31:0] data_o,
  input [38:0] encoded_o,
  input [6:0] syndrome_o,
  input [1:0]  err_o,
  input [38:0] error_inject_i
);

  // Inject a maximum of two errors simultaneously.
  `ASSUME_FPV(MaxTwoErrors_M, $countones(error_inject_i) <= 2)
  // Single bit error detection
  `ASSERT(SingleErrorDetect_A, $countones(error_inject_i) == 1 |-> err_o[0])
  `ASSERT(SingleErrorDetectReverse_A, err_o[0] |-> $countones(error_inject_i) == 1)
  // Double bit error detection
  `ASSERT(DoubleErrorDetect_A, $countones(error_inject_i) == 2 |-> err_o[1])
  `ASSERT(DoubleErrorDetectReverse_A, err_o[1] |-> $countones(error_inject_i) == 2)
  // Single bit error correction (implicitly tests the syndrome output)
  `ASSERT(SingleErrorCorrect_A, $countones(error_inject_i) < 2 |-> data_i == data_o)
  // Basic syndrome check
  `ASSERT(SyndromeCheck_A, |syndrome_o |-> $countones(error_inject_i) > 0)
  `ASSERT(SyndromeCheckReverse_A, $countones(error_inject_i) > 0 |-> |syndrome_o)

  // Check that all-one and all-zero data does not result in all-one or all-zero codewords
  `ASSERT(AllZerosCheck_A, data_i == '0 |-> encoded_o != '0)
  `ASSERT(AllOnesCheck_A, data_i == '1 |-> encoded_o != '1)


endmodule : prim_secded_inv_39_32_assert_fpv
