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

pre-refresh delay is now flexible and not fixed. Separated formal properties for testing time parameters

This commit is contained in:
AngeloJacobo 2023-07-05 16:35:57 +08:00
parent 217770b977
commit ce3ca7e158
1 changed files with 215 additions and 94 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

309
rtl/ddr3_controller.v
View File

@ -186,7 +186,9 @@ module ddr3_controller #(
localparam CWL_nCK = 5; //create a function for this localparam CWL_nCK = 5; //create a function for this
localparam DELAY_MAX_VALUE = ns_to_cycles(INITIAL_CKE_LOW); //Largest possible delay needed by the reset and refresh sequence localparam DELAY_MAX_VALUE = ns_to_cycles(INITIAL_CKE_LOW); //Largest possible delay needed by the reset and refresh sequence
localparam DELAY_COUNTER_WIDTH= $clog2(DELAY_MAX_VALUE); //Bitwidth needed by the maximum possible delay, this will be the delay counter width localparam DELAY_COUNTER_WIDTH= $clog2(DELAY_MAX_VALUE); //Bitwidth needed by the maximum possible delay, this will be the delay counter width
localparam PRE_STALL_DELAY = ((PRECHARGE_TO_ACTIVATE_DELAY+1) + (ACTIVATE_TO_WRITE_DELAY+1) + (WRITE_TO_PRECHARGE_DELAY+1) + 1)*2; localparam CALIBRATION_DELAY = 2;
localparam PRE_REFRESH_DELAY = WRITE_TO_PRECHARGE_DELAY + 1;
//localparam PRE_STALL_DELAY = ((PRECHARGE_TO_ACTIVATE_DELAY+1) + (ACTIVATE_TO_WRITE_DELAY+1) + (WRITE_TO_PRECHARGE_DELAY+1) + 1)*2;
//worst case scenario: two consecutive writes at same bank but different row //worst case scenario: two consecutive writes at same bank but different row
//delay will be: PRECHARGE -> PRECHARGE_TO_ACTIVATE_DELAY -> ACTIVATE -> ACTIVATE_TO_WRITE_DELAY -> WRITE -> WRITE_TO_PRECHARGE_DELAY -> //delay will be: PRECHARGE -> PRECHARGE_TO_ACTIVATE_DELAY -> ACTIVATE -> ACTIVATE_TO_WRITE_DELAY -> WRITE -> WRITE_TO_PRECHARGE_DELAY ->
//PRECHARGE -> PRECHARGE_TO_ACTIVATE_DELAY -> ACTIVATE -> ACTIVATE_TO_WRITE_DELAY -> WRITE -> WRITE_TO_PRECHARGE_DELAY //PRECHARGE -> PRECHARGE_TO_ACTIVATE_DELAY -> ACTIVATE -> ACTIVATE_TO_WRITE_DELAY -> WRITE -> WRITE_TO_PRECHARGE_DELAY
@ -303,7 +305,7 @@ module ddr3_controller #(
reg[ DELAY_COUNTER_WIDTH - 1:0] delay_counter = INITIAL_RESET_INSTRUCTION[DELAY_COUNTER_WIDTH - 1:0]; //counter used for delays reg[ DELAY_COUNTER_WIDTH - 1:0] delay_counter = INITIAL_RESET_INSTRUCTION[DELAY_COUNTER_WIDTH - 1:0]; //counter used for delays
reg delay_counter_is_zero = (INITIAL_RESET_INSTRUCTION[DELAY_COUNTER_WIDTH - 1:0] == 0); //counter is now zero so retrieve next delay reg delay_counter_is_zero = (INITIAL_RESET_INSTRUCTION[DELAY_COUNTER_WIDTH - 1:0] == 0); //counter is now zero so retrieve next delay
reg reset_done = 0; //high if reset has already finished reg reset_done = 0; //high if reset has already finished
reg skip_reset_seq_delay = 0; //flag to skip delay and go to next reset instruction reg pause_counter = 0;
wire issue_read_command; wire issue_read_command;
wire issue_write_command; wire issue_write_command;
reg[(1<<BA_BITS)-1:0] bank_status_q, bank_status_d; //bank_status[bank_number]: determine current state of bank (1=active , 0=idle) reg[(1<<BA_BITS)-1:0] bank_status_q, bank_status_d; //bank_status[bank_number]: determine current state of bank (1=active , 0=idle)
@ -523,7 +525,7 @@ module ddr3_controller #(
5'd11: read_rom_instruction = {5'b01011, CMD_NOP, tMOD}; 5'd11: read_rom_instruction = {5'b01011, CMD_NOP, tMOD};
//11. Delay of tMOD between MRS command to a non-MRS command excluding NOP and DES //11. Delay of tMOD between MRS command to a non-MRS command excluding NOP and DES
5'd12: read_rom_instruction = {5'b01011, CMD_NOP, {(DELAY_SLOT_WIDTH){1'b1}}}; 5'd12: read_rom_instruction = {5'b01011, CMD_NOP, CALIBRATION_DELAY[DELAY_SLOT_WIDTH-1:0]};
//12. Delay for read calibration //12. Delay for read calibration
5'd13: read_rom_instruction = {{2'b00,MR3_MPR_DIS[10], 2'b11}, CMD_MRS, MR3_MPR_DIS}; 5'd13: read_rom_instruction = {{2'b00,MR3_MPR_DIS[10], 2'b11}, CMD_MRS, MR3_MPR_DIS};
@ -535,7 +537,7 @@ module ddr3_controller #(
5'd15: read_rom_instruction = {5'b01011, CMD_NOP, tWLMRD}; 5'd15: read_rom_instruction = {5'b01011, CMD_NOP, tWLMRD};
//15. Delay of tMOD between MRS command to a non-MRS command excluding NOP and DES //15. Delay of tMOD between MRS command to a non-MRS command excluding NOP and DES
5'd16: read_rom_instruction = {5'b01011, CMD_NOP, {(DELAY_SLOT_WIDTH){1'b1}}}; 5'd16: read_rom_instruction = {5'b01011, CMD_NOP, CALIBRATION_DELAY[DELAY_SLOT_WIDTH-1:0]};
//16. Delay for write calibration //16. Delay for write calibration
5'd17: read_rom_instruction = {{2'b00,MR1_WL_DIS[10], 2'b11}, CMD_MRS, MR1_WL_DIS}; 5'd17: read_rom_instruction = {{2'b00,MR1_WL_DIS[10], 2'b11}, CMD_MRS, MR1_WL_DIS};
@ -555,7 +557,7 @@ module ddr3_controller #(
5'd21: read_rom_instruction = {5'b11011, CMD_NOP, ns_to_cycles(tREFI)}; 5'd21: read_rom_instruction = {5'b11011, CMD_NOP, ns_to_cycles(tREFI)};
//21. Reset ends now. The refresh interval also starts to count. //21. Reset ends now. The refresh interval also starts to count.
5'd22: read_rom_instruction = {5'b01011, CMD_NOP, PRE_STALL_DELAY[DELAY_SLOT_WIDTH-1:0]}; 5'd22: read_rom_instruction = {5'b01011, CMD_NOP, PRE_REFRESH_DELAY[DELAY_SLOT_WIDTH-1:0]};
// 22. Extra delay needed before starting the refresh sequence. // 22. Extra delay needed before starting the refresh sequence.
// (this already sets the wishbone stall high to make sure no user request is on-going when refresh seqeunce starts) // (this already sets the wishbone stall high to make sure no user request is on-going when refresh seqeunce starts)
@ -590,11 +592,15 @@ module ddr3_controller #(
end end
//else: decrement delay counter when current instruction needs delay //else: decrement delay counter when current instruction needs delay
else if(instruction[USE_TIMER]) delay_counter <= delay_counter - 1; //don't decrement (has infinite time) when last bit of
//delay_counter is 1 (for r/w calibration and prestall delay)
//address will only move forward for these kinds of delay only
//when skip_reset_seq_delay is toggled
else if(instruction[USE_TIMER] /*&& delay_counter != {(DELAY_COUNTER_WIDTH){1'b1}}*/ && !pause_counter) delay_counter <= delay_counter - 1;
//delay_counter of 1 means we will need to update the delay_counter next clock cycle (delay_counter of zero) so we need to retrieve //delay_counter of 1 means we will need to update the delay_counter next clock cycle (delay_counter of zero) so we need to retrieve
//now the next instruction. The same thing needs to be done when current instruction does not need the timer delay. //now the next instruction. The same thing needs to be done when current instruction does not need the timer delay.
if(delay_counter == 1 || !instruction[USE_TIMER] || skip_reset_seq_delay) begin if(delay_counter == 1 || !instruction[USE_TIMER]/* || skip_reset_seq_delay*/) begin
delay_counter_is_zero <= 1; delay_counter_is_zero <= 1;
instruction <= read_rom_instruction(instruction_address); instruction <= read_rom_instruction(instruction_address);
instruction_address <= (instruction_address == 5'd22)? 5'd19:instruction_address+1; //wrap back of address to repeat refresh sequence instruction_address <= (instruction_address == 5'd22)? 5'd19:instruction_address+1; //wrap back of address to repeat refresh sequence
@ -956,7 +962,7 @@ module ddr3_controller #(
end //end of stage 2 pending end //end of stage 2 pending
//pending request on stage 1 //pending request on stage 1
if(stage1_pending && (stage1_next_bank != stage2_bank)) begin if(stage1_pending && !((stage1_next_bank == stage2_bank) && stage2_pending)) begin
//stage 1 will mainly be for anticipation, but it can also handle //stage 1 will mainly be for anticipation, but it can also handle
//precharge and activate request. This will depend if the request //precharge and activate request. This will depend if the request
//is on the end of the row and must start the anticipation. For //is on the end of the row and must start the anticipation. For
@ -1202,7 +1208,7 @@ module ddr3_controller #(
write_calib_we <= 0; //write-enable write_calib_we <= 0; //write-enable
write_calib_col <= 0; write_calib_col <= 0;
write_calib_data <= 0; write_calib_data <= 0;
skip_reset_seq_delay <= 0; pause_counter <= 0;
read_data_store <= 0; read_data_store <= 0;
write_pattern <= 0; write_pattern <= 0;
added_read_pipe_max <= 0; added_read_pipe_max <= 0;
@ -1225,7 +1231,6 @@ module ddr3_controller #(
write_calib_we <= 0; //write-enable write_calib_we <= 0; //write-enable
write_calib_col <= 0; write_calib_col <= 0;
write_calib_data <= 0; write_calib_data <= 0;
skip_reset_seq_delay <= 0;
write_calib_dqs <= 0; write_calib_dqs <= 0;
write_calib_dq <= 0; write_calib_dq <= 0;
train_delay <= (train_delay==0)? 0:(train_delay - 1); train_delay <= (train_delay==0)? 0:(train_delay - 1);
@ -1264,6 +1269,10 @@ module ddr3_controller #(
o_phy_odelay_dqs_ld <= {LANES{1'b1}}; o_phy_odelay_dqs_ld <= {LANES{1'b1}};
o_phy_idelay_data_ld <= {LANES{1'b1}}; o_phy_idelay_data_ld <= {LANES{1'b1}};
o_phy_idelay_dqs_ld <= {LANES{1'b1}}; o_phy_idelay_dqs_ld <= {LANES{1'b1}};
pause_counter <= 1; //pause instruction address @13 until read calibration finishes
end
else if(instruction_address == 13) begin
pause_counter <= 1; //pause instruction address @13 until read calibration finishes
end end
BITSLIP_DQS_TRAIN_1: if(train_delay == 0) begin BITSLIP_DQS_TRAIN_1: if(train_delay == 0) begin
/* Bitslip cannot be asserted for two consecutive CLKDIV cycles; Bitslip must be /* Bitslip cannot be asserted for two consecutive CLKDIV cycles; Bitslip must be
@ -1286,7 +1295,6 @@ module ddr3_controller #(
end end
MPR_READ: begin //align the incoming DQS during reads to the controller clock MPR_READ: begin //align the incoming DQS during reads to the controller clock
//skip_reset_seq_delay = 1;
//issue_read_command = 1; //issue_read_command = 1;
delay_before_read_data <= READ_DELAY + 1 + 2 + 1 /*- 1*/; ///1=issue command delay (OSERDES delay), 2 = ISERDES delay delay_before_read_data <= READ_DELAY + 1 + 2 + 1 /*- 1*/; ///1=issue command delay (OSERDES delay), 2 = ISERDES delay
state_calibrate <= COLLECT_DQS; state_calibrate <= COLLECT_DQS;
@ -1333,7 +1341,7 @@ module ddr3_controller #(
BITSLIP_DQS_TRAIN_2: if(train_delay == 0) begin //train again the ISERDES to capture the DQ correctly BITSLIP_DQS_TRAIN_2: if(train_delay == 0) begin //train again the ISERDES to capture the DQ correctly
if(i_phy_iserdes_bitslip_reference[lane*LANES +: 8] == dqs_bitslip_arrangement) begin if(i_phy_iserdes_bitslip_reference[lane*LANES +: 8] == dqs_bitslip_arrangement) begin
if(lane == LANES - 1) begin if(lane == LANES - 1) begin
skip_reset_seq_delay <= 1; pause_counter <= 0; //read calibration now complete so continue the reset instruction sequence
lane <= 0; lane <= 0;
prev_write_level_feedback <= 1'b1; prev_write_level_feedback <= 1'b1;
state_calibrate <= START_WRITE_LEVEL; state_calibrate <= START_WRITE_LEVEL;
@ -1355,6 +1363,7 @@ module ddr3_controller #(
write_calib_odt <= 1'b1; write_calib_odt <= 1'b1;
delay_before_write_level_feedback <= DELAY_BEFORE_WRITE_LEVEL_FEEDBACK; delay_before_write_level_feedback <= DELAY_BEFORE_WRITE_LEVEL_FEEDBACK;
state_calibrate <= WAIT_FOR_FEEDBACK; state_calibrate <= WAIT_FOR_FEEDBACK;
pause_counter <= 1; // pause instruction address @17 until write calibration finishes
end end
WAIT_FOR_FEEDBACK: if(delay_before_write_level_feedback == 0) begin WAIT_FOR_FEEDBACK: if(delay_before_write_level_feedback == 0) begin
@ -1362,7 +1371,7 @@ module ddr3_controller #(
if({prev_write_level_feedback, i_phy_iserdes_data[lane<<3]} == 2'b01) begin if({prev_write_level_feedback, i_phy_iserdes_data[lane<<3]} == 2'b01) begin
if(lane == LANES - 1) begin if(lane == LANES - 1) begin
write_calib_odt <= 0; write_calib_odt <= 0;
skip_reset_seq_delay <= 1; pause_counter <= 0; //write calibration now complete so continue the reset instruction sequence
lane <= 0; lane <= 0;
state_calibrate <= ISSUE_WRITE_1; state_calibrate <= ISSUE_WRITE_1;
end end
@ -1386,7 +1395,7 @@ module ddr3_controller #(
write_calib_data <= { {LANES{8'h91}}, {LANES{8'h77}}, {LANES{8'h29}}, {LANES{8'h8c}}, {LANES{8'hd0}}, {LANES{8'had}}, {LANES{8'h51}}, {LANES{8'hc1}} }; write_calib_data <= { {LANES{8'h91}}, {LANES{8'h77}}, {LANES{8'h29}}, {LANES{8'h8c}}, {LANES{8'hd0}}, {LANES{8'had}}, {LANES{8'h51}}, {LANES{8'hc1}} };
state_calibrate <= ISSUE_WRITE_2; state_calibrate <= ISSUE_WRITE_2;
end end
ISSUE_WRITE_2: if(!o_wb_stall_q) begin ISSUE_WRITE_2: begin
write_calib_stb <= 1;//actual request flag write_calib_stb <= 1;//actual request flag
write_calib_aux <= 1; //AUX ID to determine later if ACK is for read or write write_calib_aux <= 1; //AUX ID to determine later if ACK is for read or write
write_calib_we <= 1; //write-enable write_calib_we <= 1; //write-enable
@ -1394,7 +1403,7 @@ module ddr3_controller #(
write_calib_data <= { {LANES{8'h80}}, {LANES{8'hdb}}, {LANES{8'hcf}}, {LANES{8'hd2}}, {LANES{8'h75}}, {LANES{8'hf1}}, {LANES{8'h2c}}, {LANES{8'h3d}} }; write_calib_data <= { {LANES{8'h80}}, {LANES{8'hdb}}, {LANES{8'hcf}}, {LANES{8'hd2}}, {LANES{8'h75}}, {LANES{8'hf1}}, {LANES{8'h2c}}, {LANES{8'h3d}} };
state_calibrate <= ISSUE_READ; state_calibrate <= ISSUE_READ;
end end
ISSUE_READ: if(!o_wb_stall_q) begin ISSUE_READ: if(!o_wb_stall_q && write_calib_stb == 0) begin
write_calib_stb <= 1;//actual request flag write_calib_stb <= 1;//actual request flag
write_calib_aux <= 0; //AUX ID to determine later if ACK is for read or write write_calib_aux <= 0; //AUX ID to determine later if ACK is for read or write
write_calib_we <= 0; //write-enable write_calib_we <= 0; //write-enable
@ -1428,7 +1437,17 @@ module ddr3_controller #(
else begin else begin
data_start_index[lane] <= data_start_index[lane] + 8; data_start_index[lane] <= data_start_index[lane] + 8;
end end
DONE_CALIBRATE: state_calibrate <= DONE_CALIBRATE; DONE_CALIBRATE: begin
state_calibrate <= DONE_CALIBRATE;
if(instruction_address == 19) begin //pre-stall delay to finish all remaining requests
pause_counter <= 1; // pause instruction address until pre-stall delay before refresh sequence finishes
//skip to instruction address 20 (precharge all before refresh) when no pending requests anymore
//toggle it for 1 clk cycle only
if(!stage1_pending && !stage2_pending && o_wb_stall) begin
pause_counter <= 0; // pre-stall delay done since all remaining requests are completed
end
end
end
endcase endcase
`ifdef FORMAL_COVER `ifdef FORMAL_COVER
@ -1638,7 +1657,9 @@ module ddr3_controller #(
`endif `endif
`ifdef FORMAL `ifdef FORMAL
`define TEST_TIME_PARAMETERS
`ifdef FORMAL_COVER `ifdef FORMAL_COVER
initial assume(!i_rst_n); initial assume(!i_rst_n);
reg[24:0] f_wb_inputs[31:0]; reg[24:0] f_wb_inputs[31:0];
@ -1740,9 +1761,157 @@ module ddr3_controller #(
assume(i_rst_n); //dont reset just to skip a request forcefully assume(i_rst_n); //dont reset just to skip a request forcefully
end end
end end
`endif //endif for FORMAL_COVER
`else
//`define TEST_DATA `ifdef TEST_TIME_PARAMETERS
// Test time parameter violations
(*keep*) reg[6:0] f_precharge_time_stamp[(1<<BA_BITS)-1:0];
(*keep*) reg[6:0] f_activate_time_stamp[(1<<BA_BITS)-1:0];
reg[6:0] f_read_time_stamp[(1<<BA_BITS)-1:0];
reg[6:0] f_write_time_stamp[(1<<BA_BITS)-1:0];
reg[6:0] f_timer = 0;
reg f_past_valid = 0;
initial assume(!i_rst_n);
always @(posedge i_controller_clk) f_past_valid <= 1;
always @(posedge i_controller_clk) begin
f_timer <= f_timer + 4;
if(f_past_valid) begin
assume($past(f_timer) < f_timer); //assume that counter will never overflow
end
end
always @(posedge i_controller_clk, negedge i_rst_n) begin
if(!i_rst_n) begin
for(index=0; index < (1<<BA_BITS); index=index+1) begin
f_precharge_time_stamp[index] <= 0;
f_activate_time_stamp[index] <= 0;
f_read_time_stamp[index] <= 0;
f_write_time_stamp[index] <= 0;
end
end
else begin
//check if a DDR3 command is issued
if(cmd_d[PRECHARGE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0010) begin //PRECHARGE
f_precharge_time_stamp[cmd_d[PRECHARGE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] <= f_timer + PRECHARGE_SLOT;
end
if(cmd_d[ACTIVATE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0011) begin //ACTIVATE
f_activate_time_stamp[cmd_d[ACTIVATE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] <= f_timer + ACTIVATE_SLOT;
end
if(cmd_d[WRITE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0100) begin //WRITE
f_write_time_stamp[cmd_d[WRITE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] <= f_timer + WRITE_SLOT;
end
if(cmd_d[READ_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0101) begin //READ
f_read_time_stamp[cmd_d[READ_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] <= f_timer + READ_SLOT;
end
end
end
always @* begin
// to make sure saved time stamp is valid
for(index=0; index < (1<<BA_BITS); index=index+1) begin
assert(f_precharge_time_stamp[index] <= f_timer);
assert(f_activate_time_stamp[index] <= f_timer);
assert(f_read_time_stamp[index] <= f_timer);
assert(f_write_time_stamp[index] <= f_timer);
// Check tRTP (Internal READ Command to PRECHARGE Command delay in SAME BANK)
if(f_precharge_time_stamp[index] > f_read_time_stamp[index]) begin
assert((f_precharge_time_stamp[index] - f_read_time_stamp[index]) >= ns_to_nCK(tRTP));
end
/*
// Check tWTR (Delay from start of internal write transaction to internal read command)
if(f_read_time_stamp[index] > f_write_time_stamp[index]) begin
assert((f_read_time_stamp[index] - f_write_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tWTR)
end
*/
// Check tRCD (ACT to internal read or write delay time)
if(f_read_time_stamp[index] > f_activate_time_stamp[index]) begin
assert((f_read_time_stamp[index] - f_activate_time_stamp[index]) >= ns_to_nCK(tRCD));
end
if(f_write_time_stamp[index] > f_activate_time_stamp[index]) begin
assert((f_write_time_stamp[index] - f_activate_time_stamp[index]) >= ns_to_nCK(tRCD));
end
// Check tRP (PRE command period)
if(f_activate_time_stamp[index] > f_precharge_time_stamp[index]) begin
assert((f_activate_time_stamp[index] - f_precharge_time_stamp[index]) >= ns_to_nCK(tRP));
end
// Check tRAS (ACTIVE to PRECHARGE command period)
if(f_precharge_time_stamp[index] > f_activate_time_stamp[index]) begin
assert((f_precharge_time_stamp[index] - f_activate_time_stamp[index]) >= ns_to_nCK(tRAS));
end
end
end
// assertion on FSM calibration
always @* begin
assert(instruction_address <= 22);
assert(state_calibrate <= DONE_CALIBRATE);
if(instruction_address < 13) begin
assert(state_calibrate == IDLE);
end
if(state_calibrate > IDLE && state_calibrate <= BITSLIP_DQS_TRAIN_2) begin
assert(instruction_address == 13);
assert(pause_counter);
end
if(state_calibrate > START_WRITE_LEVEL && state_calibrate <= WAIT_FOR_FEEDBACK) begin
assert(instruction_address == 17);
assert(pause_counter);
end
if(pause_counter) begin
assert(delay_counter != 0);
end
if(state_calibrate > ISSUE_WRITE_1 && state_calibrate < DONE_CALIBRATE) begin
assume(instruction_address == 22); //write-then-read calibration will not take more than tREFI (7.8us, delay a address 22)
assert(reset_done);
end
if(state_calibrate == DONE_CALIBRATE) begin
assert(reset_done);
assert(instruction_address >= 19);
end
if(reset_done) begin
assert(instruction_address >= 19);
end
if(!reset_done) begin
assert(!stage1_pending && !stage2_pending);
assert(o_wb_stall);
end
if(reset_done) begin
assert(instruction_address >= 19 && instruction_address <= 22);
end
//delay_counter is zero at first clock of new instruction address, the actual delay_clock wil start at next clock cycle
if(instruction_address == 19 && delay_counter != 0) begin
assert(o_wb_stall);
end
if(instruction_address == 19 && pause_counter) begin //pre-stall delay to finish all remaining requests
assert(delay_counter == PRE_REFRESH_DELAY);
assert(reset_done);
assert(DONE_CALIBRATE);
end
end
`endif //endif for TEST_TIME_PARAMETERS
`ifdef TEST_CONTROLLER_PIPELINE
// wires and registers used in this formal section // wires and registers used in this formal section
`ifdef TEST_DATA `ifdef TEST_DATA
localparam F_TEST_CMD_DATA_WIDTH = $bits(i_wb_data) + $bits(i_wb_sel) + $bits(i_aux) + $bits(i_wb_addr) + $bits(i_wb_we); localparam F_TEST_CMD_DATA_WIDTH = $bits(i_wb_data) + $bits(i_wb_sel) + $bits(i_aux) + $bits(i_wb_addr) + $bits(i_wb_we);
@ -1809,7 +1978,7 @@ module ddr3_controller #(
f_read <= 0; f_read <= 0;
end end
//move the pipeline forward when counter is about to go zero and we are not yet at end of reset sequence //move the pipeline forward when counter is about to go zero and we are not yet at end of reset sequence
else if((delay_counter == 1 || !instruction[USE_TIMER] || skip_reset_seq_delay)) begin else if((delay_counter == 1 || !instruction[USE_TIMER])) begin
f_addr <= (f_addr == 22)? 19:f_addr + 1; f_addr <= (f_addr == 22)? 19:f_addr + 1;
f_read <= f_addr; f_read <= f_addr;
end end
@ -1841,11 +2010,11 @@ module ddr3_controller #(
assert(delay_counter == f_read_inst[DELAY_COUNTER_WIDTH - 1:0]); assert(delay_counter == f_read_inst[DELAY_COUNTER_WIDTH - 1:0]);
end end
//delay_counter_is_zero can be high when counter is zero and current instruction needs delay //delay_counter_is_zero can be high when counter is zero and current instruction needs delay
if($past(f_read_inst[USE_TIMER]) && !$past(skip_reset_seq_delay) ) begin if($past(f_read_inst[USE_TIMER]) && !$past(pause_counter) ) begin
assert( delay_counter_is_zero == (delay_counter == 0) ); assert( delay_counter_is_zero == (delay_counter == 0) );
end end
//delay_counter_is_zero will go high this cycle when we received a don't-use-timer instruction //delay_counter_is_zero will go high this cycle when we received a don't-use-timer instruction
else if(!$past(f_read_inst[USE_TIMER]) && !$past(skip_reset_seq_delay)) begin else if(!$past(f_read_inst[USE_TIMER]) && !$past(pause_counter)) begin
assert(delay_counter_is_zero); assert(delay_counter_is_zero);
end end
@ -1857,13 +2026,13 @@ module ddr3_controller #(
end end
//if delay is not yet zero and timer delay is enabled, then delay_counter should decrement //if delay is not yet zero and timer delay is enabled, then delay_counter should decrement
if(!$past(delay_counter_is_zero) && $past(f_read_inst[USE_TIMER])) begin if(!$past(delay_counter_is_zero) && $past(f_read_inst[USE_TIMER]) && !$past(pause_counter) ) begin
assert(delay_counter == $past(delay_counter) - 1); assert(delay_counter == $past(delay_counter) - 1);
assert(delay_counter < $past(delay_counter) ); //just to make sure delay_counter will never overflow back to all 1's assert(delay_counter < $past(delay_counter) ); //just to make sure delay_counter will never overflow back to all 1's
end end
//sanity checking for the comment "delay_counter will be zero AT NEXT CLOCK CYCLE when counter is now one" //sanity checking for the comment "delay_counter will be zero AT NEXT CLOCK CYCLE when counter is now one"
if($past(delay_counter) == 1 && !$past(skip_reset_seq_delay,2)) begin if($past(delay_counter) == 1) begin
assert(delay_counter == 0 && delay_counter_is_zero); assert(delay_counter == 0 && delay_counter_is_zero);
end end
//assert the relationship between the stages FOR RESET SEQUENCE //assert the relationship between the stages FOR RESET SEQUENCE
@ -1931,14 +2100,17 @@ module ddr3_controller #(
if(state_calibrate > IDLE && state_calibrate <= BITSLIP_DQS_TRAIN_2) begin if(state_calibrate > IDLE && state_calibrate <= BITSLIP_DQS_TRAIN_2) begin
assert(instruction_address == 13); assert(instruction_address == 13);
assert(pause_counter);
end end
if(state_calibrate > START_WRITE_LEVEL && state_calibrate <= WAIT_FOR_FEEDBACK) begin if(state_calibrate > START_WRITE_LEVEL && state_calibrate <= WAIT_FOR_FEEDBACK) begin
assert(instruction_address == 17); assert(instruction_address == 17);
assert(pause_counter);
end end
if(instruction_address == 13 || instruction_address == 17) begin if(pause_counter) begin
assume(delay_counter != 1); //read (address 13) and write(17) will not take more than the max delay (500us) assert(delay_counter != 0);
end end
if(state_calibrate > ISSUE_WRITE_1 && state_calibrate < DONE_CALIBRATE) begin if(state_calibrate > ISSUE_WRITE_1 && state_calibrate < DONE_CALIBRATE) begin
@ -2035,7 +2207,7 @@ module ddr3_controller #(
if(stage1_pending && $past(state_calibrate) == READ_DATA && state_calibrate == READ_DATA) begin if(stage1_pending && $past(state_calibrate) == READ_DATA && state_calibrate == READ_DATA) begin
assert(!stage1_we); assert(!stage1_we);
end end
if(instruction_address == 21 || (instruction_address == 20 && delay_counter != 0) || instruction_address < 19) begin //not inside active or calibration if(instruction_address == 21 || ($past(instruction_address) == 20 && $past(instruction_address,2) == 19) || instruction_address < 19) begin //not inside active or calibration
assert(f_bank_status == 0); assert(f_bank_status == 0);
assert(bank_status_q == 0); assert(bank_status_q == 0);
end end
@ -2105,6 +2277,7 @@ module ddr3_controller #(
else if(state_calibrate > ISSUE_WRITE_1) begin else if(state_calibrate > ISSUE_WRITE_1) begin
assert(stage2_aux == 1); assert(stage2_aux == 1);
end end
//assert(f_bank_active_row[cmd_d[WRITE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] == current_row); //column to be written must be the current active row
end end
if(cmd_d[READ_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0101) begin //READ if(cmd_d[READ_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0101) begin //READ
@ -2127,6 +2300,7 @@ module ddr3_controller #(
else if(state_calibrate > ISSUE_WRITE_1) begin else if(state_calibrate > ISSUE_WRITE_1) begin
assert(stage2_aux == 0); assert(stage2_aux == 0);
end end
//assert(f_bank_active_row[cmd_d[READ_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] == current_row);//column to be written must be the current active row
end end
if(cmd_d[PRECHARGE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0010) begin //PRECHARGE if(cmd_d[PRECHARGE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0010) begin //PRECHARGE
@ -2186,14 +2360,13 @@ module ddr3_controller #(
//check if a DDR3 command is issued //check if a DDR3 command is issued
if(cmd_d[PRECHARGE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0010) begin //PRECHARGE if(cmd_d[PRECHARGE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0010) begin //PRECHARGE
bank = cmd_d[PRECHARGE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]; bank = cmd_d[PRECHARGE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1];
f_precharge_time_stamp[bank] <= f_timer; f_precharge_time_stamp[bank] <= f_timer + PRECHARGE_SLOT;
if(cmd_d[PRECHARGE_SLOT][10]) begin //A10 precharge all banks if(cmd_d[PRECHARGE_SLOT][10]) begin //A10 precharge all banks
for(index=0; index < (1<<BA_BITS); index=index+1) begin for(index=0; index < (1<<BA_BITS); index=index+1) begin
f_bank_status_2[index] = 0; f_bank_status_2[index] = 0;
end end
end end
else begin else begin
f_precharge_time_stamp[bank] <= 1;
//f_bank_status <= f_bank_status & ~(1<<bank); //set to zero to idle bank //f_bank_status <= f_bank_status & ~(1<<bank); //set to zero to idle bank
//f_bank_status[bank] <= 0; //set to zero to idle bank //f_bank_status[bank] <= 0; //set to zero to idle bank
f_bank_status_2 = f_bank_status_2 & ~(1<<bank); //set to zero to idle bank f_bank_status_2 = f_bank_status_2 & ~(1<<bank); //set to zero to idle bank
@ -2203,7 +2376,7 @@ module ddr3_controller #(
if(cmd_d[ACTIVATE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0011) begin //ACTIVATE if(cmd_d[ACTIVATE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0011) begin //ACTIVATE
bank = cmd_d[ACTIVATE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]; bank = cmd_d[ACTIVATE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1];
f_activate_time_stamp[bank] <= f_timer; f_activate_time_stamp[bank] <= f_timer + ACTIVATE_SLOT;
// f_bank_status <= f_bank_status | (1<<bank); //bank will be turned active // f_bank_status <= f_bank_status | (1<<bank); //bank will be turned active
//f_bank_status[bank] <= 1; //f_bank_status[bank] <= 1;
assert(bank <= 7); assert(bank <= 7);
@ -2211,6 +2384,14 @@ module ddr3_controller #(
f_bank_active_row[bank] <= cmd_d[ACTIVATE_SLOT][CMD_ADDRESS_START:0]; //save row to be activated f_bank_active_row[bank] <= cmd_d[ACTIVATE_SLOT][CMD_ADDRESS_START:0]; //save row to be activated
end end
f_bank_status <= f_bank_status_2; f_bank_status <= f_bank_status_2;
if(cmd_d[WRITE_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0100) begin //WRITE
f_write_time_stamp[cmd_d[WRITE_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] <= f_timer + WRITE_SLOT;
end
if(cmd_d[READ_SLOT][CMD_CS_N:CMD_WE_N] == 4'b0101) begin //READ
f_read_time_stamp[cmd_d[READ_SLOT][CMD_BANK_START:CMD_ADDRESS_START+1]] <= f_timer + READ_SLOT;
end
/* /*
if(!cmd_d[f_index_2][CMD_CS_N]) begin //only if already done calibrate and controller can accept wb request if(!cmd_d[f_index_2][CMD_CS_N]) begin //only if already done calibrate and controller can accept wb request
case(cmd_d[f_index_2][CMD_CS_N:CMD_WE_N]) case(cmd_d[f_index_2][CMD_CS_N:CMD_WE_N])
@ -2269,8 +2450,9 @@ module ddr3_controller #(
if(instruction_address == 19 && delay_counter != 0) begin if(instruction_address == 19 && delay_counter != 0) begin
assert(o_wb_stall); assert(o_wb_stall);
end end
if(instruction_address == 19 && delay_counter == PRE_STALL_DELAY/2) begin if(instruction_address == 20 || instruction_address == 21) begin //no pending request at precharge all and refresh command
assert(!stage1_pending); assert(!stage1_pending);
assert(!stage2_pending);
end end
if($past(o_wb_stall_q) && stage1_pending) begin //if pipe did not move forward if($past(o_wb_stall_q) && stage1_pending) begin //if pipe did not move forward
assert(stage1_we == $past(stage1_we)); assert(stage1_we == $past(stage1_we));
@ -2395,67 +2577,6 @@ module ddr3_controller #(
end end
end end
// Test time parameter violations
always @(posedge i_controller_clk) begin
f_timer <= f_timer + 1;
if(f_past_valid) begin
assume($past(f_timer) < f_timer); //assume that counter will never overflow
end
end
`ifdef UNDER_CONSTRUCTION
always @* begin
// to make sure saved time stamp is valid
for(index=0; index < (1<<BA_BITS); index=index+1) begin
assert(f_precharge_time_stamp[index] <= f_timer);
assert(f_activate_time_stamp[index] <= f_timer);
assert(f_read_time_stamp[index] <= f_timer);
assert(f_write_time_stamp[index] <= f_timer);
// Check tRTP (Internal READ Command to PRECHARGE Command delay in SAME BANK)
if(f_precharge_time_stamp[index] > f_read_time_stamp[index]) begin
assert((f_precharge_time_stamp[index] - f_read_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tRTP);
end
/*
// Check tWTR (Delay from start of internal write transaction to internal read command)
if(f_read_time_stamp[index] > f_write_time_stamp[index]) begin
assert((f_read_time_stamp[index] - f_write_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tWTR)
end
*/
// Check tRCD (ACT to internal read or write delay time)
if(f_read_time_stamp[index] > f_activate_time_stamp[index]) begin
assert((f_read_time_stamp[index] - f_activate_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tRCD);
end
if(f_write_time_stamp[index] > f_activate_time_stamp[index]) begin
assert((f_write_time_stamp[index] - f_activate_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tRCD);
end
// Check tRP (PRE command period)
if(f_activate_time_stamp[index] > f_precharge_time_stamp[index]) begin
assert((f_activate_time_stamp[index] - f_precharge_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tRP);
end
// Check tRAS (ACTIVE to PRECHARGE command period)
if(f_precharge_time_stamp[index] > f_activate_time_stamp[index]) begin
assert((f_precharge_time_stamp[index] - f_activate_time_stamp[index])*CONTROLLER_CLK_PERIOD >= tRAS);
end
end
end
localparam PRECHARGE_TO_ACTIVATE_DELAY = find_delay(ns_to_nCK(tRP), PRECHARGE_SLOT, ACTIVATE_SLOT); //3
localparam ACTIVATE_TO_PRECHARGE_DELAY = find_delay(ns_to_nCK(tRAS), ACTIVATE_SLOT, PRECHARGE_SLOT);
localparam ACTIVATE_TO_WRITE_DELAY = find_delay(ns_to_nCK(tRCD), ACTIVATE_SLOT, WRITE_SLOT); //3
localparam ACTIVATE_TO_READ_DELAY = find_delay(ns_to_nCK(tRCD), ACTIVATE_SLOT, READ_SLOT); //2
localparam READ_TO_WRITE_DELAY = find_delay((CL_nCK + tCCD + 3'd2 - CWL_nCK), READ_SLOT, WRITE_SLOT); //2
localparam READ_TO_READ_DELAY = 0;
localparam READ_TO_PRECHARGE_DELAY = find_delay(ns_to_nCK(tRTP), READ_SLOT, PRECHARGE_SLOT); //1
localparam WRITE_TO_WRITE_DELAY = 0;
localparam WRITE_TO_READ_DELAY = find_delay((CWL_nCK + 3'd4 + ns_to_nCK(tWTR)), WRITE_SLOT, READ_SLOT); //4
localparam WRITE_TO_PRECHARGE_DELAY = find_delay((CWL_nCK + 3'd4 + ns_to_nCK(tWR)), WRITE_SLOT, PRECHARGE_SLOT); //5
`endif
fwb_slave #( fwb_slave #(
// {{{ // {{{
@ -2514,7 +2635,7 @@ module ddr3_controller #(
// }}} // }}}
// }}} // }}}
); );
`endif //endif for FORMAL_COVER `endif //endif for TEST_CONTROLLER_PIPELINE
`endif //endif for FORMAL `endif //endif for FORMAL
endmodule endmodule