Commit e7e1c09f authored by Guillem's avatar Guillem
Browse files

Watermark for RDC, formal properities

parametrize counters

Docs and signal remap
parent 3a7580aa
No preview for this file type
......@@ -136,8 +136,13 @@
// (((....)-1)/(...)+1) is equivalent to ceil
localparam N_RDC_WEIGHTS = 0,
localparam END_RDC_WEIGHTS = END_MCCU_WEIGHTS,
// Watermark for each one of the available events
localparam BASE_RDC_WATERMARK = END_RDC_VECT + 1,
// (((....)-1)/(...)+1) is equivalent to ceil
localparam N_RDC_WATERMARK = (((MCCU_N_CORES*MCCU_N_EVENTS*MCCU_WEIGHTS_WIDTH)-1)/REG_WIDTH+1),
localparam END_RDC_WATERMARK = BASE_RDC_WATERMARK + N_RDC_WATERMARK -1,
// General parameters feature
localparam N_RDC_REGS = (N_RDC_WEIGHTS + N_RDC_VECT_REGS) * RDC,
localparam N_RDC_REGS = (N_RDC_WEIGHTS + N_RDC_VECT_REGS+N_RDC_WATERMARK) * RDC,
//---- Total of registers used
localparam integer TOTAL_NREGS =
......@@ -170,7 +175,6 @@
//----------------------------------------------
// VIVADO: list of debug signals for ILA
//----------------------------------------------
//`define ILA_DEBUG_PMU_RAW
`ifdef ILA_DEBUG_PMU_RAW
(* MARK_DEBUG = "TRUE" *) logic [REG_WIDTH-1:0] debug_regs_i [0:TOTAL_NREGS-1];
(* MARK_DEBUG = "TRUE" *) logic [REG_WIDTH-1:0] debug_regs_o [0:TOTAL_NREGS-1];
......@@ -189,7 +193,6 @@
assign debug_intr_quota_o = intr_quota_o;
assign debug_intr_MCCU_o = intr_MCCU_o;
assign debug_intr_RDC_o = intr_RDC_o;
`endif
//----------------------------------------------
......@@ -209,7 +212,9 @@
//---- Overflow interruption signals
wire [N_COUNTERS-1:0] overflow_intr_mask_i [0 : N_OVERFLOW_MASK_REGS-1];
wire [N_COUNTERS-1:0] overflow_intr_vect_o [0 : N_OVERFLOW_VECT_REGS-1];
//---- RDC watermark signals
wire [MCCU_WEIGHTS_WIDTH-1:0] MCCU_watermark_int [0:MCCU_N_CORES-1]
[0:MCCU_N_EVENTS-1];
//----------------------------------------------
//------------- Map registers from wrapper to slave functions
//----------------------------------------------
......@@ -261,6 +266,18 @@
assign regs_o[BASE_MCCU_LIMITS:END_MCCU_LIMITS] = regs_i[BASE_MCCU_LIMITS:END_MCCU_LIMITS];
assign regs_o[BASE_MCCU_WEIGHTS:END_MCCU_WEIGHTS] = regs_i[BASE_MCCU_WEIGHTS:END_MCCU_WEIGHTS];
//---- Request Duration Counter (RDC) registers
//core_0
assign regs_o[BASE_RDC_WATERMARK][MCCU_WEIGHTS_WIDTH-1:0] = MCCU_watermark_int [0][0] ;
assign regs_o[BASE_RDC_WATERMARK][2*MCCU_WEIGHTS_WIDTH-1:MCCU_WEIGHTS_WIDTH] = MCCU_watermark_int [0][1];
//core_1
assign regs_o[BASE_RDC_WATERMARK][3*MCCU_WEIGHTS_WIDTH-1:2*MCCU_WEIGHTS_WIDTH] = MCCU_watermark_int [1][0];
assign regs_o[BASE_RDC_WATERMARK][4*MCCU_WEIGHTS_WIDTH-1:3*MCCU_WEIGHTS_WIDTH] = MCCU_watermark_int [1][1] ;
//core_2
assign regs_o[BASE_RDC_WATERMARK+1][MCCU_WEIGHTS_WIDTH-1:0] = MCCU_watermark_int [2][0] ;
assign regs_o[BASE_RDC_WATERMARK+1][2*MCCU_WEIGHTS_WIDTH-1:MCCU_WEIGHTS_WIDTH] = MCCU_watermark_int [2][1] ;
//core_3
assign regs_o[BASE_RDC_WATERMARK+1][3*MCCU_WEIGHTS_WIDTH-1:2*MCCU_WEIGHTS_WIDTH] = MCCU_watermark_int [3][0] ;
assign regs_o[BASE_RDC_WATERMARK+1][4*MCCU_WEIGHTS_WIDTH-1:3*MCCU_WEIGHTS_WIDTH] = MCCU_watermark_int [3][1] ;
//----------------------------------------------
//------------- Selftest configuration
......@@ -372,13 +389,13 @@ end
//be hardcoded to specific corssbars outputs
wire [MCCU_N_EVENTS-1:0] MCCU_events_int[0:MCCU_N_CORES-1];
//core_0
assign MCCU_events_int [0] = {{events_int[0]},{events_int[1]}};
assign MCCU_events_int [0] = {{events_int[1]},{events_int[0]}};
//core_1
assign MCCU_events_int [1] = {{events_int[2]},{events_int[3]}};
assign MCCU_events_int [1] = {{events_int[3]},{events_int[2]}};
//core_2
assign MCCU_events_int [2] = {{events_int[4]},{events_int[5]}};
assign MCCU_events_int [2] = {{events_int[5]},{events_int[4]}};
//core_3
assign MCCU_events_int [3] = {{events_int[6]},{events_int[7]}};
assign MCCU_events_int [3] = {{events_int[7]},{events_int[6]}};
//NON-PARAMETRIC This can be autogenenerated TODO
wire [MCCU_WEIGHTS_WIDTH-1:0] MCCU_events_weights_int [0:MCCU_N_CORES-1]
......@@ -450,6 +467,7 @@ end
wire RDC_softrst;
assign RDC_softrst = regs_i[BASE_MCCU_CFG][7];
RDC #(
// Width of data registers
.DATA_WIDTH (REG_WIDTH),
......@@ -468,7 +486,9 @@ end
// interruption signaling a signal has exceed the expected maximum request time
.interruption_rdc_o(intr_RDC_o),
// vector with offending signals. One hot encoding. Cleared when MCCU is disabled.
.interruption_vector_rdc_o(interruption_rdc_o)
.interruption_vector_rdc_o(interruption_rdc_o),
//maximum pulse length of a given core event
.watermark_o(MCCU_watermark_int)
);
/////////////////////////////////////////////////////////////////////////////////
//
......
......@@ -36,7 +36,7 @@
// Cores connected to MCCU
localparam MCCU_N_CORES = 4,
// Total amount of registers
parameter integer N_REGS = 26,
parameter integer N_REGS = 28,
// Number of configuration registers
localparam PMU_CFG = 1,
// Number of counters
......@@ -89,7 +89,6 @@
//----------------------------------------------
// VIVADO: list of debug signals for ILA
//----------------------------------------------
`define ILA_DEBUG_PMU_AHB
`ifdef ILA_DEBUG_PMU_AHB
(* MARK_DEBUG = "TRUE" *) wire debug_hsel_i ;
(* MARK_DEBUG = "TRUE" *) wire [HADDR_WIDTH-1:0] debug_haddr_i ;
......@@ -191,8 +190,6 @@ var struct packed{
logic [REG_WIDTH-1:0] slv_reg_D [0:N_REGS-1];
logic [REG_WIDTH-1:0] slv_reg_Q [0:N_REGS-1];
assign slv_reg_Q = slv_reg;
always_ff @(posedge clk_i, negedge rstn_i) begin
if(rstn_i == 1'b0 ) begin
slv_reg<='{default:0};
......@@ -267,7 +264,7 @@ end
//data phase - state update
always_ff @(posedge clk_i, negedge rstn_i) begin
if(rstn_i == 1'b0 ) begin
state<=TRANS_IDLE;
state <= TRANS_IDLE;
end else begin
state <= next;
end
......@@ -327,25 +324,7 @@ end
wire [REG_WIDTH-1:0] pmu_regs_int [0:N_REGS-1];
wire ahb_write_req;
assign ahb_write_req = address_phase.write && address_phase.select;
logic delay1_ahb_write_req;
logic [REG_WIDTH-1:0]delay1_dwrite_slave;
logic [$clog2(N_REGS)-1:0] delay1_slv_index;
//sice the modules that recieve the .wrapper_we_i get the value from
//slv_reg_Q it needs one cycle of delay to get the right value
//To avoid update the vaule of the slv_reg with old values from the PMU
//after a write slv_index dwrite_slave ahb_write_req are held for one
//cycle until the value is updated in .regs_o
always_ff @(posedge clk_i, negedge rstn_i) begin
if(rstn_i == 1'b0 ) begin
delay1_ahb_write_req <= 0;
delay1_dwrite_slave <= 0;
delay1_slv_index <= 0;
end else begin
delay1_ahb_write_req <= ahb_write_req;
delay1_dwrite_slave <= dwrite_slave;
delay1_slv_index <= slv_index;
end
end
PMU_raw #(
.REG_WIDTH(REG_WIDTH),
.N_COUNTERS(PMU_COUNTERS),
......@@ -355,7 +334,7 @@ end
.rstn_i(rstn_i),
.regs_i(slv_reg_Q),
.regs_o(pmu_regs_int),
.wrapper_we_i(delay1_ahb_write_req),
.wrapper_we_i(ahb_write_req),
//on pourpose .name connections
.events_i,
.intr_overflow_o,
......@@ -381,18 +360,13 @@ always_comb begin
//register the values given by pmu_raw
if(address_phase.write && address_phase.select) begin
// get the values from the pmu_raw instance
slv_reg_D=pmu_regs_int;
//If there is a write pending to be written and is not overwritten
//for the current write update two registers, else write only the
//most recent value
if(delay1_ahb_write_req && (delay1_slv_index!=slv_index)) begin
slv_reg_D[delay1_slv_index] = delay1_dwrite_slave;
slv_reg_Q = slv_reg;
slv_reg_Q [slv_index] = dwrite_slave;
slv_reg_D = pmu_regs_int;
slv_reg_D[slv_index] = dwrite_slave;
end else begin
slv_reg_D[slv_index] = dwrite_slave;
end
end else begin
slv_reg_D=pmu_regs_int;
slv_reg_D = pmu_regs_int;
slv_reg_Q = slv_reg;
end
end
......@@ -474,11 +448,19 @@ end
end
endgenerate
//Base configuration register remains stables if there isn't a reset or
//write
assert property (
no_ahb_write and no_counter_reset
|-> $stable(slv_reg_Q[0]) && $stable(pmu_regs_int[0]) && $stable(slv_reg[0])
);
//TODO: If counters cant decrease by their own what explains that we read
//incoherent values out of the pmu? AHB properties? Does it fail to read
//when only one core is available? Does only happen in multicore? What if
//nops are inserted after each read?
`endif
endmodule
......
......@@ -22,9 +22,9 @@
// Width of weights registers
parameter integer WEIGHTS_WIDTH = 8,
//Cores. Change this may break Verilator TB
parameter integer N_CORES =2,
parameter integer N_CORES =4,
//Signals per core. Change this may break Verilator TB
parameter integer CORE_EVENTS =4
parameter integer CORE_EVENTS =2
)
(
input wire clk_i,
......@@ -42,7 +42,11 @@
//Event longer than specified weight , single bit
output wire interruption_rdc_o,
//Interruption vector to indicate signal exceeding weight
output reg [CORE_EVENTS-1:0] interruption_vector_rdc_o [0:N_CORES-1]
output reg [CORE_EVENTS-1:0] interruption_vector_rdc_o [0:N_CORES-1],
//High watermark for each event of a given core.
output logic [WEIGHTS_WIDTH-1:0] watermark_o [0:N_CORES-1]
[0:CORE_EVENTS-1]
);
//-------------Adders with reset
......@@ -55,21 +59,30 @@
//Each clock cycle if the input signal (events_i) for a given counter is
//high at the positive edge of the clock the counter increases
localparam N_COUNTERS = CORE_EVENTS * N_CORES;
//reg [WEIGHTS_WIDTH-1 : 0] max_value [0 : N_COUNTERS-1];
reg [WEIGHTS_WIDTH-1 : 0] max_value [0 : N_COUNTERS-1];
//I need a bit to hold the interruption state until RCD is reset on
//disabled once the interrupt is risen
reg past_interruption_rdc_o;
genvar k;
genvar x;
genvar y;
generate
for (k=0; k<N_COUNTERS; k=k+1) begin : generated_counter
for(x=0;x<N_CORES;x++) begin
for(y=0;y<CORE_EVENTS;y++) begin
always_ff @(posedge clk_i, negedge rstn_i) begin
if(!rstn_i)
max_value[k] <={WEIGHTS_WIDTH{1'b0}};
max_value[CORE_EVENTS*x+y] <={WEIGHTS_WIDTH{1'b0}};
else begin
if(!enable_i || !events_i[k/CORE_EVENTS][k/N_CORES])
max_value[k] <={WEIGHTS_WIDTH{1'b0}};
else if(events_i[k/CORE_EVENTS][k/N_CORES] & enable_i)
max_value[k] <= max_value[k]+1;
if(enable_i && events_i[x][y]) begin
if(max_value[CORE_EVENTS*x+y]=={WEIGHTS_WIDTH{1'b1}}) begin
max_value[CORE_EVENTS*x+y] <= max_value[CORE_EVENTS*x+y];
end else begin
max_value[CORE_EVENTS*x+y] <= max_value[CORE_EVENTS*x+y]+1'b1;
end
end else begin
max_value[CORE_EVENTS*x+y] <={WEIGHTS_WIDTH{1'b0}};
end
end
end
end
end
......@@ -80,8 +93,6 @@
Interruption is only generated if the MCCU is enabled
----------*/
wire [CORE_EVENTS-1:0] interruption_vector_int [0:N_CORES-1];
genvar x;
genvar y;
generate
for(x=0;x<N_CORES;x++) begin
for(y=0;y<CORE_EVENTS;y++) begin
......@@ -127,23 +138,93 @@
//output interrupt if new interrupt or already on interrupt state
assign interruption_rdc_o = (|unpacked_vector_rdc_int) || past_interruption_rdc_o;
`ifdef ASSERTIONS
//-------------Watermark registers
logic [WEIGHTS_WIDTH-1 : 0] watermark_int [0 : N_COUNTERS-1];
genvar q;
generate
for (q=0; q<N_COUNTERS; q=q+1) begin : generated_watermark
always_ff @(posedge clk_i, negedge rstn_i) begin
if(!rstn_i) begin
watermark_int[q] <={WEIGHTS_WIDTH{1'b0}};
end else begin
if(!enable_i) begin
watermark_int[q] <= watermark_int[q];
end else begin
if (watermark_int[q] < max_value[q] )
watermark_int[q] <= max_value[q];
end
end
end
end
endgenerate
genvar n;
// n for iterate over cores
// q to iterate over signals
for (n=0; n<N_CORES; n=n+1) begin
for (q=0; q<CORE_EVENTS; q=q+1) begin
assign watermark_o[n][q] = watermark_int[n*CORE_EVENTS+q];
end
end
/////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
//auxiliar registers
reg f_past_valid ;
initial f_past_valid = 1'b0;
//Set f_past_valid after first clock cycle
always@( posedge clk_i )
f_past_valid <= 1'b1;
//Check that interrupt can only be removed by user or reset
integer sum_interruption_vector_rdc_o;
assign sum_interruption_vector_rdc_o = interruption_vector_rdc_o.sum();
/*
always@(posedge clk_i) begin
if(rstn_i && f_past_valid && enable_i)
//TODO: This assertion keeps failing. check again
assert (interruption_vector_rdc_o.sum()>=$past(interruption_vector_rdc_o.sum()));
end
*/
`endif
//assume that if f_past is not valid you have to reset
always @(*) begin
if(0 == f_past_valid) begin
assume(0 == rstn_i);
end
end
default clocking @(posedge clk_i); endclocking
//Check that counters never overflows
for(x=0;x<N_CORES;x++) begin
for(y=0;y<CORE_EVENTS;y++) begin
assert property (max_value[CORE_EVENTS*x+y]=={WEIGHTS_WIDTH{1'b1}}
and events_i[x][y]==1 and enable_i |=>
max_value[CORE_EVENTS*x+y]=={WEIGHTS_WIDTH{1'b1}} or rstn_i);
end
end
//Check that counters get to 0 in the next cycle if a signal is low
for(x=0;x<N_CORES;x++) begin
for(y=0;y<CORE_EVENTS;y++) begin
assert property (events_i[x][y]==0 |=> max_value[CORE_EVENTS*x+y]==0);
end
end
//Check that counters are map to the correct signals
for(x=0;x<N_CORES;x++) begin
for(y=0;y<CORE_EVENTS;y++) begin
assert property (events_i[x][y]==1 and enable_i==1 and rstn_i==1
|=> max_value[CORE_EVENTS*x+y] == {WEIGHTS_WIDTH{1'b1}} or
max_value[CORE_EVENTS*x+y]== $past(max_value[CORE_EVENTS*x+y])+1
or rstn_i==0 or enable_i ==0 );
end
end
for(x=0;x<N_CORES;x++) begin
for(y=0;y<CORE_EVENTS;y++) begin
cover property ((watermark_int[CORE_EVENTS*x+y] ==8'h10));
end
end
//The counter can get to 0 without reset or disable the enable
cover property ( f_past_valid and enable_i==1 and rstn_i==1 and events_i[0][0]==1
and $stable(enable_i) and $stable(rstn_i) and $stable(events_i[0][0])
|=> events_i[0][0]==0 and $stable(enable_i) and $stable(rstn_i)
);
`endif
endmodule
`default_nettype wire
This diff is collapsed.
[tasks]
bmc
cover
[options]
bmc:
mode bmc
depth 50
--
cover:
mode cover
depth 50
--
[engines]
bmc:
smtbmc boolector
smtbmc
#abc bmc3
--
cover:
smtbmc boolector
smtbmc
--
#SystemVerilog
[script]
verific -vlog-define FORMAL
verific -sv RDC.sv
verific -import -extnets -all RDC
prep -top RDC
[files]
../../../submodules/RDC/hdl/RDC.sv
#Check that the formal properties pass
sby -f RDC.sby $1 | \
GREP_COLORS='mt=01;31' egrep --color=always 'Unreached|Unreached cover statement at|Assert failed in|' | \
GREP_COLORS='mt=01;31' egrep -i --color=always 'FAIL|FAILED|ERROR|syntax|' | \
GREP_COLORS='mt=01;34' egrep --color=always 'Reached cover statement at|BMC|' | \
GREP_COLORS='mt=01;32' egrep -i --color=always 'PASS|PASSED|' | \
GREP_COLORS='mt=01;33' egrep -i --color=always 'WARNING|' | \
GREP_COLORS='mt=01;36' egrep -i --color=always 'Writing trace to VCD file:|counterexample trace:|'
#Run a particular case
#sby -f RDC_cover.sby
#Show the trace of the cover
#gtkwave ./RDC/engine_0/trace.vcd RDC.gtkw
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment