Commit 7e6c0003 authored by Guillem Cabo's avatar Guillem Cabo
Browse files

Merge branch 'jk/FT-rebase' into 'develop'

add fault tolerance

See merge request !11
parents a383924a 9d9db298
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Single error corection, double error detection
// Description: This module takes 26 bits of incomming data and computes the checkbits
// for Hamming codes.
//
// Coder : G.Cabo
// References : Ben Eater "What is error correction? Hamming codes in hardware" YT
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module hamming32t26d_enc #
(
//Parameter that does nothing but prevents tcmalloc bug VIVADO
parameter VIVADO=0,
// Width of sampled signal
localparam integer IN_WIDTH = 26,
// Number of hamming bits
localparam integer N_CHECKB = $clog2(IN_WIDTH) //4
)
(
// Signal at register input
input wire [IN_WIDTH-1:0] data_i,
// Hamming vector
output wire [IN_WIDTH+N_CHECKB:0] hv_o
);
logic [N_CHECKB-1:0] hcheck_int; // hamming parity bits
logic ocheck_int; // Overall parity bit
//Rearrange ingputs
//Data
assign hv_o[3]=data_i[0];
assign hv_o[5]=data_i[1];
assign hv_o[6]=data_i[2];
assign hv_o[7]=data_i[3];
assign hv_o[9]=data_i[4];
assign hv_o[10]=data_i[5];
assign hv_o[11]=data_i[6];
assign hv_o[12]=data_i[7];
assign hv_o[13]=data_i[8];
assign hv_o[14]=data_i[9];
assign hv_o[15]=data_i[10];
assign hv_o[17]=data_i[11];
assign hv_o[18]=data_i[12];
assign hv_o[19]=data_i[13];
assign hv_o[20]=data_i[14];
assign hv_o[21]=data_i[15];
assign hv_o[22]=data_i[16];
assign hv_o[23]=data_i[17];
assign hv_o[24]=data_i[18];
assign hv_o[25]=data_i[19];
assign hv_o[26]=data_i[20];
assign hv_o[27]=data_i[21];
assign hv_o[28]=data_i[22];
assign hv_o[29]=data_i[23];
assign hv_o[30]=data_i[24];
assign hv_o[31]=data_i[25];
//Checkbits
assign hv_o[0]=ocheck_int;
assign hv_o[1]=hcheck_int[0];
assign hv_o[2]=hcheck_int[1];
assign hv_o[4]=hcheck_int[2];
assign hv_o[8]=hcheck_int[3];
assign hv_o[16]=hcheck_int[4];
//compute checkbits
assign hcheck_int[0] = ^{hv_o[3],hv_o[5],hv_o[7],
hv_o[9],hv_o[11],hv_o[13],hv_o[15],
hv_o[17],hv_o[19],hv_o[21],hv_o[23],
hv_o[25],hv_o[27],hv_o[29],hv_o[31]};
assign hcheck_int[1] = ^{hv_o[3],hv_o[6],hv_o[7],
hv_o[10],hv_o[11],hv_o[14],hv_o[15],
hv_o[18],hv_o[19], hv_o[22],hv_o[23],
hv_o[26],hv_o[27], hv_o[30],hv_o[31] };
assign hcheck_int[2] = ^{hv_o[5],hv_o[6],hv_o[7],
hv_o[12],hv_o[13],hv_o[14],hv_o[15],
hv_o[20],hv_o[21],hv_o[22],hv_o[23],
hv_o[28],hv_o[29],hv_o[30],hv_o[31]};
assign hcheck_int[3] = ^{hv_o[9],hv_o[10],hv_o[11],hv_o[12],hv_o[13],hv_o[14],hv_o[15],
hv_o[24],hv_o[25],hv_o[26],hv_o[27],hv_o[28],hv_o[29],hv_o[30],hv_o[31]};
assign hcheck_int[4] = ^{hv_o[17],hv_o[18],hv_o[19],hv_o[20],hv_o[21],hv_o[22],hv_o[23],
hv_o[24],hv_o[25],hv_o[26],hv_o[27],hv_o[28],hv_o[29],hv_o[30],hv_o[31]};
assign ocheck_int = ^hv_o[31:1];
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
// assert (IN_WIDTH==26);
// assert (N_CHECKB==5);
`endif
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip
IPs for Transient and permanent error detection and correction mechanisms
* com\_tr.sv: Single or multiple event transient error detector for
combinational logic. Registered output error signal. Non-intrusive changes.
* reg\_sbf.sv: Single bitflip error detection for registers. Registered output
signal. Non-intrusive changes.
* ecc\_reg\_sbf.sv: Single bitflip error correction for registers.
* hamming16t11d\_enc: SEC-DEC Hamming encoder. 11 data bits, 5 check bits.
* hamming16t11d\_dec: SEC-DEC Hamming decoder. 11 data bits, 5 check bits.
* way3\_voter: Tree way voter for replicated logic.
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Single bit-flip error detector circuit.
// Description: This module takes a signals coming from the input of a register,
// computes an even parity bit at the input and registers its value. The output
// of the monitored register is used afterwards to compute again the parity bit.
// If the parity bit at the output is different to the previous parity bit and
// error is signaled.
//
// Number of ones for data + parity bit shall be even.
//
// Error signal is only active while the bit-flip is present in the circuit aka
// the error signal is NOT holded until it is handled.
//
// Coder : G.Cabo
// References : Fault-Tolerance Techniques for SRAM-Based FPGAs - ISBN 978-0-387-31069-5
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module reg_sbf #
(
// Width of sampled signal
parameter integer IN_WIDTH = 32
)
(
// Global Clock Signal
input wire clk_i,
// Global Reset Signal. This Signal is Active LOW
input wire rstn_i,
// Signal at register input
input wire [IN_WIDTH-1:0] regi_i,
// Signal at register output
input wire [IN_WIDTH-1:0] rego_i,
// Enable for error detection
output reg error_o
);
logic parity1_int; //parity bit at input
logic parity2_int; //parity bit at output
logic reg_parity_int; // parity bit from input register
//Get parity from input of register and register value
assign parity1_int = ^regi_i;
always_ff @(posedge clk_i) begin
if(!rstn_i) begin
reg_parity_int <= 1'b0;
end else begin
reg_parity_int <= parity1_int;
end
end
//Get parity from output of register
assign parity2_int = ^rego_i;
//Compare parity bits and signal error if discrepancy
assign error_o = (parity2_int == reg_parity_int)? 1'b0:1'b1;
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
`endif
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Instance of register with parity bit detection
// Description:
//
// Coder : G.Cabo
// References :
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module sbf_reg #
(
// Width of sampled signal
parameter integer IN_WIDTH = 4
)
(
// Global Clock Signal
input wire clk_i,
// Global Reset Signal. This Signal is Active LOW
input wire rstn_i,
// data input
input wire [IN_WIDTH-1:0] din_i,
// error detected
output wire error_o
);
logic [IN_WIDTH-1:0] sbf_preg;
logic [IN_WIDTH-1:0] sbf_preg_d;
logic [IN_WIDTH-1:0] sbf_preg_q;
logic sbf_error;
assign sbf_preg_d = din_i;
always_ff @(posedge clk_i) begin
if(!rstn_i) begin
sbf_preg <= '{default:'0};
end else begin
sbf_preg <= sbf_preg_d;
end
end
assign sbf_preg_q = sbf_preg;
reg_sbf #(
.IN_WIDTH(IN_WIDTH)
)dut_reg_sbf (
.clk_i(clk_i),
.rstn_i(rstn_i),
.regi_i(sbf_preg_d),
.rego_i(sbf_preg_q),
.error_o(error_o)
);
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
`endif
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Instance of register with triplication and voting SECDEC
// Description:
//
// Coder : G.Cabo
// References :
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module triple_reg #
(
// Width of sampled signal
parameter integer IN_WIDTH = 4
)
(
// Global Clock Signal
input wire clk_i,
// Global Reset Signal. This Signal is Active LOW
input wire rstn_i,
// data input
input wire [IN_WIDTH-1:0] din_i,
// data output
output wire [IN_WIDTH-1:0] dout_o,
// Single error detected and corrected
output wire error1_o,
// Two errors detected NON corrected
output wire error2_o
);
logic [IN_WIDTH-1:0] trip0_preg;
logic [IN_WIDTH-1:0] trip1_preg;
logic [IN_WIDTH-1:0] trip2_preg;
logic [IN_WIDTH-1:0] trip_preg_d;
logic [IN_WIDTH-1:0] trip0_preg_q;
logic [IN_WIDTH-1:0] trip1_preg_q;
logic [IN_WIDTH-1:0] trip2_preg_q;
logic trip_error1;
logic trip_error2;
logic [IN_WIDTH-1:0] trip_dout;
assign trip_preg_d = din_i;
assign trip0_preg_q = trip0_preg;
assign trip1_preg_q = trip1_preg;
assign trip2_preg_q = trip2_preg;
always_ff @(posedge clk_i) begin
if(!rstn_i) begin
trip0_preg <= '{default:'0};
trip1_preg <= '{default:'0};
trip2_preg <= '{default:'0};
end else begin
trip0_preg <= trip_preg_d;
trip1_preg <= trip_preg_d;
trip2_preg <= trip_preg_d;
end
end
way3_voter #(
.IN_WIDTH(IN_WIDTH)
)dut_way3(
.in0(trip0_preg_q),
.in1(trip1_preg_q),
.in2(trip2_preg_q),
.out(trip_dout),
.error1_o(trip_error1),
.error2_o(trip_error2)
);
assign dout_o = trip_dout;
assign error1_o = trip_error1;
assign error2_o = trip_error2;
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
`endif
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Three way voter for reduncancy mechanisms
// Description: This module compares tree signals and outputs the most common value.
// If one signal is different rises error1_o.
// If Non of the signals is the same it rises error2_o
//
// Error signal is only active while the condition it describes is active.
//
// The circuit is combinational, is up to the designer to add input or
// output registers.
//
// Coder : G.Cabo
// References :
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module way3_voter #
(
// Width of sampled signal
parameter integer IN_WIDTH = 32
)
(
// Input 0
input wire logic [IN_WIDTH-1:0] in0,
// Input 1
input wire logic [IN_WIDTH-1:0] in1,
// Input 2
input wire logic [IN_WIDTH-1:0] in2,
// Voted output
output logic [IN_WIDTH-1:0] out,
// One discrepance - recovered
output logic error1_o,
// Two discrepancies - unrecoverable
output logic error2_o
);
always_comb begin
if (in0==in1) begin
out = in0;
if (in0!=in2) begin
error1_o = 1'b1;
error2_o = 1'b0;
end else begin
error1_o = 1'b0;
error2_o = 1'b0;
end
end else begin
error1_o = 1'b1;//Reach else implies in0!=in1
if (in0==in2) begin
out = in0;
error2_o = 1'b0;
end else begin
if (in1==in2) begin
out = in1;
error2_o = 1'b0;
end else begin
// Non of the signals match
// Select one input, but it may be incorrect
out = in0;
error2_o = 1'b1;
end
end
end
end
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
`endif
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Three way voter for reduncancy mechanisms
// Description: This module compares tree signals and outputs the most common value.
// Way3u2a_voter stands for 3 inputs voter for 2D unpacked arrays
// Takes as input an unpacked array of depth U and width W.
// If one signal is different rises error1_o.
// If Non of the signals is the same it rises error2_o
//
// Error signal is only active while the condition it describes is active.
//
// The circuit is combinational, is up to the designer to add input or
// output registers.
//
// Coder : G.Cabo
// References :
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module way3u2a_voter #
(
// Width of sampled signal
parameter integer W = 32,
// Depth of unpacked entries
parameter integer D = 32,
// Number of unpacked entries
parameter integer U = 4
)
(
// Input 0
input wire logic [W-1:0] in0 [0:U-1][0:D-1],
// Input 1
input wire logic [W-1:0] in1 [0:U-1][0:D-1],
// Input 2
input wire logic [W-1:0] in2 [0:U-1][0:D-1],
// Voted output
output logic [W-1:0] out [0:U-1][0:D-1],
// One discrepance - recovered
output logic error1_o,
// Two discrepancies - unrecoverable
output logic error2_o
);
always_comb begin
if (in0==in1) begin
out = in0;
if (in0!=in2) begin
error1_o = 1'b1;
error2_o = 1'b0;
end else begin
error1_o = 1'b0;
error2_o = 1'b0;
end
end else begin
error1_o = 1'b1;//Reach else implies in0!=in1
if (in0==in2) begin
out = in0;
error2_o = 1'b0;
end else begin
if (in1==in2) begin
out = in1;
error2_o = 1'b0;
end else begin
// Non of the signals match
// Select one input, but it may be incorrect
out = in0;
error2_o = 1'b1;
end
end
end
end
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
`endif
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip
//-----------------------------------------------------
// ProjectName: De-RISC/SELENE
// Function : Three way voter for reduncancy mechanisms
// Description: This module compares tree signals and outputs the most common value.
// Way3ua_voter stands for 3 inputs voter for unpacked arrays
// Takes as input an unpacked array of depth U and width W.
// If one signal is different rises error1_o.
// If Non of the signals is the same it rises error2_o
//
// Error signal is only active while the condition it describes is active.
//
// The circuit is combinational, is up to the designer to add input or
// output registers.
//
// Coder : G.Cabo
// References :
`default_nettype none
`timescale 1 ns / 1 ps
`ifndef SYNT
`ifdef FORMAL
`define ASSERTIONS
`endif
`endif
module way3ua_voter #
(
// Width of sampled signal
parameter integer W = 32,
// Number of unpacked entries
parameter integer U = 4
)
(
// Input 0
input wire logic [W-1:0] in0 [0:U-1],
// Input 1
input wire logic [W-1:0] in1 [0:U-1],
// Input 2
input wire logic [W-1:0] in2 [0:U-1],
// Voted output
output logic [W-1:0] out [0:U-1],
// One discrepance - recovered
output logic error1_o,
// Two discrepancies - unrecoverable
output logic error2_o
);
always_comb begin
if (in0==in1) begin
out = in0;
if (in0!=in2) begin
error1_o = 1'b1;
error2_o = 1'b0;
end else begin
error1_o = 1'b0;
error2_o = 1'b0;
end
end else begin
error1_o = 1'b1;//Reach else implies in0!=in1
if (in0==in2) begin
out = in0;
error2_o = 1'b0;
end else begin
if (in1==in2) begin
out = in1;
error2_o = 1'b0;
end else begin
// Non of the signals match
// Select one input, but it may be incorrect
out = in0;
error2_o = 1'b1;
end
end
end
end
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL