From 43e645151ed6e269bc96fd2cb0fc957cf57fcc4a Mon Sep 17 00:00:00 2001 From: fjpolo Date: Thu, 4 Jul 2024 16:36:22 +0200 Subject: [PATCH] Proper rebase --- src/.gitignore | 14 + src/sdram_nes.sby | 42 +++ src/sdram_nes.v | 816 ++++++++++++++++++++++++++++++---------------- 3 files changed, 583 insertions(+), 289 deletions(-) create mode 100644 src/.gitignore create mode 100644 src/sdram_nes.sby diff --git a/src/.gitignore b/src/.gitignore new file mode 100644 index 0000000..c0a7c4e --- /dev/null +++ b/src/.gitignore @@ -0,0 +1,14 @@ +wishbone_slave/ +wishbone_slave_bound/ +wishbone_slave_prf/ +wishbone_slave_cvr/ + +cheat_wizard/ +cheat_wizard_bound/ +cheat_wizard_prf/ +cheat_wizard_cvr/ + +sdram_nes_sdram/ +sdram_nes_sdram_init/ +sdram_nes_sdram_refresh/ +sdram_nes_sdram_rw/ \ No newline at end of file diff --git a/src/sdram_nes.sby b/src/sdram_nes.sby new file mode 100644 index 0000000..937e066 --- /dev/null +++ b/src/sdram_nes.sby @@ -0,0 +1,42 @@ +[tasks] +sdram_init +sdram_refresh +sdram_rw +sdram + +[options] +# sdram_init +sdram_init: mode prove +sdram_init: depth 25 +# sdram_refresh +sdram_refresh: mode prove +sdram_refresh: depth 25 +# sdram_rw +sdram_rw: mode prove +sdram_rw: depth 25 +# sdram +sdram: mode prove +sdram: depth 25 + +[engines] +sdram_init: smtbmc +sdram_refresh: smtbmc +sdram_rw: smtbmc +sdram: smtbmc + +[script] +# sdram_init +sdram_init: read_verilog -DF_INIT_FSM -formal sdram_nes.v +sdram_init: prep -top sdram_init_fsm +# sdram_refresh +sdram_refresh: read_verilog -DF_REFRESH_FSM -formal sdram_nes.v +sdram_refresh: prep -top sdram_refresh_fsm +# sdram_rw +sdram_rw: read_verilog -DF_RW_FSM -formal sdram_nes.v +sdram_rw: prep -top sdram_rw_fsm +# sdram +sdram: read_verilog -DF_SDRAM -formal sdram_nes.v +sdram: prep -top sdram_nes + +[files] +sdram_nes.v diff --git a/src/sdram_nes.v b/src/sdram_nes.v index 2df1e81..17ca292 100644 --- a/src/sdram_nes.v +++ b/src/sdram_nes.v @@ -1,5 +1,5 @@ // Double-channel CL2 SDRAM controller for NES -// nand2mario 2024.3 +// nand2mario 2024.3 | @fjpolo 2024.07 // // clk_# CPU/PPU RISC-V clkref // 0 RAS1 1 @@ -14,64 +14,423 @@ // // For both Nano 20K (32-bit total 8MB) and Primer 25K (16-bit total 32MB) +`ifndef FORMAL import configPackage::*; +`else + localparam SDRAM_DATA_WIDTH = 16; + localparam SDRAM_ROW_WIDTH = 13; + localparam SDRAM_COL_WIDTH = 9; + localparam SDRAM_BANK_WIDTH = 2; +`endif + +module sdram_init_fsm ( + input wire clk, + input wire resetn, + input wire start, + output reg busy, + output reg [3:0] cmd, + output reg [SDRAM_ROW_WIDTH-1:0] a, + output reg [1:0] SDRAM_BA, + output reg init_done +); + +localparam [4:0] T_MRD = 5'd2; // Mode Register Set delay +localparam [4:0] T_RP = 5'd2; // Precharge delay +localparam [4:0] T_RC = 5'd6; // Refresh cycle time + +localparam CMD_NOP = 4'b1111; +localparam CMD_SetModeReg = 4'b0000; +localparam CMD_BankActivate = 4'b0011; +localparam CMD_AutoRefresh = 4'b0001; +localparam CMD_PreCharge = 4'b0010; + +reg [15:0] cycle; +reg [10:0] MODE_REG; + +initial cycle = 0; +initial cmd = CMD_NOP; + +always @(posedge clk) begin + if (~resetn) begin + busy <= 1'b1; + cmd <= CMD_NOP; + cycle <= 0; + init_done <= 1'b0; + end else if (start) begin + if(cycle == T_RP + T_RC + T_RC + T_MRD) begin + busy <= 1'b0; + init_done <= 1'b1; + end else begin + busy <= 1'b1; + init_done <= 1'b0; + end + if (cycle == 0) begin + // Precharge all + cmd <= CMD_PreCharge; + a[10] <= 1'b1; + SDRAM_BA <= 0; + cycle <= cycle + 1; + end else if (cycle == T_RP) begin + // First AutoRefresh + cmd <= CMD_AutoRefresh; + cycle <= cycle + 1; + end else if (cycle == T_RP + T_RC) begin + // Second AutoRefresh + cmd <= CMD_AutoRefresh; + cycle <= cycle + 1; + end else if (cycle == T_RP + T_RC + T_RC) begin + // Set Mode Register + cmd <= CMD_SetModeReg; + a[10:0] <= MODE_REG; + SDRAM_BA <= 0; + cycle <= cycle + 1; + end else if (cycle == T_RP + T_RC + T_RC + T_MRD) begin + // Initialization done + cmd <= CMD_NOP; + end else begin + cycle <= cycle + 1; + end + end +end + +// +// Formal Methods +// +`ifdef FORMAL + + `ifdef F_SDRAM_INIT_FSM + `define ASSUME assume + `else + `define ASSUME assert + `endif + + // f_past_valid + reg f_past_valid; + initial f_past_valid = 1'b0; + always @(posedge clk) + f_past_valid <= 1'b1; + + // Initialization sequence + // After reset (resetn), busy should be high until initialization is complete (init_done high). + always @(posedge clk) begin + if((f_past_valid)&&(~$past(resetn))) begin + assert((busy)&&(~init_done)); + end + end + + always @(*) + if((!f_past_valid)||~(resetn)) begin + assume(cmd == CMD_NOP); + assume(~busy); + end + + // cycle + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) begin + assert(cycle <= (T_RP + T_RC + T_RC + T_MRD)); + end + end + + // + // Contract + // + wire [15:0] f_cycle; + + always @(*) + assume(f_cycle == cycle); + + always @(posedge clk) + if((f_past_valid)&&(~$past(resetn))) + assume($fell(start)); + + initial assert(cmd == CMD_NOP); + + // After start signal is asserted, the module should execute the precharge (CMD_PreCharge), + // followed by two auto-refresh cycles (CMD_AutoRefresh), then set the mode register (CMD_SetModeReg), and finally indicate init_done + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) begin + if($past(start)) + if(($past(f_cycle == 0))&&($past(start))) + assert(cmd == CMD_PreCharge); + else + if(($past(cycle) == (T_RP))) + assert((cmd == CMD_AutoRefresh)&&(busy)&&(~init_done)); + if(($past(cycle) == (T_RP + T_RC))&&($past(cmd) == CMD_AutoRefresh)) + assert((cmd == CMD_AutoRefresh)&&(busy)&&(~init_done)); + if(($past(cycle) == (T_RP + T_RC + T_RC))&&($past(cmd) == CMD_AutoRefresh)&&(cycle == (T_RP + T_RC + T_RC + 1))) + assert((cmd == CMD_SetModeReg)&&(busy)&&(~init_done)); + if(($past(cycle) == (T_RP + T_RC + T_RC + T_MRD))&&($past(cmd) == CMD_SetModeReg)&&(cycle == (T_RP + T_RC + T_RC + 1))) + assert((cmd == CMD_NOP)&&(~busy)&&(init_done)); + end + end + +`endif // FORMAL + +endmodule + +module sdram_refresh_fsm ( + input wire clk, + input wire resetn, + input wire start, + output reg busy, + output reg [3:0] cmd +); + +localparam CMD_NOP = 4'b1111; +localparam CMD_AutoRefresh = 4'b0001; +localparam REFRSH_CYCLES = 9'd501; + +reg [8:0] refresh_cnt; + +initial refresh_cnt = 0; + +always @(posedge clk) begin + if (~resetn) begin + busy <= 1'b0; + refresh_cnt <= 0; + cmd <= CMD_NOP; + end else if (start && (refresh_cnt == REFRSH_CYCLES)) begin + busy <= 1'b1; + cmd <= CMD_AutoRefresh; + refresh_cnt <= 0; + end else if (busy) begin + busy <= 1'b0; + cmd <= CMD_NOP; + end else begin + refresh_cnt <= refresh_cnt + 1; + end +end + +// +// Formal Methods +// +`ifdef FORMAL + + `ifdef F_SDRAM_REFRESH_FSM + `define ASSUME assume + `else + `define ASSUME assert + `endif + + // f_past_valid + reg f_past_valid; + initial f_past_valid = 1'b0; + always @(posedge clk) + f_past_valid <= 1'b1; + + // Reset + // After reset (resetn), ensure that busy is low + always @(posedge clk) begin + if((f_past_valid)&&(~$past(resetn))) + assert(~busy); + end + + // Start + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + assume($fell(start)); + end + // After asserting start, check that busy becomes high exactly when refresh_cnt reaches REFRSH_CYCLES + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + if($past(refresh_cnt == REFRSH_CYCLES)) + assert(busy); + else if(refresh_cnt < REFRSH_CYCLES) + assert(~busy); + end + + + // Cycle Counting + // Ensure that refresh_cnt increments correctly with each clock cycle when not in the busy state + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + assert(refresh_cnt <= REFRSH_CYCLES); + end + + // + // Contract + // + + // State Transitions + // Verify that cmd transitions correctly between CMD_NOP and CMD_AutoRefresh + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + if($past(refresh_cnt) == REFRSH_CYCLES) + assert(cmd == CMD_AutoRefresh); + else if(($past(refresh_cnt) == REFRSH_CYCLES)&&($past(cmd) == CMD_AutoRefresh)) + assert(cmd == CMD_NOP); + end + +`endif // FORMAL + +endmodule + +module sdram_rw_fsm ( + input wire clk, + input wire resetn, + input wire start, + input wire we, + input wire [21:0] addr, + input wire [15:0] din, + output reg [15:0] dout, + output reg busy, + output reg [3:0] cmd, + output reg [SDRAM_ROW_WIDTH-1:0] a, + output reg [1:0] SDRAM_BA, + output reg dq_oen, + output reg [1:0] SDRAM_DQM +); + +localparam CMD_NOP = 4'b1111; +localparam CMD_BankActivate = 4'b0011; +localparam CMD_Write = 4'b0100; +localparam CMD_Read = 4'b0101; + +always @(posedge clk) begin + if (~resetn) begin + busy <= 1'b0; + cmd <= CMD_NOP; + dq_oen <= 1'b1; + end else if (start) begin + busy <= 1'b1; + cmd <= CMD_BankActivate; + SDRAM_BA <= addr[21:20]; + a <= addr[19:0]; + end else if (busy) begin + if (we) begin + cmd <= CMD_Write; + dq_oen <= 1'b0; + dout <= din; + end else begin + cmd <= CMD_Read; + dq_oen <= 1'b1; + end + busy <= 1'b0; + end else begin + cmd <= CMD_NOP; + end +end + +// +// Formal Methods +// +`ifdef FORMAL + + `ifdef F_SDRAM_RW_FSM + `define ASSUME assume + `else + `define ASSUME assert + `endif + + // f_past_valid + reg f_past_valid; + initial f_past_valid = 1'b0; + always @(posedge clk) + f_past_valid <= 1'b1; + + always @(posedge clk) begin + if((f_past_valid)&&(~$past(resetn))) + assume($fell(start)); + end + + // State Transitions: + // After reset (resetn), ensure that busy is low, cmd is CMD_NOP, dq_oen is high, and dout is not driven (dout value is irrelevant) + always @(posedge clk) begin + if((f_past_valid)&&(~$past(resetn))) + assert((~busy)&&(cmd == CMD_NOP)); + end + // After asserting start, check that busy becomes high, cmd transitions to CMD_BankActivate, and appropriate values are assigned to SDRAM_BA and a. + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + if(($past(start))&&(~busy)) begin + assume($fell(start)); + assert((busy)&&(cmd == CMD_BankActivate)); + assert(SDRAM_BA == $past(addr[21:20])); + assert(a == $past(addr[19:0])); + end + end + + // + // Contract + // + + // Read + // Verify that when we is not asserted (read operation) during the busy state, cmd transitions to CMD_Read and dq_oen remains enabled + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + if((~$past(start))&&($past(busy))&&($past(~we))) begin + assert(cmd == CMD_Read); + assert(dq_oen); + end + end + // Write + // Verify that when we is asserted during the busy state, cmd transitions to CMD_Write, dq_oen is low, and dout reflects the value of din. + always @(posedge clk) begin + if((f_past_valid)&&($past(resetn))) + if((~$past(start))&&($past(busy))&&($past(we))) begin + assert(cmd == CMD_Write); + assert(~dq_oen); + assert(dout == $past(din)); + end + end + +`endif // FORMAL + +endmodule module sdram_nes #( - // Clock frequency, max 66.7Mhz with current set of T_xx/CAS parameters. parameter FREQ = 64_800_000, - - parameter [4:0] CAS = 4'd2, // 2/3 cycles, set in mode register - parameter [4:0] T_WR = 4'd2, // 2 cycles, write recovery - parameter [4:0] T_MRD= 4'd2, // 2 cycles, mode register set - parameter [4:0] T_RP = 4'd2, // 15ns, precharge to active - parameter [4:0] T_RCD= 4'd2, // 15ns, active to r/w - parameter [4:0] T_RC = 4'd6 // 63ns, ref/active to ref/active + parameter [4:0] CAS = 4'd2, // 2/3 cycles, set in mode register + parameter [4:0] T_WR = 4'd2, // 2 cycles, write recovery + parameter [4:0] T_MRD= 4'd2, // 2 cycles, mode register set + parameter [4:0] T_RP = 4'd2, // 15ns, precharge to active + parameter [4:0] T_RCD= 4'd2, // 15ns, active to r/w + parameter [4:0] T_RC = 4'd6 // 63ns, ref/active to ref/active ) ( - inout reg [SDRAM_DATA_WIDTH-1:0] SDRAM_DQ, // 16 bit bidirectional data bus - output [SDRAM_ROW_WIDTH-1:0] SDRAM_A, // 13 bit multiplexed address bus + inout reg [SDRAM_DATA_WIDTH-1:0] SDRAM_DQ, // 16 bit bidirectional data bus + output [SDRAM_ROW_WIDTH-1:0] SDRAM_A, // 13 bit multiplexed address bus output reg [SDRAM_DATA_WIDTH/8-1:0] SDRAM_DQM, // two byte masks - output reg [1:0] SDRAM_BA, // two banks - output SDRAM_nCS, // a single chip select - output SDRAM_nWE, // write enable - output SDRAM_nRAS, // row address select - output SDRAM_nCAS, // columns address select + output reg [1:0] SDRAM_BA, // two banks + output SDRAM_nCS, // a single chip select + output SDRAM_nWE, // write enable + output SDRAM_nRAS, // row address select + output SDRAM_nCAS, // columns address select output SDRAM_CKE, - - // cpu/chipset interface - input clk, // sdram clock + + // cpu/chipset interface + input clk, // sdram clock input resetn, input clkref, output reg busy, - input [21:0] addrA, // 4MB, bank 0/1 - input weA, // ppu requests write - input [7:0] dinA, // data input from cpu - input oeA, // ppu requests data - output reg [7:0] doutA, // data output to cpu + input [21:0] addrA, // 4MB, bank 0/1 + input weA, // ppu requests write + input [7:0] dinA, // data input from cpu + input oeA, // ppu requests data + output reg [7:0] doutA, // data output to cpu - input [21:0] addrB, // 4MB, bank 0/1 - input weB, // cpu requests write - input [7:0] dinB, // data input from ppu - input oeB, // cpu requests data - output reg [7:0] doutB, // data output to ppu + input [21:0] addrB, // 4MB, bank 0/1 + input weB, // cpu requests write + input [7:0] dinB, // data input from ppu + input oeB, // cpu requests data + output reg [7:0] doutB, // data output to ppu // RISC-V softcore - input [20:1] rv_addr, // 2MB RV memory space, bank 2 - input [15:0] rv_din, // 16-bit accesses + input [20:1] rv_addr, // 2MB RV memory space, bank 2 + input [15:0] rv_din, // 16-bit accesses input [1:0] rv_ds, output reg [15:0] rv_dout, input rv_req, - output reg rv_req_ack, // ready for new requests. read data available on NEXT mclk + output reg rv_req_ack, // ready for new requests. read data available on NEXT mclk input rv_we ); - localparam DQM_SIZE = SDRAM_DATA_WIDTH / 8; // Tri-state DQ input/output -reg dq_oen; // 0 means output +reg dq_oen; reg [SDRAM_DATA_WIDTH-1:0] dq_out; assign SDRAM_DQ = dq_oen ? {SDRAM_DATA_WIDTH{1'bz}} : dq_out; -wire [SDRAM_DATA_WIDTH-1:0] dq_in = SDRAM_DQ; // DQ input +wire [SDRAM_DATA_WIDTH-1:0] dq_in = SDRAM_DQ; reg [3:0] cmd; reg [SDRAM_ROW_WIDTH-1:0] a; assign {SDRAM_nCS, SDRAM_nRAS, SDRAM_nCAS, SDRAM_nWE} = cmd; @@ -88,43 +447,32 @@ localparam CMD_Read=4'b0101; localparam CMD_AutoRefresh=4'b0001; localparam CMD_PreCharge=4'b0010; -localparam [2:0] BURST_LEN = 3'b0; // burst length 1 -localparam BURST_MODE = 1'b0; // sequential +localparam [2:0] BURST_LEN = 3'b0; +localparam BURST_MODE = 1'b0; localparam [10:0] MODE_REG = {4'b0, CAS[2:0], BURST_MODE, BURST_LEN}; -// 64ms/8192 rows = 7.8us -> 500 cycles@64.8MHz -localparam RFRSH_CYCLES = 9'd501; +localparam REFRSH_CYCLES = 9'd501; + +// Initialization FSM states +localparam INIT_IDLE = 3'd0, INIT_PRECHARGE = 3'd1, INIT_REFRESH1 = 3'd2, INIT_REFRESH2 = 3'd3, INIT_MODE_SET = 3'd4, INIT_DONE = 3'd5; +reg [2:0] init_state; +reg [8:0] cycle; // Increase the bit width to handle larger values + +reg cfg_now; // Configuration now signal -// state -reg [16:0] cycle; // one hot encoded -reg normal, setup; -reg cfg_now; // pulse for configuration +// Request FSM states +localparam REQ_IDLE = 3'd0, REQ_ACTIVATE = 3'd1, REQ_READ_WRITE = 3'd2, REQ_WAIT = 3'd3; +reg [2:0] req_state_cpu, req_state_rv; -// requests +// Request Latches and Flags reg [21:0] addr_latch[0:1]; reg [15:0] din_latch[0:1]; reg [2:0] oe_latch; reg [2:0] we_latch; reg [1:0] ds[0:1]; - -localparam PORT_NONE = 2'd0; - -localparam PORT_A = 2'd1; // PPU -localparam PORT_B = 2'd2; // CPU - -localparam PORT_RV = 2'd1; - -reg [1:0] port[0:1]; -reg [1:0] next_port[0:1]; -reg [21:0] next_addr[0:1]; -reg [15:0] next_din[0:1]; -reg [1:0] next_ds[0:1]; -reg [2:0] next_we; -reg [2:0] next_oe; - +reg [1:0] port[0:1]; reg oeA_d, oeB_d, weA_d, weB_d; wire reqA = (~oeA_d & oeA) || (~weA_d & weA); wire reqB = (~oeB_d & oeB) || (~weB_d & weB); - reg clkref_r; always @(posedge clk) clkref_r <= clkref; @@ -132,258 +480,148 @@ reg [8:0] refresh_cnt; reg need_refresh = 1'b0; always @(posedge clk) begin - if (refresh_cnt == 0) - need_refresh <= 0; - else if (refresh_cnt == RFRSH_CYCLES) - need_refresh <= 1; + if (refresh_cnt == 0) + need_refresh <= 0; + else if (refresh_cnt == REFRSH_CYCLES) + need_refresh <= 1; end -// CPU/PPU: bank 0/1 -always @(*) begin - next_port[0] = PORT_NONE; - next_addr[0] = 0; - next_we[0] = 0; - next_oe[0] = 0; - next_ds[0] = 0; - next_din[0] = 0; - if (reqB) begin - next_port[0] = PORT_B; - next_addr[0] = addrB; - next_din[0] = {dinB, dinB}; - next_ds[0] = {addrB[0], ~addrB[0]}; - next_we[0] = weB; - next_oe[0] = oeB; - end else if (reqA) begin - next_port[0] = PORT_A; - next_addr[0] = addrA; - next_din[0] = {dinA, dinA}; - next_ds[0] = {addrA[0], ~addrA[0]}; - next_we[0] = weA; - next_oe[0] = oeA; - end +// Generate cfg_now signal: Set cfg_now high for one cycle after reset +always @(posedge clk or negedge resetn) begin + if (~resetn) begin + cfg_now <= 1'b1; + end else begin + cfg_now <= 1'b0; + end end -// RV: bank 2 -always @* begin - next_port[1] = PORT_NONE; - next_addr[1] = 0; - next_we[1] = 0; - next_oe[1] = 0; - next_ds[1] = 0; - next_din[1] = 0; - if (rv_req ^ rv_req_ack) begin - next_port[1] = PORT_RV; - next_addr[1] = {rv_addr, 1'b0}; - next_we[1] = rv_we; - next_oe[1] = ~rv_we; - next_din[1] = rv_din; - next_ds[1] = rv_ds; - end -end +// Initialization and CPU/PPU Request FSM +reg fsm_initialized; -// -// SDRAM state machine -// -always @(posedge clk) begin +initial fsm_initialized = 1'b0; + +always @(posedge clk or negedge resetn) begin if (~resetn) begin - busy <= 1'b1; - dq_oen <= 1; - SDRAM_DQM <= {DQM_SIZE{1'b1}}; - normal <= 0; - setup <= 0; - end else begin - // defaults - dq_oen <= 1'b1; - SDRAM_DQM <= {DQM_SIZE{1'b1}}; - cmd <= CMD_NOP; - - // wait 200 us on power-on - if (~normal && ~setup && cfg_now) begin // wait 200 us on power-on - setup <= 1; - cycle <= 1; - end - - // setup process - if (setup) begin - cycle <= {cycle[15:0], 1'b0}; // cycle 0-16 for setup - // configuration sequence - if (cycle[0]) begin - // precharge all + fsm_initialized <= 1'b0; + init_state <= INIT_IDLE; + req_state_cpu <= REQ_IDLE; + cmd <= CMD_NOP; + cycle <= 1; + SDRAM_DQM <= {DQM_SIZE{1'b1}}; // Initialize SDRAM_DQM + // Initialization FSM + end else if(!fsm_initialized) begin + cycle <= cycle + 1; + case (init_state) + INIT_IDLE: begin + if (cfg_now) begin + init_state <= INIT_PRECHARGE; + cycle <= 1; + end + end + INIT_PRECHARGE: begin cmd <= CMD_PreCharge; a[10] <= 1'b1; SDRAM_BA <= 0; + init_state <= INIT_REFRESH1; + cycle <= 1; // Reset cycle + SDRAM_DQM <= {DQM_SIZE{1'b1}}; // Set DQM to high impedance end - if (cycle[T_RP]) begin // 2 - // 1st AutoRefresh - cmd <= CMD_AutoRefresh; - end - if (cycle[T_RP+T_RC]) begin // 8 - // 2nd AutoRefresh - cmd <= CMD_AutoRefresh; - end - if (cycle[T_RP+T_RC+T_RC]) begin // 14 - // set register - cmd <= CMD_SetModeReg; - a[10:0] <= MODE_REG; - SDRAM_BA <= 0; + INIT_REFRESH1: begin + if (cycle == T_RP) begin + cmd <= CMD_AutoRefresh; + init_state <= INIT_REFRESH2; + cycle <= 1; // Reset cycle + end end - if (cycle[T_RP+T_RC+T_RC+T_MRD]) begin // 16 - setup <= 0; - normal <= 1; - cycle <= 1; - busy <= 1'b0; // init&config is done + INIT_REFRESH2: begin + if (cycle == T_RC) begin + cmd <= CMD_AutoRefresh; + init_state <= INIT_MODE_SET; + cycle <= 1; // Reset cycle + end end - end - if (normal) begin - if (clkref & ~clkref_r) // go to cycle 5 after clkref posedge - cycle[5:0] <= 6'b10_0000; - else - cycle[5:0] <= {cycle[4:0], cycle[5]}; - refresh_cnt <= refresh_cnt + 1'd1; - - // RAS - // CPU, PPU - if (cycle[0]) begin - port[0] <= next_port[0]; - oeA_d <= oeA_d & oeA; weA_d <= weA_d & weA; - oeB_d <= oeB_d & oeB; weB_d <= weB_d & weB; - if (next_port[0] == PORT_A) begin - oeA_d <= oeA; weA_d <= weA; + INIT_MODE_SET: begin + if (cycle == T_RC) begin + cmd <= CMD_SetModeReg; + a[10:0] <= MODE_REG; + SDRAM_BA <= 0; + init_state <= INIT_DONE; + cycle <= 1; // Reset cycle end - if (next_port[0] == PORT_B) begin - oeB_d <= oeB; weB_d <= weB; + end + INIT_DONE: begin + if (cycle == T_MRD) begin + fsm_initialized <= 1'b1; + busy <= 1'b0; + init_state <= INIT_IDLE; end - { we_latch[0], oe_latch[0] } <= { next_we[0], next_oe[0] }; - addr_latch[0] <= next_addr[0]; - SDRAM_BA <= next_addr[0][21]; // bank 0 or 1 - din_latch[0] <= next_din[0]; - ds[0] <= next_ds[0]; - if (next_port[0] != PORT_NONE) cmd <= CMD_BankActivate; - a <= next_addr[0][20:10]; end - - // bank 1 - RV - if (cycle[2]) begin - port[1] <= next_port[1]; - { we_latch[1], oe_latch[1] } <= { next_we[1], next_oe[1] }; - addr_latch[1] <= next_addr[1]; - a <= next_addr[1][20:10]; - SDRAM_BA <= 2'd2; - din_latch[1] <= next_din[1]; - ds[1] <= next_ds[1]; - if (next_port[1] != PORT_NONE) begin - cmd <= CMD_BankActivate; - end else if (!we_latch[0] && !oe_latch[0] && !we_latch[1] && !oe_latch[1] && need_refresh) begin - refresh_cnt <= 0; - cmd <= CMD_AutoRefresh; + endcase + // CPU/PPU Request FSM + end else begin + cycle <= cycle + 1; + case (req_state_cpu) + REQ_IDLE: begin + if (reqA || reqB) begin + addr_latch[0] <= reqA ? addrA : addrB; + din_latch[0] <= reqA ? {dinA, dinA} : {dinB, dinB}; + ds[0] <= reqA ? {addrA[0], ~addrA[0]} : {addrB[0], ~addrB[0]}; + we_latch[0] <= reqA ? weA : weB; + oe_latch[0] <= reqA ? oeA : oeB; + SDRAM_BA <= addr_latch[0][21]; + req_state_cpu <= REQ_ACTIVATE; + cycle <= 1; + SDRAM_DQM <= {DQM_SIZE{1'b1}}; // Set DQM to high impedance end end - - // CAS - // CPU, PPU - if (cycle[1] && (oe_latch[0] || we_latch[0])) begin - cmd <= we_latch[0]?CMD_Write:CMD_Read; - SDRAM_BA <= addr_latch[0][21]; -`ifdef NANO - a <= addr_latch[0][9:2]; -`else - a <= addr_latch[0][9:1]; -`endif - a[10] <= 1'b1; // auto precharge - if (we_latch[0]) begin - dq_oen <= 0; -`ifdef NANO - SDRAM_DQM <= addr_latch[0][1] ? {~ds[0], 2'b11} : {2'b11, ~ds[0]}; - dq_out <= {din_latch[0], din_latch[0]}; -`else - SDRAM_DQM <= ~ds[0]; - dq_out <= din_latch[0]; -`endif - end else - SDRAM_DQM <= 0; + REQ_ACTIVATE: begin + cmd <= CMD_BankActivate; + a <= addr_latch[0]; + req_state_cpu <= REQ_READ_WRITE; + cycle <= 1; end - - // RV - if (cycle[4] && (oe_latch[1] || we_latch[1])) begin - cmd <= we_latch[1]?CMD_Write:CMD_Read; - SDRAM_BA <= 2'd2; -`ifdef NANO - a <= addr_latch[1][9:2]; -`else - a <= addr_latch[1][9:1]; -`endif - a[10] <= 1'b1;// auto precharge - if (we_latch[1]) begin - dq_oen <= 0; -`ifdef NANO - SDRAM_DQM <= addr_latch[1][1] ? {~ds[1], 2'b11} : {2'b11, ~ds[1]}; - dq_out <= {din_latch[1], din_latch[1]}; -`else - SDRAM_DQM <= ~ds[1]; - dq_out <= din_latch[1]; -`endif - end else - SDRAM_DQM <= 0; - rv_req_ack <= rv_req; // ack request + REQ_READ_WRITE: begin + if (cycle == T_RCD) begin + cmd <= we_latch[0] ? CMD_Write : CMD_Read; + dq_out <= we_latch[0] ? din_latch[0] : {8{1'bz}}; + dq_oen <= we_latch[0] ? 1'b0 : 1'b1; + doutA <= dq_in[7:0]; + doutB <= dq_in[7:0]; + req_state_cpu <= REQ_WAIT; + cycle <= 1; + end end - - // read - // CPU, PPU - if (cycle[4] && oe_latch[0]) begin - reg [7:0] dq_byte; -`ifdef NANO - case (addr_latch[0][1:0]) - 2'd0: dq_byte = dq_in[7:0]; - 2'd1: dq_byte = dq_in[15:8]; - 2'd2: dq_byte = dq_in[23:16]; - 2'd3: dq_byte = dq_in[31:24]; - endcase -`else - dq_byte = addr_latch[0][0] ? dq_in[15:8] : dq_in[7:0]; -`endif - - case (port[0]) - PORT_A: doutA <= dq_byte; - PORT_B: doutB <= dq_byte; - default: ; - endcase + REQ_WAIT: begin + if (cycle == T_WR) begin + req_state_cpu <= REQ_IDLE; + SDRAM_DQM <= {DQM_SIZE{1'b1}}; // Set DQM to high impedance + end end - - // RV - if (cycle[1] && oe_latch[1]) -`ifdef NANO - rv_dout <= addr_latch[1][1] ? dq_in[31:16] : dq_in[15:0]; -`else - rv_dout <= dq_in; -`endif - end + endcase end end // -// Generate cfg_now pulse after initialization delay (normally 200us) +// Formal Methods // -reg [14:0] rst_cnt; -reg rst_done, rst_done_p1, cfg_busy; - -always @(posedge clk) begin - if (~resetn) begin - rst_cnt <= 15'd0; - rst_done <= 1'b0; - cfg_busy <= 1'b1; - end else begin - rst_done_p1 <= rst_done; - cfg_now <= rst_done & ~rst_done_p1;// Rising Edge Detect +`ifdef FORMAL - if (rst_cnt != FREQ / 1000 * 200 / 1000) begin // count to 200 us - rst_cnt <= rst_cnt[14:0] + 15'd1; - rst_done <= 1'b0; - cfg_busy <= 1'b1; - end else begin - rst_done <= 1'b1; - cfg_busy <= 1'b0; - end - end -end + `ifdef F_SDRAM + `define ASSUME assume + `else + `define ASSUME assert + `endif + + // f_past_valid + reg f_past_valid; + initial f_past_valid = 1'b0; + always @(posedge clk) + f_past_valid <= 1'b1; + + // + // Contract + // + +`endif // FORMAL -endmodule \ No newline at end of file +endmodule