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 to exhaustively verify hardware using advanced algorithms and techniques.

In the spirit of open source, the open source EBMC is used here.

Step 1

Download and install my fork, specifically the vcd_for_all_cover branch to have the capability of generating waveform for each cover statement.

git clone --single-branch --branch vcd_for_all_cover https://github.com/ShashankVM/hw-cbmc/
cd hw-cbmc
git submodule init; git submodule update
make -C lib/cbmc/src minisat2-download
make -C src

Step 2

Clone my GitHub repo and run ebmc checker:

git clone https://github.com/ShashankVM/formal_verif_ecc
cd formal_verif_ecc
ebmc --systemverilog --top top top.sv rvecc_encode.sv channel_model.sv rvecc_decode.sv  --trace --vcd cover

Step 3

Install VSCode and Vaporview. Open the folder formal_verif_ecc in VSCode, and click on any VCD file to view trace in Vaporview.

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:

1. Assume the valid value for the first error position. This is specified in ASSUME_VALID_ERROR_POS1.

2. Assume the valid value for the second error position. This is specified in ASSUME_VALID_ERROR_POS2.

3. Assume that the first and second error positions are equal when in single error detection and correction mode. This is specified in ASSUME_SINGLE_ERROR_POSITION.

4. Assume that first and second error positions are not equal when in double error detection mode. This is specified in ASSUME_DOUBLE_ERROR_POSITION.

Assertions:

1. Prove that single_ecc_error becomes 1 if and only if single errors are injected and corrected. This is specified in 2 assertions: ASSERT_SINGLE_ECC and ASSERT_NO_SPURIOUS_SINGLE_ECC.

2. Prove that double_ecc_error becomes 1 if and only if double errors are injected and detected. This is specified in 2 assertions: ASSERT_DOUBLE_ED and ASSERT_NO_SPURIOUS_DOUBLE_ED.

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. This is specified in COVER_ALL_0.

2. Data is non-zero. This is specified in COVER_NON_0.

3. Few random error positions. These are specified in COVER_ERROR_0_POS, COVER_ERROR_38_POS, COVER_ERROR_9_POS, COVER_ERROR_24_POS.

4. Single error detection and correction. This is specified in COVER_SINGLE_ERROR_CORRECTION.

5. Double error detection. This is specified in COVER_DOUBLE_ERROR_DETECTION.

6. No error injection. This is specified in COVER_ERROR_INJECT_OFF.