luke
/
UberDDR3
mirror of https://github.com/AngeloJacobo/UberDDR3.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix error when bitflip is on MSB (sb_err dont need to assert here)

This commit is contained in:
AngeloJacobo 2024-07-28 17:31:46 +08:00
parent 9b99dbfe77
commit 4073e4f3fa
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
formal/ecc_formal.v
View File

@ -8,7 +8,7 @@ module ecc_formal;
integer m; integer m;
begin begin
m=1; m=1;
while (2**m < m+k+1) m++; while (2**m < m+k+1) m=m+1;
calculate_m = m; calculate_m = m;
end end
endfunction endfunction
@ -67,6 +67,7 @@ module ecc_formal;
q_o_enc_corrupted = q_o_enc; q_o_enc_corrupted = q_o_enc;
if(corrupted == 1) begin if(corrupted == 1) begin
q_o_enc_corrupted[corrupted_bit1] = !q_o_enc_corrupted[corrupted_bit1]; //corrupt 1 random bit q_o_enc_corrupted[corrupted_bit1] = !q_o_enc_corrupted[corrupted_bit1]; //corrupt 1 random bit
assume(corrupted_bit1 != (K+calculate_m(K))); //
end end
else if (corrupted == 2) begin // flip 2 bits 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_bit1] = !q_o_enc_corrupted[corrupted_bit1]; //corrupt 2 random bits
@ -80,7 +81,8 @@ module ecc_formal;
// main contract of this design // main contract of this design
always @* begin always @* begin
// if no corrupted bits, then decoded info must be equal to original info, and error flags should be low // 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 // OR there is 1 corrupted bit but its the MSB p0 that is corrupted
if( (corrupted == 0 || corrupted == 3) || ( (corrupted == 1) && (corrupted_bit1 == (K+calculate_m(K))) ) ) begin
assert(d_i == q_o_dec); assert(d_i == q_o_dec);
assert(!sb_err_o); assert(!sb_err_o);
assert(!db_err_o); assert(!db_err_o);