Formal Verification of RVECC Error Correcting Code Hardware

RVECC is an RTL design from CHIPS Alliance, consisting of encoder and decoder for correcting all 1-bit errors and detecting all 2-bit errors.

To verify that it corrects all 1-bit errors and detects all 2-bit errors, one can simulate all combinations, which would be a large number for a 32-bit input. All possible 1-bit errors alone would be 32 (2^5) possible error positions multiplied by 2^32 input combinations: for a total of 2^37 combinations! And we haven't even added the combinations for 2-bit errors. Simulating so many combinations is very tedious. Enter Formal Verification, a verification methodology that solves this problem using advanced algorithms and techniques. In formal property verification, we constrain the tool to generate valid inputs using assumptions. Then we use model checking to check our assertions hold true for all valid inputs.

In the spirit of open source, the Open Source Software Suite version of Yosys is used here.

Step 1

Download and install Yosys and clone the GitHub repo.

Step 2

Run

sby -f ecc.sby

Step 3

View the traces in GTKWave by opening the VCD files present in ecc_witness/engine_0/.

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.