Overview of RVECC:

RVECC encoder has a 32-bit data input (din) and generates a 7-bit output syndrome (ecc_out).

The 7-bit output syndrome is prepended to the data and sent through the channel.

The output of the channel is sent to the RVECC Decoder. The ecc_out of the encoder gets sent to the ecc_in of the decoder.

RVECC Decoder corrects single-bit errors and outputs the corrected 32-bit data (dout). The single_ecc_error output goes high when a single error is detected and corrected. The double_ecc_error output goes high when a double error is detected.

RVECC decoder can operate in one of 2 operating modes:

1. Single Error Detection and Correction. (sed_ded = 0)

2. Double Error Detection. (sed_ded = 1)

Channel Model:

A channel model with error injection functionality is designed. When sed_ded is 0, only 1 error is injected and when sed_ded is 1, 2 errors are injected.

Error is injected by inverting the bit at the error position.

Assumptions:

ASSUME_VALID_ERROR_POS1: Assumes the valid value for the first error position.

ASSUME_VALID_ERROR_POS2: Assumes the valid value for the first error position and also assumes that error positions 1 & 2 are not equal

ASSUME_DECODER_ENABLE: Assuming decoder enable to be high so that decoder is enabled.

Assertions:

ASSERT_ERROR_PRESENT: Proving that the encoder output is not equal to the data received by the decoder, that is, error is always injected by the channel model.

ASSERT_DATA_RECOVERED: For the single-bit error correcting case, prove that the original data is recovered.

ASSERT_SINGLE_ECC: Prove that the single_ecc_error output goes high when single bit errors are injected.

ASSERT_NO_DOUBLE_ED: Prove that no double errors detected when single bit errors are injected, i.e. double_ecc_error remains low.

ASSERT_DATA_NOT_RECOVERED: For the double-bit error detection case, prove that the original data is not recovered.

ASSERT_NO_SINGLE_ECC: Prove that the single_ecc_error output remains low when double bit errors are injected.

ASSERT_DOUBLE_ED: Prove that the double_ecc_error output goes high when double bit errors are injected.

Cover statements:

Cover statements are written to view traces of properties of a few cases, to ensure we haven't over-constrained our inputs.

1. Data is zero.

2. Data is non-zero.

3. Few random error positions.

4. Single error detection and correction.

5. Double error detection.