Design and Verification of High Throughput Hamming Decoder

Introduction:

In coding theory, Hamming(7, 4) is a linear error-correcting code that encodes four bits of data into seven bits by adding three parity bits.

Source: https://en.wikipedia.org/wiki/Hamming(7, 4)

In this project, a High Throughput Hamming(7, 4) decoder capable of producing an output on every input is developed using time division multiplexing of 2 Meggitt decoders. It is implemented on Nexys A7 FPGA board and formally verified using HW CBMC.

Encoder output and decoder input is in Bit serial fashion, to support high speeds.

A simple Valid Ready protocol is used to synchronize encoder and decoder operation.

1. Encoder Design description:

• ready signal is high on the first cycle of operation.
• valid is high on every cycle of operation.
• Encoder output is bit serial, so that it can be used for transmitting data over a channel at high speeds.
• It uses a Parallel-In-Serial-Out to output data serially, on every cycle.

Encoder Finite State Machine:

• MESSAGE_0: first cycle of reading message first bit; syndrome calculation
• MESSAGE_1: second cycle of reading message second bit; syndrome calculation
• MESSAGE_2: third cycle of reading message third bit; syndrome calculation
• MESSAGE_3: fourth cycle of reading message fourth bit; syndrome calculation
• SYNDROME_0: Output syndrome first bit
• SYNDROME_1: Output syndrome second bit
• SYNDROME_2: Output syndrome third bit

2. Decoder Design Description:

• valid from encoder is connected to the decoder as an input. This is used to control state transition only if the valid input is High.
• valid output is high after any 1 bit errors are corrected.
• Syndrome is computed using a Linear Feedback Shift register.
• Combinatorial circuit is used to compute the position of the error from the generated Syndrome.
• It uses a serial input, so that it can be used for receiving data over a channel at high speeds.
• Output is converted to parallel format using a buffer register.
• Time division multiplexing of 2 Linear Feedback Shift Registers is used to obtain a valid output on every cycle.
• A sticky bit is used to identify the first valid output after reset.

Decoder Finite State Machine:

• DECODER_1_CALC_0: first cycle of decoder 1; error correction and output of decoder 2.
• DECODER_1_CALC_1: second cycle of decoder 1; reset decoder 2.
• DECODER_1_CALC_2: third cycle of decoder 1.
• DECODER_1_CALC_3: fourth cycle of decoder 1.
• DECODER_1_CALC_4: fifth cycle of decoder 1.
• DECODER_1_CALC_5: sixth cycle of decoder 1.
• DECODER_1_CALC_6: seventh cycle of decoder 1.
• DECODER_1_OUTPUT: error correction and output of decoder 1; first cycle of decoder 2
• DECODER_1_CLEAR : reset decoder 1. second cycle of decoder 2.
• DECODER_2_CALC_2: third cycle of decoder 2.
• DECODER_2_CALC_3: fourth cycle of decoder 2.
• DECODER_2_CALC_4: fifth cycle of decoder 2.
• DECODER_2_CALC_5: sixth cycle of decoder 2.
• DECODER_2_CALC_6: seventh cycle of decoder 2

3. Channel Model Design

• Model of a bit serial channel with Bit error rate = 1 Bit Error in a 7 bit codeword.
• Double bit errors are also possible.
• Error injection can be turned off.
• Channel model is used in both formal verification and prototyping on FPGA Board.

4. Formal Verification:

• Auxiliary model is written to sample transmitted code word. When encoder is ready, then the code word transmitted by the encoder is sampled. Error inject input is sampled into error_inject_reg when encoder is ready. The auxiliary model is synthesizable and used in the FPGA prototype.
• The final transmitted codeword, tx_final, for comparing with the received codeword, rx, is updated in the formal model only when encoder is ready and the receiver has valid output.

logic [6:0] tx_message,
              tx_final;

  logic error_inject_reg;

  always_ff @(posedge clk or posedge reset) begin
    if (reset) begin
      tx_message       <= 'b0;
      error_inject_reg <= 'b0;
    end else if (encoder_ready) begin
      tx_message       <= tx;
      error_inject_reg <= error_inject;
    end
  end

  always_comb begin
    if (encoder_ready && rx_valid)
      tx_final = tx;
    else
      tx_final = tx_message;
  end

• Assuming Message, error inject, error position inputs are stable throughout the duration that encoder ready is low.

ASSUME_STABLE_MESSAGE: assume property (@(posedge clk) disable iff (reset) $fell(encoder_ready) or !encoder_ready |-> $stable(message));

ASSUME_STABLE_ERROR_INJECT: assume property (@(posedge clk) disable iff (reset) $fell(encoder_ready) or !encoder_ready |-> $stable(error_inject));

ASSUME_STABLE_ERROR_POSITION1: assume property (@(posedge clk) disable iff (reset) $fell(encoder_ready) or !encoder_ready |-> $stable(error_pos1));

ASSUME_STABLE_ERROR_POSITION2: assume property (@(posedge clk) disable iff (reset) $fell(encoder_ready) or !encoder_ready |-> $stable(error_pos2));

• Assuming valid error positions, i.e. from 0th position to 6th position.

ASSUME_VALID_ERROR_POSITION1: assume property (@(posedge clk) disable iff (reset) error_pos1 < 3'd7);

ASSUME_VALID_ERROR_POSITION2: assume property (@(posedge clk) disable iff (reset) error_pos2 < 3'd7);

• Prove that the final transmitted codeword and received codeword are always equal in the absence of error injection.

ASSERT_RX_EQUAL_TX_NO_INJECTION: assert property (@(posedge clk) disable iff (reset) rx_valid && !error_inject_reg |-> (tx_final == rx));

• Prove that all single errors are corrected.

ASSERT_RX_EQUAL_TX_SINGLE_ERROR_WITH_INJECTION: assert property (@(posedge clk) disable iff (reset) rx_valid && ($past(error_pos1) == $past(error_pos2)) && error_inject_reg |-> (tx_final == rx));

• Prove that no double bit errors are corrected.

ASSERT_RX_NOT_EQUAL_TX_FOR_DOUBLE_ERROR: assert property (@(posedge clk) disable iff (reset) rx_valid && ($past(error_pos1) != $past(error_pos2)) && error_inject_reg |-> (tx_final != rx));

• Prove encoder has latency of 7 cycles.

ASSERT_ENCODER_LATENCY: assert property (@(posedge clk) disable iff (reset) $rose(encoder_ready) |-> ##7 encoder_ready);

• Prove decoder has latency of 7 cycles.

ASSERT_DECODER_LATENCY: assert property (@(posedge clk) disable iff (reset) $rose(rx_valid) |-> ##7 rx_valid);

• Prove errors are detected if and only if they are injected.

ASSERT_ERROR_DET_IF_ERROR_INJECT: assert property (@(posedge clk) disable iff (reset) rx_valid && error_inject_reg |-> error_det);

ASSERT_ERROR_DET_IMPLIES_ERROR_INJECT: assert property (@(posedge clk) disable iff (reset) error_det |-> error_inject_reg);

• Liveness property to prove that decoder's valid output goes high eventually. In other words, no input can cause system to hang.

ASSERT_RX_EVENTUALLY: assert property (@(posedge clk) disable iff (reset) s_eventually rx_valid);

• A few cover properties are written to ensure important design behaviors can be observed in the current formal environment.

COVER_ZERO_MESSAGE: cover property (@(posedge clk) disable iff (reset) (message == 4'b0000));

COVER_NON_ZERO_MESSAGE: cover property (@(posedge clk) disable iff (reset) (message != 4'b0000));

COVER_ERROR_INJECT_OFF: cover property (@(posedge clk) disable iff (reset) !error_inject ##9 error_inject);

COVER_ERROR_DET: cover property (@(posedge clk) disable iff (reset) error_det);

• Run command:

ebmc -D FORMAL --bound 100 --top dut dut.sv cc_encoder.sv piso.sv lfsr_encoder.sv cc_decoder_ht.sv lfsr_decoder.sv buffer_reg.sv error_correction_and_detection.sv channel.sv --reset reset==1 --vcd wave.vcd

• Results:

[dut.ASSUME_STABLE_MESSAGE] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.message)): ASSUMED 
[dut.ASSUME_STABLE_ERROR_INJECT] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.error_inject)): ASSUMED 
[dut.ASSUME_STABLE_ERROR_POSITION1] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.error_pos1)): ASSUMED 
[dut.ASSUME_STABLE_ERROR_POSITION2] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.error_pos2)): ASSUMED 
[dut.ASSUME_VALID_ERROR_POSITION1] always (disable iff (dut.reset) dut.error_pos1 < 3'b111): ASSUMED 
[dut.ASSUME_VALID_ERROR_POSITION2] always (disable iff (dut.reset) dut.error_pos2 < 3'b111): ASSUMED 
[dut.ASSERT_RX_EQUAL_TX_NO_INJECTION] always (disable iff (dut.reset) dut.rx_valid && !dut.error_inject_reg |-> dut.tx_final == dut.rx): PROVED up to bound 100 
[dut.ASSERT_RX_EQUAL_TX_SINGLE_ERROR_WITH_INJECTION] always (disable iff (dut.reset) dut.rx_valid && $past(dut.error_pos1) == $past(dut.error_pos2) && dut.error_inject_reg |-> dut.tx_final == dut.rx): PROVED up to bound 100 
[dut.ASSERT_RX_NOT_EQUAL_TX_FOR_DOUBLE_ERROR] always (disable iff (dut.reset) dut.rx_valid && $past(dut.error_pos1) != $past(dut.error_pos2) && dut.error_inject_reg |-> dut.tx_final != dut.rx): PROVED up to bound 100 
[dut.ASSERT_ENCODER_LATENCY] always (disable iff (dut.reset) $rose(dut.encoder_ready) |-> (##7 dut.encoder_ready)): PROVED up to bound 100 
[dut.ASSERT_DECODER_LATENCY] always (disable iff (dut.reset) $rose(dut.rx_valid) |-> (##7 dut.rx_valid)): PROVED up to bound 100 
[dut.ASSERT_ERROR_DET_IF_ERROR_INJECT] always (disable iff (dut.reset) dut.rx_valid && dut.error_inject_reg |-> dut.error_det): PROVED up to bound 100 
[dut.ASSERT_ERROR_DET_IMPLIES_ERROR_INJECT] always (disable iff (dut.reset) dut.error_det |-> dut.error_inject_reg): PROVED up to bound 100 
[dut.ASSERT_RX_EVENTUALLY] always (disable iff (dut.reset) s_eventually dut.rx_valid): PROVED up to bound 100 
[dut.COVER_ZERO_MESSAGE] cover (disable iff (dut.reset) dut.message == 4'b0): PROVED 
[dut.COVER_NON_ZERO_MESSAGE] cover (disable iff (dut.reset) dut.message != 4'b0): PROVED 
[dut.COVER_ERROR_INJECT_OFF] cover (disable iff (dut.reset) !dut.error_inject ##9 dut.error_inject): PROVED 
[dut.COVER_ERROR_DET] cover (disable iff (dut.reset) dut.error_det): PROVED 
[dut.COVER_NO_VACUOUS_PASS] cover (disable iff (dut.reset) dut.rx_valid && dut.error_inject_reg && dut.error_pos1 == dut.error_pos2 && dut.tx_final == dut.rx): PROVED

5. FPGA Prototyping

Constraints file:

https://github.com/ShashankVM/hamming_encoder_decoder_bmc/blob/master/Nexys-A7-100T-Master.xdc

Video demonstration on FPGA: