Add Formal Verification and Fix Bug

.gitignore

@@ -0,0 +1,2 @@
+**ecc_cover**
+**ecc_prf**

bench/verilog/testbench_top.sv

@@ -322,7 +322,7 @@ module testbench_top;
 
 
   //delay data; same delay as channel
-  always @(posedge clk) ch_enc_d <= enc_d;
+	always @(negedge clk) ch_enc_d <= enc_d;
 
 
   //instantiate decoder

formal/ecc.sby

@@ -0,0 +1,45 @@
+[tasks]
+prf_8 prf opt_K8
+prf_16 prf opt_K16
+prf_32 prf opt_K32
+prf_64 prf opt_K64
+cover cvr
+
+[options]
+prf: mode prove
+prf: depth 1
+cvr: mode cover
+cvr: depth 15
+multiclock on
+
+[engines]
+smtbmc
+
+[script]
+read -formal ecc_formal.v
+read -formal ecc_enc.sv
+read -formal ecc_dec.sv
+
+--pycode-begin--
+cmd = "hierarchy -top ecc_formal"
+
+# Choose value of K parameter
+if "opt_K8" in  tags:
+    cmd += " -chparam K 8"
+elif "opt_K16" in tags:
+    cmd += " -chparam K 16"
+elif "opt_K32" in tags:
+    cmd += " -chparam K 32"
+else:
+    cmd += " -chparam K 64"
+
+output(cmd)
+--pycode-end--
+
+
+prep -top ecc_formal
+
+[files]
+./ecc_formal.v
+../rtl/verilog/ecc_enc.sv
+../rtl/verilog/ecc_dec.sv

formal/ecc_formal.v

@@ -0,0 +1,123 @@
+module ecc_formal;
+    parameter K = 8,
+        P0_LSB = 0;
+
+    // function to find number of check bits
+     function integer calculate_m;
+        input integer k;
+        integer m;
+        begin
+            m=1;
+            while (2**m < m+k+1) m++;
+            calculate_m = m;
+        end
+    endfunction
+
+    // anyseq indicates nets that are controllable by engine
+    (*anyseq*)wire[K-1:0] d_i; // information input
+    (*anyseq*) wire[1:0] corrupted; // 0 or 3 = not corrupted bit, 1 = 1 corrupted bit, 2 = 2 corrupted bits
+    (*anyseq*) wire[$clog2(K+calculate_m(K))-1:0] corrupted_bit1, corrupted_bit2; // which bit will be corrupted
+
+    wire[K-1:0] q_o_dec;
+    wire[K+calculate_m(K):0] q_o_enc;
+    reg[K+calculate_m(K):0] q_o_enc_corrupted;
+    wire sb_err_o;
+    wire db_err_o;
+
+    ecc_enc #(
+        .K(K), //Information bit vector size
+        .P0_LSB(P0_LSB) //0: p0 is located at MSB
+                    //1: p0 is located at LSB
+    ) ecc_enc_inst (
+        .d_i(d_i),      //information bit vector input
+        .q_o(q_o_enc),  //encoded data word output
+        .p_o(),      //parity vector output
+        .p0_o()      //extended parity bit
+    );
+
+    ecc_dec #(
+        .K(K), //Information bit vector size
+        .LATENCY(0), //0: no latency (combinatorial design)
+                            //1: registered outputs
+                            //2: registered inputs+outputs
+        .P0_LSB(P0_LSB) //0: p0 is located at MSB
+                            //1: p0 is located at LSB
+    ) ecc_dec_inst (
+        //clock/reset ports (if LATENCY > 0)
+        .rst_ni(1'b1),     //asynchronous reset
+        .clk_i(1'b0),      //clock input
+        .clkena_i(1'b0),   //clock enable input
+        //data ports
+        .d_i(q_o_enc_corrupted),        //encoded code word input
+        .q_o(q_o_dec),        //information bit vector output
+        .syndrome_o(), //syndrome vector output
+        //flags
+        .sb_err_o(sb_err_o),   //single bit error detected
+        .db_err_o(db_err_o),   //double bit error detected
+        .sb_fix_o()    //repaired error in the information bits
+    );
+
+    `ifdef FORMAL
+        (*gclk*) reg f_clk = 0; // reference: https://symbiyosys.readthedocs.io/en/latest/verilog.html#global-clock
+        reg[9:0] f_counter = 0;
+
+        // corrupt the information based on the value of "corrupted" which is controllable by formal engine:
+        // 0 = no corrupted bits , 1 = 1 corrupted bit, 2 = 2 corrupted bits, 3 = no corrupted bits
+        always @* begin
+            q_o_enc_corrupted = q_o_enc;
+            if(corrupted == 1) begin 
+                q_o_enc_corrupted[corrupted_bit1] = !q_o_enc_corrupted[corrupted_bit1]; //corrupt 1 random bit
+            end
+            else if (corrupted == 2) begin // flip 2 bits
+                q_o_enc_corrupted[corrupted_bit1] = !q_o_enc_corrupted[corrupted_bit1]; //corrupt 2 random bits 
+                q_o_enc_corrupted[corrupted_bit2] = !q_o_enc_corrupted[corrupted_bit2];
+            end
+            assume(corrupted_bit1 != corrupted_bit2); // corrupted bit should be different (in case of 2 corrupted bits)
+            assume(corrupted_bit1 <= (K+calculate_m(K))); // corrupted bit should be within the index of q_o_enc_corrupted
+            assume(corrupted_bit2 <= (K+calculate_m(K))); // corrupted bit should be within the index of q_o_enc_corrupted
+        end
+
+        // main contract of this design
+        always @* begin
+            // if no corrupted bits, then decoded info must be equal to original info, and error flags should be low
+            if(corrupted == 0 || corrupted == 3) begin
+                assert(d_i == q_o_dec);
+                assert(!sb_err_o);
+                assert(!db_err_o);
+            end
+            // if 1 corrupted bit, then decoded info must still be equal to original info, single-bit error flag must be high, double-bit error flag must be low
+            else if(corrupted == 1) begin
+                assert(d_i == q_o_dec);
+                assert(sb_err_o);
+                assert(!db_err_o);
+            end
+            // if 2 corrupted bits, then single-bit error flag must be low, double-bit error flag must be high
+            else if(corrupted == 2) begin
+                assert(!sb_err_o);
+                assert(db_err_o);
+            end
+        end
+
+        // cover 10 cycles
+        always @(posedge f_clk) begin
+            f_counter <= f_counter + 1;
+            assume(corrupted == f_counter[1:0]); // number of corrupted bits change per clock cycle
+            cover((f_counter == 10));
+        end
+
+        // simulate random information
+        always @(posedge f_clk) begin
+            assume(d_i != $past(d_i,1)); 
+            assume(d_i != $past(d_i,2)); 
+            assume(d_i != $past(d_i,3)); 
+            assume(d_i != $past(d_i,4)); 
+            assume(d_i != $past(d_i,5)); 
+            assume(d_i != $past(d_i,6)); 
+            assume(d_i != $past(d_i,7)); 
+            assume(d_i != $past(d_i,8)); 
+            assume(d_i != $past(d_i,9)); 
+            assume(d_i != $past(d_i,10)); 
+        end
+
+    `endif
+endmodule

formal/run_formal.sh

@@ -0,0 +1,24 @@
+echo ""
+echo -e "\e[32mRun Symbiyosys Formal Verification: \e[0m"
+echo "---------------------------------------"
+sby -f ecc.sby
+
+# ANSI color codes
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+NC='\033[0m' # No Color
+
+echo ""
+echo ""
+echo "Summary:"
+# Iterate over folders starting with 'ecc_*'
+for folder in ecc_*/ ; do
+    # Check if the 'PASS' file exists in the folder
+    if [[ -e "${folder}PASS" ]]; then
+        # Print the folder name and 'PASS' in green
+        echo -e "${folder}: ${GREEN}PASS${NC}"
+    else
+        # Print the folder name and 'FAIL' in red
+        echo -e "${folder}: ${RED}FAIL${NC}"
+    fi
+done

rtl/verilog/altecc_enc.v

@@ -1,4 +1,4 @@
-i/////////////////////////////////////////////////////////////////////
+/////////////////////////////////////////////////////////////////////
 //   ,------.                    ,--.                ,--.          //
 //   |  .--. ' ,---.  ,--,--.    |  |    ,---. ,---. `--' ,---.    //
 //   |  '--'.'| .-. |' ,-.  |    |  |   | .-. | .-. |,--.| .--'    //

rtl/verilog/ecc_dec.sv

@@ -270,7 +270,7 @@ assign cw_fixed = correct_codeword(d_reg, syndrome_reg);
 assign q = extract_q(cw_fixed);
 
 //Step 7: Generate status flags
-assign sb_err =  parity_reg & |syndrome_reg;
+assign sb_err = (parity_reg & |syndrome_reg) || (parity_reg & syndrome_reg == 0); // include error when the overall parity bit itself is wrong
 assign db_err = ~parity_reg & |syndrome_reg;
 assign sb_fix =  parity_reg & |information_error(syndrome_reg);