Added Hamming-code based single-error correction encoder and decoder

crates/std/veryl/src/coding/linear_sec_decoder.veryl

@@ -0,0 +1,110 @@
+/// Decodes a Hamming encoded single-error-correcting bitvector into its closest word
+module linear_sec_decoder #(
+    /// Number of parity bits
+    param P: u32 = 4,
+    /// Length of codeword
+    param K: u32 = (1 << P) - 1,
+    /// Length of data
+    param N: u32 = K - P,
+) (
+    i_codeword: input  logic<K>,
+    o_word    : output logic<N>,
+    /// Set iff the input codeword had a detected and corrected single-bit error in it
+    o_corrected: output logic,
+
+) {
+    // 1-indexed codeword
+    let codeword          : logic<K + 1> = {i_codeword, 1'b0};
+    var codeword_corrected: logic<K + 1>;
+
+    var errors: logic<P>;
+
+    // Generate word from corrected codeword
+    for idx in 1..(K + 2) :g_create_word {
+        if !$onehot(idx) :g_data_bit {
+            local CEIL            : u32 = $clog2(idx);
+            local WORD_IDX        : u32 = idx - 1 - CEIL;
+            assign o_word[WORD_IDX] = codeword_corrected[idx];
+        }
+    }
+
+    // Check parities
+    // for k in 1..K + 1 :g_check_parities {
+    //     local ERROR_IDX: u32 = k - 1;
+    //     if $onehot(k) :g_error_check_parities {
+    //         var masked_bits    : logic<K + 1>;
+    //         assign masked_bits[0]  = 1'b0;
+    //         local ONE_IDX_SET_BIT: u32 = $clog2(k);
+    //         for idx in 1..K + 1 :g_check_bits {
+    //             if idx[ONE_IDX_SET_BIT] :g_take_parity {
+    //                 assign masked_bits[idx] = codeword[idx];
+    //             } else {
+    //                 assign masked_bits[idx] = 1'b0;
+    //             }
+    //         }
+    //         assign errors[ERROR_IDX] = ^masked_bits;
+    //     } else {
+    //         assign errors[ERROR_IDX] = 1'b0;
+    //     }
+    // }
+    for pbit in 1..P + 1 :g_check_parities {
+        local ONE_IDX_SET_BIT: u32          = pbit - 1;
+        var masked_bits    : logic<K + 1>;
+        assign masked_bits[0]  = 1'b0;
+        for idx in 1..K + 1 :g_check_bits {
+            if idx[ONE_IDX_SET_BIT] :g_take_parity {
+                assign masked_bits[idx] = codeword[idx];
+            } else {
+                assign masked_bits[idx] = 1'b0;
+            }
+        }
+        assign errors[ONE_IDX_SET_BIT] = ^masked_bits;
+    }
+    // for idx in 1..(K + 1) :g_check_parities {
+    //     if $onehot(idx) :g_is_onehot {
+    //         local ONE_IDX_SET_BIT: u32      = $clog2(idx);
+    //         var masked_bits    : logic<K>;
+    //         for idx2 in 1..(P + 1) :gen_mask {
+    //             if idx2[ONE_IDX_SET_BIT] :g_take_parity {
+    //                 assign masked_bits[idx2 - 1] = codeword[idx2];
+    //             } else {
+    //                 assign masked_bits[idx2 - 1] = 1'b0;
+    //             }
+    //         }
+    //         assign errors[ONE_IDX_SET_BIT] = ~^masked_bits;
+    //     }
+    // }
+
+    // Correct as needed
+    assign o_corrected = |errors;
+    always_comb {
+        codeword_corrected         =  codeword;
+        codeword_corrected[errors] ^= 1;
+    }
+}
+
+#[test(test_3_1_hamming_decode)]
+embed (inline) sv{{{
+module test_3_1_hamming_code;
+  bit o_word;
+  logic o_corrected;
+  logic [2:0] i_codeword;
+
+  std_linear_sec_decoder#(.P(2)) dut(.*);
+
+  initial begin
+    $monitor("word: %b\n", o_word, "cwrd: %3b\n", i_codeword,
+        "corrected: %b\n", o_corrected,
+        "errors: %b\n\n", dut.errors
+    );
+    i_codeword = 3'b111;
+    #1 assert(o_word == 1'b1);
+    i_codeword = 3'b000;
+    #1 assert(o_word == 1'b0);
+    i_codeword = 3'b010;
+    #1 assert(o_word == 1'b0 && o_corrected);
+    $finish;
+  end
+
+endmodule
+}}}

crates/std/veryl/src/coding/linear_sec_encoder.veryl

@@ -0,0 +1,73 @@
+/// Enocdes a vector for single-error correction using a linear Hamming code.
+module linear_sec_encoder #(
+    /// Number of parity bits
+    param P: u32 = 4,
+    /// Length of codeword
+    param K: u32 = (1 << P) - 1,
+    /// Length of data
+    param N: u32 = K - P,
+) (
+    i_word    : input  logic<N>,
+    o_codeword: output logic<K>,
+) {
+
+    // Generate H Matrix
+    var h: logic<P, K>;
+    for p in 0..P :gen_vector {
+        for k in 0..K :gen_bit {
+            local IDX    : u32 = k + 1;
+            assign h[p][k] = IDX[p];
+        }
+    }
+
+    // Move data from input word to its larger k-bit length vector
+    var codeword_data_only: logic<K>;
+    for k in 1..K + 1 :gen_move_data {
+        local CODEWORD_IDX: u32 = k - 1;
+        if !$onehot(k) :gen_move_data_bit {
+            local WORD_IDX                        : u32 = k - $clog2(k) - 1;
+            assign codeword_data_only[CODEWORD_IDX] = i_word[WORD_IDX];
+        } else {
+            assign codeword_data_only[CODEWORD_IDX] = 1'b0;
+        }
+    }
+
+    // Compute parity bits
+    var codeword_parity_only: logic<K>;
+    for p in 0..P :gen_parities {
+        local CODEWORD_IDX                      : u32 = (1 << p) - 1;
+        assign codeword_parity_only[CODEWORD_IDX] = ^(h[p] & codeword_data_only);
+    }
+    for k in 0..K :gen_zeros {
+        if !$onehot(k + 1) :gen_zero_bit {
+            assign codeword_parity_only[k] = 1'b0;
+        }
+    }
+
+    assign o_codeword = codeword_data_only | codeword_parity_only;
+}
+
+#[test(test_3_1_hamming_encode)]
+embed (inline) sv{{{
+module test_3_1_hamming_code;
+  bit i_word;
+  logic [2:0] o_codeword;
+
+  std_linear_sec_encoder#(.P(2)) dut(.*);
+
+  initial begin
+    $display("enc.h[0]: %b\n", dut.h[0]);
+    $display("enc.h[1]: %b\n", dut.h[1]);
+    $monitor("word: %b\n", i_word, "cwrd: %3b\n", o_codeword,
+    "cwrd_dataonly: %b\n", dut.codeword_data_only,
+    "cwrd_parionly: %b\n\n", dut.codeword_parity_only,
+    );
+    i_word = 1'b0;
+    #1 assert(o_codeword == 3'b000);
+    i_word = 1'b1;
+    #1 assert(o_codeword == 3'b111);
+    $finish;
+  end
+
+endmodule
+}}}

crates/std/veryl/src/coding/test_linear_sec.veryl

@@ -0,0 +1,45 @@
+#[test(test_formal_sec)]
+embed (inline) sv{{{
+module test_linear_sec
+#(
+    parameter P = 9,
+    localparam N = (1 << P) - 1 - P,
+    localparam K = N + P
+)
+(
+    input i_clk,
+    input  logic [N-1:0] i_word,
+    input logic [K-1:0] i_err
+);
+
+`ifdef FORMAL
+default clocking @(posedge i_clk);
+endclocking
+
+default disable iff (1'b0);
+
+as_onehot0: assume property ($onehot0(i_err));
+
+logic [K-1:0] codeword;
+logic [K-1:0] perturbed_codeword;
+logic [N-1:0] word;
+logic corrected;
+
+std_linear_sec_encoder #(.P(P)) u_enc (.*, .o_codeword(codeword));
+assign perturbed_codeword = codeword ^ i_err;
+std_linear_sec_decoder #(.P(P)) u_dec (
+    .i_codeword(perturbed_codeword), .o_word(word), .o_corrected(corrected));
+
+ast_correct: assert property (word == i_word);
+ast_error: assert property (corrected == $onehot(i_err));
+`else
+  initial begin
+    $display("Skipping formal verification");
+    $finish;
+  end
+`endif
+
+
+
+endmodule
+}}}