Commit 36a3f993 authored by GuillemCabo's avatar GuillemCabo Committed by Guillem
Browse files

BMC and Cover FV passes

bugfix

add FT ahb_pmu and doc

add spreadsheet with FT actions; completed fix high priority items pmu_ahb; add FT reg modules to seu_ip folder; Updated FV, synth and Questa scripts;

number faults tex, update status fixes ods

fix FV and sim scripts
parent 6a1ad51b
This diff is collapsed.
......@@ -50,8 +50,9 @@
\numberwithin{table}{section} % Number tables within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4)
%\setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text
\usepackage{enumitem}
\setenumerate[1]{label=\thesubsection.\arabic*.}
\setenumerate[2]{label*=\arabic*.}
\setlength\parskip{4pt}
%----------------------------------------------------------------------------------------
......@@ -61,7 +62,7 @@
\newcommand{\horrule}[1]{\rule{\linewidth}{#1}} % Create horizontal rule command with 1 argument of height
\title{
\normalfont \normalsize
\normalfont \normalsize º
\horrule{0.5pt} \\[0.4cm] % Thin top horizontal rule
\huge SafePMU Fault Tolerance Measures\\ % The assignment title
\horrule{2pt} \\[0.5cm] % Thick bottom horizontal rule
......
......@@ -36,6 +36,8 @@
parameter integer N_SOC_EV = 32,
// Configuration registers
parameter integer N_CONF_REGS = 1,
// Fault tolerance mechanisms (FT==0 -> FT disabled)
parameter integer FT = 1,
//------------- Internal Parameters
......@@ -619,7 +621,12 @@ end
end
end
if (FT==0) begin
//register enable to solve Hazards
// Does not nid replication since regs_i is already protected
// RDC_enable_int may be disabled for a single cycle but
// it will not be a permanent fault
reg RDC_enable_int;
always @(posedge clk_i) begin: RDC_glitchless_enable
if (!rstn_i) begin
......@@ -629,7 +636,6 @@ end
RDC_enable_int <= regs_i[BASE_MCCU_CFG][MCCU_N_CORES+2+1];
end
end
RDC #(
// Width of data registers
.DATA_WIDTH (REG_WIDTH),
......@@ -652,6 +658,137 @@ end
//maximum pulse length of a given core event
.watermark_o(MCCU_watermark_int)
);
end else begin : Rdctrip
//register enable to solve Hazards
// Does not nid replication since regs_i is already protected
// RDC_enable_int may be disabled for a single cycle but
// it will not be a permanent fault
logic RDC_enable_int_D, RDC_enable_int_Q;
logic RDC_enable_fte1, RDC_enable_fte2;
triple_reg#(.IN_WIDTH(1)
)RDC_enable_trip(
.clk_i(clk_i),
.rstn_i(rstn_i),
.din_i(RDC_enable_int_D),
.dout_o(RDC_enable_int_Q),
.error1_o(RDC_enable_fte1), // ignore corrected errors
.error2_o(RDC_enable_fte2)
);
always @(posedge clk_i) begin: RDC_glitchless_enable
if (!rstn_i) begin
RDC_enable_int_D <= 0;
end else begin
RDC_enable_int_D <= regs_i[BASE_MCCU_CFG][6];
end
end
//Signals from instances to way3 voter
//inst
logic intr_RDC_ft0 ;
logic [MCCU_N_EVENTS-1:0] interruption_rdc_ft0 [0:MCCU_N_CORES-1];
logic [MCCU_WEIGHTS_WIDTH-1:0] MCCU_watermark_ft0 [0:MCCU_N_CORES-1]
[0:MCCU_N_EVENTS-1];
//inst1
logic intr_RDC_ft1 ;
logic [MCCU_N_EVENTS-1:0] interruption_rdc_ft1 [0:MCCU_N_CORES-1];
logic [MCCU_WEIGHTS_WIDTH-1:0] MCCU_watermark_ft1 [0:MCCU_N_CORES-1]
[0:MCCU_N_EVENTS-1];
//inst2
logic intr_RDC_ft2 ;
logic [MCCU_N_EVENTS-1:0] interruption_rdc_ft2 [0:MCCU_N_CORES-1];
logic [MCCU_WEIGHTS_WIDTH-1:0] MCCU_watermark_ft2 [0:MCCU_N_CORES-1]
[0:MCCU_N_EVENTS-1];
//FT error detected signals
//Even when the error is corrected latent faults may be present on this signals
// and software shall clear them
logic intr_RDC_fte1, interruption_rdc_fte1, MCCU_watermark_fte1;
logic intr_RDC_fte2, interruption_rdc_fte2, MCCU_watermark_fte2;
RDC #(
.DATA_WIDTH (REG_WIDTH),
.WEIGHTS_WIDTH (RDC_WEIGHTS_WIDTH),
.N_CORES (RDC_N_CORES),
.CORE_EVENTS (RDC_N_EVENTS)
) inst_RDC(
.clk_i (clk_i),
.rstn_i (RDC_rstn), //active low
.enable_i (RDC_enable_int_Q),// Software map
.events_i (MCCU_events_int),
.events_weights_i (MCCU_events_weights_int),
.interruption_rdc_o(intr_RDC_ft0),
.interruption_vector_rdc_o(interruption_rdc_ft0),
.watermark_o(MCCU_watermark_ft0)
);
RDC #(
.DATA_WIDTH (REG_WIDTH),
.WEIGHTS_WIDTH (RDC_WEIGHTS_WIDTH),
.N_CORES (RDC_N_CORES),
.CORE_EVENTS (RDC_N_EVENTS)
) inst1_RDC(
.clk_i (clk_i),
.rstn_i (RDC_rstn), //active low
.enable_i (RDC_enable_int_Q),// Software map
.events_i (MCCU_events_int),
.events_weights_i (MCCU_events_weights_int),
.interruption_rdc_o(intr_RDC_ft1),
.interruption_vector_rdc_o(interruption_rdc_ft1),
.watermark_o(MCCU_watermark_ft1)
);
RDC #(
.DATA_WIDTH (REG_WIDTH),
.WEIGHTS_WIDTH (RDC_WEIGHTS_WIDTH),
.N_CORES (RDC_N_CORES),
.CORE_EVENTS (RDC_N_EVENTS)
) inst2_RDC(
.clk_i (clk_i),
.rstn_i (RDC_rstn), //active low
.enable_i (RDC_enable_int_Q),// Software map
.events_i (MCCU_events_int),
.events_weights_i (MCCU_events_weights_int),
.interruption_rdc_o(intr_RDC_ft2),
.interruption_vector_rdc_o(interruption_rdc_ft2),
.watermark_o(MCCU_watermark_ft2)
);
// intr_RDC_ft
way3_voter #(
.IN_WIDTH(1)
)intr_RDC_way3(
.in0(intr_RDC_ft0),
.in1(intr_RDC_ft1),
.in2(intr_RDC_ft2),
.out(intr_RDC_o),
.error1_o(intr_RDC_fte1),
.error2_o(intr_RDC_fte2)
);
// interruption_rdc_ft
way3ua_voter #(
.W(MCCU_N_EVENTS),
.U(MCCU_N_CORES)
)interruption_rdc_way3(
.in0(interruption_rdc_ft0),
.in1(interruption_rdc_ft1),
.in2(interruption_rdc_ft2),
.out(interruption_rdc_o),
.error1_o(interruption_rdc_fte1),
.error2_o(interruption_rdc_fte2)
);
// MCCU_watermark_ft
way3u2a_voter #(
.W(MCCU_WEIGHTS_WIDTH),
.U(MCCU_N_CORES),
.D(MCCU_N_EVENTS)
)watermark_way3(
.in0(MCCU_watermark_ft0),
.in1(MCCU_watermark_ft1),
.in2(MCCU_watermark_ft2),
.out(MCCU_watermark_int),
.error1_o(MCCU_watermark_fte1),
.error2_o(MCCU_watermark_fte2)
);
end
/////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
......
......@@ -179,11 +179,66 @@ localparam TRANSFER_ERROR_RESP_2CYCLE = 2'b11;
//------------- Data structures
//----------------------------------------------
var struct packed{
logic select;
logic write;
logic select_D, select_Q;
logic write_D, write_Q;
// logic master_ready;
logic [HADDR_WIDTH-1:0] master_addr;
logic [HADDR_WIDTH-1:0] master_addr_D, master_addr_Q;
} address_phase;
if (FT==0) begin
logic select, write;
logic [HADDR_WIDTH-1:0] master_addr;
always_ff @(posedge clk_i) begin
if (rstn_i==0) begin
select <= 1'b0;
write <= 1'b0;
master_addr <= '{default:0};
end else begin
select <= address_phase.select_D;
write <= address_phase. write_D;
master_addr <= address_phase.master_addr_D;
end
end
always_comb begin
address_phase.select_Q = select;
address_phase.write_Q = write;
address_phase.master_addr_Q = master_addr;
end
end else begin : Apft //Address phase FT
logic write_fte, select_fte, master_addr_fte;
triple_reg#(.IN_WIDTH(1)
)write_trip(
.clk_i(clk_i),
.rstn_i(rstn_i),
.din_i(address_phase.write_D),
.dout_o(address_phase.write_Q),
.error1_o(), // ignore corrected errors
.error2_o(write_fte)
);
triple_reg#(.IN_WIDTH(1)
)select_trip(
.clk_i(clk_i),
.rstn_i(rstn_i),
.din_i(address_phase.select_D),
.dout_o(address_phase.select_Q),
.error1_o(), // ignore corrected errors
.error2_o(select_fte)
);
triple_reg#(.IN_WIDTH(HADDR_WIDTH)
)master_addr_trip(
.clk_i(clk_i),
.rstn_i(rstn_i),
.din_i(address_phase.master_addr_D),
.dout_o(address_phase.master_addr_Q),
.error1_o(), // ignore corrected errors
.error2_o(master_addr_fte)
);
end
//----------------------------------------------
//------------- AHB registers
......@@ -220,7 +275,7 @@ var struct packed{
//AHB write
//Write to slv registers if slave was selected & was a write. Else
//register the values given by pmu_raw
if(address_phase.write && address_phase.select) begin
if(address_phase.write_Q && address_phase.select_Q) begin
// get the values from the pmu_raw instance
slv_reg_Q = slv_reg;
slv_reg_Q [slv_index] = dwrite_slave;
......@@ -231,8 +286,7 @@ var struct packed{
slv_reg_Q = slv_reg;
end
end
assign intr_FT_o = 1'b0;
end else begin
end else begin : Slvft
//FT version of the registers
// Hamming bits, 6 for each 26 bits of data
localparam HAM_P=6;//protection bits
......@@ -242,7 +296,7 @@ var struct packed{
//interrupt FT error
wire [N_HAM32_SLV-1:0] ift_slv; //interrupt fault tolerance mechanism
//"Flat" slv_reg Q and D signals
wire [N_HAM32_SLV*HAM_D-1:0] slv_reg_fti;//fault tolerance in
wire [N_HAM32_SLV*HAM_D-1:0] slv_reg_fte;//fault tolerance in
wire [N_HAM32_SLV*HAM_D-1:0] slv_reg_fto;//fault tolerance out
wire [REG_WIDTH-1:0] slv_reg_ufto [0:N_REGS-1];//unpacked fault tolerance out
wire [N_HAM32_SLV*HAM_D-1:0] slv_reg_pQ ;//protected output
......@@ -254,15 +308,15 @@ var struct packed{
//Feed and send flat assigment in to original format
for (genvar i =0; i<N_REGS; i++) begin
//assign slv_register inputs to a flat hamming input
assign slv_reg_fti[(i+1)*REG_WIDTH-1:i*REG_WIDTH]=slv_reg_D[i][REG_WIDTH-1:0];
assign slv_reg_fte[(i+1)*REG_WIDTH-1:i*REG_WIDTH]=slv_reg_D[i][REG_WIDTH-1:0];
end
// SEC-DEC hamming on 26 bit data chunks
for (genvar i =0; i<(N_HAM32_SLV); i++) begin : slv_ham_enc
//encoder
//hv_o needs to inteleave protection and data bits
hamming32t26d_enc#(
)dut_hamming32t26d_enc (
.data_i(slv_reg_fti[(i+1)*HAM_D-1:i*HAM_D]),
)slv_hamming32t26d_enc (
.data_i(slv_reg_fte[(i+1)*HAM_D-1:i*HAM_D]),
.hv_o(ham_mbits_D[(i+1)*(HAM_M)-1:i*(HAM_M)])
);
end
......@@ -274,7 +328,7 @@ var struct packed{
end else begin
//You could be using ham_mbits_D but code is longer
//Some of the ham_mbits_D aren't needed
slv_reg[i] <= slv_reg_fti[(i+1)*REG_WIDTH-1:REG_WIDTH*i];
slv_reg[i] <= slv_reg_fte[(i+1)*REG_WIDTH-1:REG_WIDTH*i];
end
end
assign slv_reg_pQ[(i+1)*REG_WIDTH-1:i*REG_WIDTH] = slv_reg[i];
......@@ -282,7 +336,7 @@ var struct packed{
// pad signals to fill an integer number of 26 bit chunks
for (genvar i =(N_REGS)*REG_WIDTH; i<N_HAM32_SLV*HAM_D; i++) begin
assign slv_reg_pQ[i] = 1'b0;
assign slv_reg_fti[i] = 1'b0;
assign slv_reg_fte[i] = 1'b0;
end
//Feed encoded parity bits into extra registers
......@@ -318,7 +372,7 @@ var struct packed{
for (genvar i =0; i<N_HAM32_SLV; i++) begin : slv_ham_dec
//decoder
hamming32t26d_dec#(
)dut_hamming32t26d_dec (
)slv_hamming32t26d_dec (
.data_o(slv_reg_fto[(i+1)*HAM_D-1:i*HAM_D]),
.hv_i(ham_mbits_Q[(i+1)*HAM_M-1:i*HAM_M]),
.ded_error_o(ift_slv[i])
......@@ -342,7 +396,7 @@ var struct packed{
//AHB write
//Write to slv registers if slave was selected & was a write. Else
//register the values given by pmu_raw
if(address_phase.write && address_phase.select) begin
if(address_phase.write_Q && address_phase.select_Q) begin
//Feed and send flat assigment in to original format
//assign flat hamming outputs to slv_reg_Q
slv_reg_Q=slv_reg_ufto;
......@@ -356,16 +410,121 @@ var struct packed{
slv_reg_Q=slv_reg_ufto;
end
end
//reduce all DED errors from hamming blocks to single interrupt
assign intr_FT_o = |ift_slv;
end
endgenerate
//----------------------------------------------
//------------- AHB control logic
//----------------------------------------------
logic [1:0] state, next;
logic [1:0] next;
if (FT==0) begin
logic [1:0] state;
//data phase - state update
always_ff @(posedge clk_i) begin
if(rstn_i == 1'b0 ) begin
state <= TRANS_IDLE;
end else begin
state <= next;
end
end
always_comb begin
//NOTE: I don't expect any of the cafe beaf values in the registers if they do
//there is a bug
case (state)
TRANS_IDLE: begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = 32'hbeaf1d1e;
dread_slave = 32'hcafe1d1e;
end
TRANS_BUSY:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = 32'hbeafb551;
dread_slave = 32'hcafeb551;
end
TRANS_NONSEQUENTIAL:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = hwdata_i;
if (!address_phase.write_Q) begin
dread_slave = slv_reg_Q[slv_index];
end else begin
dread_slave = 32'hcafe01a1;
end
end
TRANS_SEQUENTIAL:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = hwdata_i;
if (!address_phase.write_Q) begin
dread_slave = slv_reg_Q[slv_index];
end else begin
dread_slave = 32'hcafee1a1;
end
end
endcase
end
end else begin : Stateft
//Fault tolerant implementation
//Triplication of next and state registers
logic [1:0] state_D, state_Q;
logic state_fte; //fault tolerance errors
//error1 signals a corrected error, safe to ignore
triple_reg#(.IN_WIDTH(2)
)state_trip(
.clk_i(clk_i),
.rstn_i(rstn_i),
.din_i(state_D),
.dout_o(state_Q),
.error1_o(),
.error2_o(state_fte)
);
//data phase - state update
always_comb begin
if(rstn_i == 1'b0 ) begin
state_D = TRANS_IDLE;
end else begin
state_D = next;
end
end
always_comb begin
//NOTE: I don't expect any of the cafe beaf values in the registers if they do
//there is a bug
case (state_Q)
TRANS_IDLE: begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = 32'hbeaf1d1e;
dread_slave = 32'hcafe1d1e;
end
TRANS_BUSY:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = 32'hbeafb551;
dread_slave = 32'hcafeb551;
end
TRANS_NONSEQUENTIAL:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = hwdata_i;
if (!address_phase.write_Q) begin
dread_slave = slv_reg_Q[slv_index];
end else begin
dread_slave = 32'hcafe01a1;
end
end
TRANS_SEQUENTIAL:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = hwdata_i;
if (!address_phase.write_Q) begin
dread_slave = slv_reg_Q[slv_index];
end else begin
dread_slave = 32'hcafee1a1;
end
end
endcase
end
end
// address phase - state update
always_comb begin
case (htrans_i)
......@@ -395,98 +554,54 @@ always_comb begin
end
endcase
end
// address phase - register required inputs
always_ff @(posedge clk_i) begin
if(rstn_i == 1'b0 ) begin
//initialize all the structure to 0 at reset
address_phase <= '{default:0};
end else begin
case (next)
TRANS_IDLE:begin
address_phase.select <= hsel_i;
address_phase.write <= 0;
end
TRANS_BUSY:begin
address_phase.select <= hsel_i;
address_phase.write <= 0;
end
TRANS_NONSEQUENTIAL:begin
address_phase.select <= hsel_i;
address_phase.write <= hwrite_i;
address_phase.master_addr <= haddr_i;
end
TRANS_SEQUENTIAL:begin
address_phase.select <= hsel_i;
address_phase.write <= hwrite_i;
address_phase.master_addr <= haddr_i;
end
endcase
end
end
//data phase - state update
always_ff @(posedge clk_i) begin
if(rstn_i == 1'b0 ) begin
state <= TRANS_IDLE;
end else begin
state <= next;
end
end
//data phase - slave response
assign slv_index = address_phase.master_addr[$clog2(N_REGS)+1:2];
assign hrdata_o = dread_slave;
assign hreadyo_o = complete_transfer_status [0];
//TODO: review the amount of bits for hresp_o
assign hresp_o = {{complete_transfer_status[1]},{complete_transfer_status[1]}};
// address phase - register required inputs
always_comb begin
//NOTE: I don't expect any of the cafe beaf values in the registers if they do
//there is a bug
case (state)
TRANS_IDLE: begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = 32'hbeaf1d1e;
dread_slave = 32'hcafe1d1e;
case (next)
TRANS_IDLE:begin
address_phase.select_D = hsel_i;
address_phase.write_D = 0;
address_phase.master_addr_D = address_phase.master_addr_Q;
end
TRANS_BUSY:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = 32'hbeafb551;
dread_slave = 32'hcafeb551;
address_phase.select_D = hsel_i;
address_phase.write_D = 0;
address_phase.master_addr_D = address_phase.master_addr_Q;
end
TRANS_NONSEQUENTIAL:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = hwdata_i;
if (!address_phase.write) begin
dread_slave = slv_reg_Q[slv_index];
end else begin
dread_slave = 32'hcafe01a1;
end
address_phase.select_D = hsel_i;
address_phase.write_D = hwrite_i;
address_phase.master_addr_D = haddr_i;
end
TRANS_SEQUENTIAL:begin
complete_transfer_status = TRANSFER_SUCCESS_COMPLETE;
dwrite_slave = hwdata_i;
if (!address_phase.write) begin
dread_slave = slv_reg_Q[slv_index];
end else begin
dread_slave = 32'hcafee1a1;
end
address_phase.select_D = hsel_i;
address_phase.write_D = hwrite_i;
address_phase.master_addr_D = haddr_i;
end
endcase
end
//data phase - slave response
assign slv_index = address_phase.master_addr_Q[$clog2(N_REGS)+1:2];
assign hrdata_o = dread_slave;
assign hreadyo_o = complete_transfer_status [0];
//TODO: review the amount of bits for hresp_o
assign hresp_o = {{complete_transfer_status[1]},{complete_transfer_status[1]}};
//----------------------------------------------
//------------- PMU_raw instance
//----------------------------------------------
wire ahb_write_req;
assign ahb_write_req = address_phase.write && address_phase.select;
assign ahb_write_req = address_phase.write_Q && address_phase.select_Q;
PMU_raw #(
.REG_WIDTH(REG_WIDTH),
.MCCU_N_CORES(MCCU_N_CORES),
.N_COUNTERS(PMU_COUNTERS),
.N_SOC_EV(N_SOC_EV),
.FT(FT),
.N_CONF_REGS(PMU_CFG)
)inst_pmu_raw (
.clk_i(clk_i),
......@@ -502,6 +617,19 @@ end
.intr_RDC_o
);
//----------------------------------------------
//------------- Generate intr_FT_o
//----------------------------------------------
if (FT == 0 ) begin
assign intr_FT_o = 1'b0;
end else begin
//Gather all the signals of uncorrected errors from FT scopes
// Codestyle. All scopes start with a capital letter
assign intr_FT_o = |{Slvft.ift_slv,
Apft.write_fte,Apft.select_fte, Apft.master_addr_fte,
Stateft.state_fte
};
end
/////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
......@@ -550,7 +678,7 @@ end
//There is no pending write or it is not valid
sequence no_ahb_write;
//since ahb is pipelined i check for the last addres phase
f_past_valid && ($past(ahb_write_req==1'b0));
f_past_valid && (ahb_write_req==1'b0);
endsequence
//Register 1, assigned to counter 0 can't decrease
sequence no_decrease_counter(n);
......@@ -566,8 +694,8 @@ end
genvar i;
for (i=0;i<PMU_COUNTERS;i++) begin
assert property (
no_ahb_write and no_counter_reset
|=> no_decrease_counter(i) or counter_reset or overflow_counter(i)
no_ahb_write and (rstn_i==1) and