//////////////////////////////////////////////////////////////////////////////// // // Filename: wbsdram.v // // Project: ArrowZip, a demonstration of the Arrow MAX1000 FPGA board // // Purpose: Provide 32-bit wishbone access to the SDRAM memory on a MAX1000 // board. Specifically, on each access, the controller will // activate an appropriate bank of RAM (the SDRAM has four banks), and // then issue the read/write command. In the case of walking off the // bank, the controller will activate the next bank before you get to it. // Upon concluding any wishbone access, all banks will be precharged and // returned to idle. // // This particular implementation represents a second generation version // because my first version was too complex. To speed things up, this // version includes an extra wait state where the wishbone inputs are // clocked into a flip flop before any action is taken on them. // // Creator: Dan Gisselquist, Ph.D. // Gisselquist Technology, LLC // //////////////////////////////////////////////////////////////////////////////// // // Copyright (C) 2015-2019, Gisselquist Technology, LLC // // This program is free software (firmware): you can redistribute it and/or // modify it under the terms of the GNU General Public License as published // by the Free Software Foundation, either version 3 of the License, or (at // your option) any later version. // // This program is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or // FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License // for more details. // // You should have received a copy of the GNU General Public License along // with this program. (It's in the $(ROOT)/doc directory. Run make with no // target there if the PDF file isn't present.) If not, see // for a copy. // // License: GPL, v3, as defined and found on www.gnu.org, // http://www.gnu.org/licenses/gpl.html // // //////////////////////////////////////////////////////////////////////////////// // // `default_nettype none // `define DMOD_GETINPUT 1'b0 `define DMOD_PUTOUTPUT 1'b1 `define RAM_OPERATIONAL 2'b00 `define RAM_POWER_UP 2'b01 `define RAM_SET_MODE 2'b10 `define RAM_INITIAL_REFRESH 2'b11 // module wbsdram(i_clk, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, o_wb_ack, o_wb_stall, o_wb_data, o_ram_cs_n, o_ram_cke, o_ram_ras_n, o_ram_cas_n, o_ram_we_n, o_ram_bs, o_ram_addr, o_ram_dmod, i_ram_data, o_ram_data, o_ram_dqm, o_debug); parameter RDLY = 6; localparam NCA=10, NRA=13, AW=(NCA+NRA+2)-1, DW=32; localparam [NCA-2:0] COL_THRESHOLD = -16; input wire i_clk; // Wishbone // inputs input wire i_wb_cyc, i_wb_stb, i_wb_we; input wire [(AW-1):0] i_wb_addr; input wire [(DW-1):0] i_wb_data; input wire [(DW/8-1):0] i_wb_sel; // outputs output wire o_wb_ack; output reg o_wb_stall; output wire [31:0] o_wb_data; // SDRAM control output wire o_ram_cke; output reg o_ram_cs_n, o_ram_ras_n, o_ram_cas_n, o_ram_we_n; output reg [1:0] o_ram_bs; output reg [12:0] o_ram_addr; output reg o_ram_dmod; input [15:0] i_ram_data; output reg [15:0] o_ram_data; output reg [1:0] o_ram_dqm; output wire [(DW-1):0] o_debug; // Calculate some metrics // // First, do we *need* a refresh now --- i.e., must we break out of // whatever we are doing to issue a refresh command? // // The step size here must be such that 8192 charges may be done in // 64 ms. Thus for a clock of: // ClkRate(MHz) (64ms/1000(ms/s)*ClkRate)/8192 // 100 MHz 781 // 96 MHz 750 // 92 MHz 718 // 88 MHz 687 // 84 MHz 656 // 80 MHz 625 // // However, since we do two refresh cycles everytime we need a refresh, // this standard is close to overkill--but we'll use it anyway. At // some later time we should address this, once we are entirely // convinced that the memory is otherwise working without failure. Of // course, at that time, it may no longer be a priority ... // reg need_refresh; reg [9:0] refresh_clk; wire refresh_cmd; assign refresh_cmd = (!o_ram_cs_n)&&(!o_ram_ras_n)&&(!o_ram_cas_n)&&(o_ram_we_n); initial refresh_clk = 0; always @(posedge i_clk) begin if (refresh_cmd) refresh_clk <= 10'd703; // Make suitable for 90 MHz clk else if (|refresh_clk) refresh_clk <= refresh_clk - 10'h1; end initial need_refresh = 1'b0; always @(posedge i_clk) need_refresh <= (refresh_clk == 10'h00)&&(!refresh_cmd); reg in_refresh; reg [2:0] in_refresh_clk; initial in_refresh_clk = 3'h0; always @(posedge i_clk) if (refresh_cmd) in_refresh_clk <= 3'h6; else if (|in_refresh_clk) in_refresh_clk <= in_refresh_clk - 3'h1; initial in_refresh = 0; always @(posedge i_clk) in_refresh <= (in_refresh_clk != 3'h0)||(refresh_cmd); `ifdef FORMAL always @(posedge i_clk) if (in_refresh) assert((refresh_cmd)||($past(in_refresh_clk) <= 3'h6)); always @(posedge i_clk) if (in_refresh) assert(refresh_clk==10'd619+{{(7){1'b0}},in_refresh_clk}); `endif reg [2:0] bank_active [0:3]; reg [(RDLY-1):0] r_barrell_ack; reg r_pending; reg r_we; reg [(AW-1):0] r_addr; reg [31:0] r_data; reg [3:0] r_sel; reg [(AW-NCA-2):0] bank_row [0:3]; // // Second, do we *need* a precharge now --- must be break out of // whatever we are doing to issue a precharge command? // // Keep in mind, the number of clocks to wait has to be reduced by // the amount of time it may take us to go into a precharge state. // You may also notice that the precharge requirement is tighter // than this one, so ... perhaps this isn't as required? // reg [2:0] clocks_til_idle; reg [1:0] m_state; wire bus_cyc; assign bus_cyc = ((i_wb_cyc)&&(i_wb_stb)&&(!o_wb_stall)); reg nxt_dmod; // Pre-process pending operations wire pending; initial r_pending = 1'b0; reg [(AW-1):0] fwd_addr; initial r_addr = 0; initial fwd_addr = { {(AW-(NCA)){1'b0}}, 1'b1, {(NCA-1){1'b0}} }; always @(posedge i_clk) begin fwd_addr[NCA-2:0] <= 0; if (bus_cyc) begin r_pending <= 1'b1; r_we <= i_wb_we; r_addr <= i_wb_addr; r_data <= i_wb_data; r_sel <= i_wb_sel; fwd_addr[AW-1:NCA-1]<=i_wb_addr[(AW-1):(NCA-1)] + 1'b1; end else if ((!o_ram_cs_n)&&(o_ram_ras_n)&&(!o_ram_cas_n)) r_pending <= 1'b0; else if (!i_wb_cyc) r_pending <= 1'b0; end `ifdef FORMAL always @(*) assert(fwd_addr[AW-1:NCA-1] == r_addr[(AW-1):(NCA-1)] + 1'b1); always @(*) assert(fwd_addr[NCA-3:0] == 0); `endif wire [1:0] wb_bs, r_bs, fwd_bs; // Bank select assign wb_bs = i_wb_addr[NCA:NCA-1]; assign r_bs = r_addr[NCA:NCA-1]; assign fwd_bs = fwd_addr[NCA:NCA-1]; wire [NRA-1:0] wb_row, r_row, fwd_row; assign wb_row = i_wb_addr[AW-1:NCA+1]; assign r_row = r_addr[AW-1:NCA+1]; assign fwd_row = fwd_addr[AW-1:NCA+1]; reg r_bank_valid; initial r_bank_valid = 1'b0; always @(posedge i_clk) if (bus_cyc) r_bank_valid <=((bank_active[wb_bs][2]) &&(bank_row[wb_bs] == wb_row)); else r_bank_valid <= ((bank_active[r_bs][2]) &&(bank_row[r_bs] == r_row)); reg fwd_bank_valid; initial fwd_bank_valid = 0; always @(posedge i_clk) fwd_bank_valid <= ((bank_active[fwd_bs][2]) &&(bank_row[fwd_bs] == fwd_row)); assign pending = (r_pending)&&(o_wb_stall); // // // Maintenance mode (i.e. startup) wires and logic reg maintenance_mode; reg m_ram_cs_n, m_ram_ras_n, m_ram_cas_n, m_ram_we_n, m_ram_dmod; reg [(NRA-1):0] m_ram_addr; // // // // Address MAP: // 22-bits bits in, 23-bits out // // 22 1111 1111 1100 0000 0000 // 10 9876 5432 1098 7654 3210 // rr rrrr rrrr rrBB cccc cccc 0 // 8765 4321 0 // initial r_barrell_ack = 0; initial clocks_til_idle = 3'h0; initial o_wb_stall = 1'b1; initial o_ram_dmod = `DMOD_GETINPUT; initial nxt_dmod = `DMOD_GETINPUT; initial o_ram_cs_n = 1'b0; initial o_ram_ras_n = 1'b1; initial o_ram_cas_n = 1'b1; initial o_ram_we_n = 1'b1; initial o_ram_dqm = 2'b11; assign o_ram_cke = 1'b1; initial bank_active[0] = 3'b000; initial bank_active[1] = 3'b000; initial bank_active[2] = 3'b000; initial bank_active[3] = 3'b000; always @(posedge i_clk) if (maintenance_mode) begin bank_active[0] <= 0; bank_active[1] <= 0; bank_active[2] <= 0; bank_active[3] <= 0; r_barrell_ack[(RDLY-1):0] <= 0; o_wb_stall <= 1'b1; // o_ram_cs_n <= m_ram_cs_n; o_ram_ras_n <= m_ram_ras_n; o_ram_cas_n <= m_ram_cas_n; o_ram_we_n <= m_ram_we_n; o_ram_dmod <= m_ram_dmod; o_ram_addr <= m_ram_addr; o_ram_bs <= 2'b00; nxt_dmod <= `DMOD_GETINPUT; end else begin o_wb_stall <= (r_pending)||(bus_cyc); if (!i_wb_cyc) r_barrell_ack <= 0; else r_barrell_ack <= r_barrell_ack >> 1; nxt_dmod <= `DMOD_GETINPUT; o_ram_dmod <= nxt_dmod; // // We assume that, whatever state the bank is in, that it // continues in that state and set up a series of shift // registers to contain that information. If it will not // continue in that state, all that therefore needs to be // done is to set bank_active[?][2] below. // bank_active[0] <= { bank_active[0][2], bank_active[0][2:1] }; bank_active[1] <= { bank_active[1][2], bank_active[1][2:1] }; bank_active[2] <= { bank_active[2][2], bank_active[2][2:1] }; bank_active[3] <= { bank_active[3][2], bank_active[3][2:1] }; // o_ram_cs_n <= (!i_wb_cyc); // o_ram_cke <= 1'b1; if (|clocks_til_idle[2:0]) clocks_til_idle[2:0] <= clocks_til_idle[2:0] - 3'h1; // Default command is a // NOOP if (i_wb_cyc) // Device deselect if (!i_wb_cyc) // o_ram_cs_n <= (!i_wb_cyc) above, NOOP o_ram_ras_n <= 1'b1; o_ram_cas_n <= 1'b1; o_ram_we_n <= 1'b1; // o_ram_data <= r_data[15:0]; if (nxt_dmod) ; else if ((!i_wb_cyc)||(need_refresh)) begin // Issue a precharge all command (if any banks are open), // otherwise an autorefresh command if ((bank_active[0][2:1]==2'b10) ||(bank_active[1][2:1]==2'b10) ||(bank_active[2][2:1]==2'b10) ||(bank_active[3][2:1]==2'b10) ||(|clocks_til_idle[2:0])) begin // Do nothing this clock // Can't precharge a bank immediately after // activating it end else if (bank_active[0][2] ||(bank_active[1][2]) ||(bank_active[2][2]) ||(bank_active[3][2])) begin // Close all active banks o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b0; o_ram_cas_n <= 1'b1; o_ram_we_n <= 1'b0; o_ram_addr[10] <= 1'b1; bank_active[0][2] <= 1'b0; bank_active[1][2] <= 1'b0; bank_active[2][2] <= 1'b0; bank_active[3][2] <= 1'b0; end else if ((|bank_active[0]) ||(|bank_active[1]) ||(|bank_active[2]) ||(|bank_active[3])) // Can't precharge yet, the bus is still busy begin end else if ((!in_refresh)&&((refresh_clk[9:8]==2'b00)||(need_refresh))) begin // Send autorefresh command o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b0; o_ram_cas_n <= 1'b0; o_ram_we_n <= 1'b1; end // Else just send NOOP's, the default command end else if (in_refresh) begin // NOOPS only here, until we are out of refresh end else if ((pending)&&(!r_bank_valid)&&(bank_active[r_bs]==3'h0)) begin // Need to activate the requested bank o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b0; o_ram_cas_n <= 1'b1; o_ram_we_n <= 1'b1; o_ram_addr <= r_row; o_ram_bs <= r_bs; // clocks_til_idle[2:0] <= 1; bank_active[r_bs][2] <= 1'b1; bank_row[r_bs] <= r_row; // end else if ((pending)&&(!r_bank_valid) &&(bank_active[r_bs]==3'b111)) begin // Need to close an active bank o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b0; o_ram_cas_n <= 1'b1; o_ram_we_n <= 1'b0; // o_ram_addr <= r_addr[(AW-1):(NCA+2)]; o_ram_addr[10]<= 1'b0; o_ram_bs <= r_bs; // clocks_til_idle[2:0] <= 1; bank_active[r_bs][2] <= 1'b0; // bank_row[r_bs] <= r_row; end else if ((pending)&&(!r_we) &&(bank_active[r_bs][2]) &&(r_bank_valid) &&(clocks_til_idle[2:0] < 4)) begin // Issue the read command o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b1; o_ram_cas_n <= 1'b0; o_ram_we_n <= 1'b1; o_ram_addr <= { 4'h0, r_addr[NCA-2:0], 1'b0 }; o_ram_bs <= r_bs; clocks_til_idle[2:0] <= 4; o_wb_stall <= 1'b0; r_barrell_ack[(RDLY-1)] <= 1'b1; end else if ((pending)&&(r_we) &&(bank_active[r_bs][2]) &&(r_bank_valid) &&(clocks_til_idle[2:0] == 0)) begin // Issue the write command o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b1; o_ram_cas_n <= 1'b0; o_ram_we_n <= 1'b0; o_ram_addr <= { 4'h0, r_addr[NCA-2:0], 1'b0 }; o_ram_bs <= r_bs; clocks_til_idle[2:0] <= 3'h1; o_wb_stall <= 1'b0; r_barrell_ack[1] <= 1'b1; // o_ram_data <= r_data[31:16]; // o_ram_dmod <= `DMOD_PUTOUTPUT; nxt_dmod <= `DMOD_PUTOUTPUT; end else if ((r_pending)&&(r_addr[(NCA-2):0] >= COL_THRESHOLD) &&(!fwd_bank_valid)) begin // Do I need to close the next bank I'll need? if (bank_active[fwd_bs][2:1]==2'b11) begin // Need to close the bank first o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b0; o_ram_cas_n <= 1'b1; o_ram_we_n <= 1'b0; o_ram_addr[10] <= 1'b0; o_ram_bs <= fwd_bs; bank_active[fwd_bs][2] <= 1'b0; end else if (bank_active[fwd_bs]==0) begin // Need to (pre-)activate the next bank o_ram_cs_n <= 1'b0; o_ram_ras_n <= 1'b0; o_ram_cas_n <= 1'b1; o_ram_we_n <= 1'b1; o_ram_addr <= fwd_row; o_ram_bs <= fwd_bs; // clocks_til_idle[3:0] <= 1; bank_active[fwd_bs] <= 3'h4; bank_row[fwd_bs] <= fwd_row; end end if (!i_wb_cyc) r_barrell_ack <= 0; end reg startup_hold; reg [15:0] startup_idle; initial startup_idle = 16'd20500; initial startup_hold = 1'b1; always @(posedge i_clk) if (|startup_idle) startup_idle <= startup_idle - 1'b1; always @(posedge i_clk) startup_hold <= |startup_idle; `ifdef FORMAL always @(*) if (startup_hold) assert(maintenance_mode); always @(*) if (|startup_idle) assert(startup_hold); `endif reg [3:0] maintenance_clocks; reg maintenance_clocks_zero; initial maintenance_mode = 1'b1; initial maintenance_clocks = 4'hf; initial maintenance_clocks_zero = 1'b0; initial m_ram_addr = { 2'b00, 1'b0, 2'b00, 3'b010, 1'b0, 3'b001 }; initial m_state = `RAM_POWER_UP; initial m_ram_cs_n = 1'b1; initial m_ram_ras_n = 1'b1; initial m_ram_cas_n = 1'b1; initial m_ram_we_n = 1'b1; initial m_ram_dmod = `DMOD_GETINPUT; always @(posedge i_clk) begin if (!maintenance_clocks_zero) begin maintenance_clocks <= maintenance_clocks - 4'h1; maintenance_clocks_zero <= (maintenance_clocks == 4'h1); end // The only time the RAM address matters is when we set // the mode. At other times, addr[10] matters, but the rest // is ignored. Hence ... we'll set it to a constant. m_ram_addr <= { 2'b00, 1'b0, 2'b00, 3'b010, 1'b0, 3'b001 }; if (m_state == `RAM_POWER_UP) begin // All signals must be held in NOOP state during powerup // m_ram_cke <= 1'b1; m_ram_cs_n <= 1'b1; m_ram_ras_n <= 1'b1; m_ram_cas_n <= 1'b1; m_ram_we_n <= 1'b1; m_ram_dmod <= `DMOD_GETINPUT; if (!startup_hold) begin m_state <= `RAM_SET_MODE; maintenance_clocks <= 4'h3; maintenance_clocks_zero <= 1'b0; // Precharge all cmd m_ram_cs_n <= 1'b0; m_ram_ras_n <= 1'b0; m_ram_cas_n <= 1'b1; m_ram_we_n <= 1'b0; m_ram_addr[10] <= 1'b1; end end else if (m_state == `RAM_SET_MODE) begin // Wait m_ram_cs_n <= 1'b1; m_ram_cs_n <= 1'b1; m_ram_ras_n <= 1'b1; m_ram_cas_n <= 1'b1; m_ram_we_n <= 1'b1; m_ram_addr[10] <= 1'b1; if (maintenance_clocks_zero) begin // Set mode cycle m_ram_cs_n <= 1'b0; m_ram_ras_n <= 1'b0; m_ram_cas_n <= 1'b0; m_ram_we_n <= 1'b0; m_ram_dmod <= `DMOD_GETINPUT; m_ram_addr[10] <= 1'b0; m_state <= `RAM_INITIAL_REFRESH; maintenance_clocks <= 4'hc; maintenance_clocks_zero <= 1'b0; end end else if (m_state == `RAM_INITIAL_REFRESH) begin // Refresh command if (maintenance_clocks > 4'ha) // Wait two clocks first m_ram_cs_n <= 1'b1; else if (maintenance_clocks > 4'h2) m_ram_cs_n <= 1'b0; else m_ram_cs_n <= 1'b1; m_ram_ras_n <= 1'b0; m_ram_cas_n <= 1'b0; m_ram_we_n <= 1'b1; m_ram_dmod <= `DMOD_GETINPUT; // m_ram_addr <= { 3'b000, 1'b0, 2'b00, 3'b010, 1'b0, 3'b001 }; if (maintenance_clocks_zero) maintenance_mode <= 1'b0; end end always @(posedge i_clk) if (nxt_dmod) o_ram_data <= r_data[15:0]; else o_ram_data <= r_data[31:16]; always @(posedge i_clk) if (maintenance_mode) o_ram_dqm <= 2'b11; else if (r_we) begin if (nxt_dmod) o_ram_dqm <= ~r_sel[1:0]; else o_ram_dqm <= ~r_sel[3:2]; end else o_ram_dqm <= 2'b00; `ifdef VERILATOR // While I hate to build something that works one way under Verilator // and another way in practice, this really isn't that. The problem // \/erilator is having is resolved in toplevel.v---one file that // \/erilator doesn't implement. In toplevel.v, there's not only a // single clocked latch but two taking place. Here, we replicate one // of those. The second takes place (somehow) within the sdramsim.cpp // file. reg [15:0] ram_data, last_ram_data; always @(posedge i_clk) ram_data <= i_ram_data; always @(posedge i_clk) last_ram_data <= ram_data; assign o_wb_data = { last_ram_data, ram_data }; `else reg [15:0] last_ram_data; always @(posedge i_clk) last_ram_data <= i_ram_data; assign o_wb_data = { last_ram_data, i_ram_data }; `endif assign o_wb_ack = r_barrell_ack[0]; // // The following outputs are not necessary for the functionality of // the SDRAM, but they can be used to feed an external "scope" to // get an idea of what the internals of this SDRAM are doing. // // Just be aware of the r_we: it is set based upon the currently pending // transaction, or (if none is pending) based upon the last transaction. // If you want to capture the first value "written" to the device, // you'll need to write a nothing value to the device to set r_we. // The first value "written" to the device can be caught in the next // interaction after that. // reg trigger; always @(posedge i_clk) trigger <= ((o_wb_data[15:0]==o_wb_data[31:16]) &&(o_wb_ack)&&(!i_wb_we)); assign o_debug = { i_wb_cyc, i_wb_stb, i_wb_we, o_wb_ack, o_wb_stall, // 5 o_ram_cs_n, o_ram_ras_n, o_ram_cas_n, o_ram_we_n, o_ram_bs,//6 o_ram_dmod, r_pending, // 2 trigger, // 1 o_ram_addr[9:0], // 10 more (r_we) ? { o_ram_data[7:0] } // 8 values : { o_wb_data[23:20], o_wb_data[3:0] } // i_ram_data[7:0] }; // Make Verilator happy // verilator lint_off UNUSED wire [NCA-1:0] unused; assign unused = { fwd_addr[NCA-1:0] }; // verilator lint_on UNUSED `ifdef FORMAL localparam REFRESH_CLOCKS = 6; localparam ACTIVATE_CLOCKS = 6; // This device is 23MB, assert such always @(*) assert(AW == 21); always @(*) assert(NRA+NCA+2 == AW+1); wire [(5-1):0] f_nreqs, f_nacks, f_outstanding; reg f_past_valid; wire f_reset; always @(*) if (o_ram_dmod) assume(i_ram_data == o_ram_data); initial f_past_valid = 1'b0; always @(posedge i_clk) f_past_valid <= 1'b1; assign f_reset = !f_past_valid; always @(*) if (o_ram_dmod) assert(i_ram_data == o_ram_data); // Properties // 1. Wishbone fwb_slave #( .AW(AW), .DW(DW), .F_MAX_STALL(ACTIVATE_CLOCKS + REFRESH_CLOCKS + ACTIVATE_CLOCKS + RDLY +ACTIVATE_CLOCKS), .F_MAX_ACK_DELAY(REFRESH_CLOCKS + ACTIVATE_CLOCKS + ACTIVATE_CLOCKS + ACTIVATE_CLOCKS+RDLY), .F_LGDEPTH(5)) fwb(i_clk, f_reset, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, o_wb_ack, o_wb_stall, o_wb_data, 1'b0, f_nreqs, f_nacks, f_outstanding); // 2. Proper startup ... // 3. Operation // 4. Refresh // 4. SDRAM request == WB request // // Once we leave maintenance mode (i.e. startup sequence), we *cannot* // go back into it. always @(posedge i_clk) if ((f_past_valid)&&(!$past(maintenance_mode))) assert(!maintenance_mode); // On the very first clock, we must always start up in maintenance mode always @(posedge i_clk) if (!f_past_valid) assert(maintenance_mode); // Just to make things simpler, assume no accesses to the core during // maintenance mode. Such accesses might violate our minimum // acknowledgement time criteria for the wishbone above always @(posedge i_clk) if ((f_past_valid)&&(maintenance_mode)) assume(!i_wb_stb); // Likewise, assert that there are *NO* outstanding transactions in // this maintenance mode always @(posedge i_clk) if ((f_past_valid)&&(maintenance_mode)) assert(f_outstanding == 0); // ... and that while we are in maintenance mode, any incoming request // is stalled. This guarantees that our assumptions above are kept // valid. always @(posedge i_clk) if ((f_past_valid)&&(maintenance_mode)) assume(o_wb_stall); // If there are no attempts to access memory while in maintenance // mode, then there should never be any pending operations upon // completion of maintenance mode always @(posedge i_clk) if ((f_past_valid)&&(maintenance_mode)) assert(!r_pending); wire [(2+AW+DW+DW/8-1):0] f_pending, f_request; assign f_pending = { r_pending, r_we, r_addr, r_data, r_sel }; assign f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }; always @(posedge i_clk) if ((f_past_valid)&&($past(r_pending))&&($past(i_wb_cyc)) &&(($past(o_ram_cs_n)) ||(!$past(o_ram_ras_n)) ||($past(o_ram_cas_n))) ) assert($stable(f_pending)); wire [4:0] f_cmd; assign f_cmd = { o_ram_addr[10], o_ram_cs_n, o_ram_ras_n, o_ram_cas_n, o_ram_we_n }; `define F_MODE_SET 5'b?0000 `define F_BANK_PRECHARGE 5'b00010 `define F_PRECHARGE_ALL 5'b10010 `define F_BANK_ACTIVATE 5'b?0011 `define F_WRITE 5'b00100 `define F_READ 5'b00101 `define F_REFRESH 5'b?0001 `define F_NOOP 5'b?0111 `define F_BANK_ACTIVATE_S 4'b0011 `define F_REFRESH_S 4'b0001 `define F_NOOP_S 4'b0111 reg [(AW-1):0] f_next_addr; always @(*) begin f_next_addr = 0; f_next_addr[(AW-1):NCA-1] = r_addr[(AW-1):NCA-1] + 1'b1; end wire [NRA-1:0] f_next_row, f_this_row; wire [1:0] f_next_bank, f_this_bank; assign f_next_row = f_next_addr[(AW-1):(NCA+1)]; assign f_next_bank = f_next_addr[NCA:NCA-1]; assign f_this_bank = r_bs; assign f_this_row = r_row; always @(*) if (o_ram_cs_n==1'b0) casez(f_cmd) `F_MODE_SET: begin end `F_BANK_PRECHARGE: begin end `F_PRECHARGE_ALL: begin end `F_BANK_ACTIVATE: begin end `F_WRITE: begin end `F_READ: begin end `F_REFRESH: begin end default: assert(f_cmd[3:0] == `F_NOOP_S); endcase always @(posedge i_clk) if ((f_past_valid)&&(!maintenance_mode)) casez(f_cmd) `F_BANK_ACTIVATE: begin // Can only activate de-activated banks assert(bank_active[o_ram_bs][1:0] == 0); // Need to activate the right bank if (o_ram_bs == $past(f_this_bank)) assert($past(f_this_row)==o_ram_addr); else if (o_ram_bs != 0) begin assert(o_ram_bs == $past(f_next_bank)); assert($past(f_this_row)==o_ram_addr); end else begin assert(o_ram_bs == $past(f_next_bank)); assert($past(f_next_row)==o_ram_addr); end end `F_BANK_PRECHARGE: begin // Can only precharge (de-active) a fully active bank assert(bank_active[o_ram_bs] == 3'b011); end `F_PRECHARGE_ALL: begin // If pre-charging all, one of the banks must be active and in // need of a pre-charge assert( (bank_active[0] == 3'b011) ||(bank_active[1] == 3'b011) ||(bank_active[2] == 3'b011) ||(bank_active[3] == 3'b011) ); end `F_WRITE: begin assert($past(r_we)); assert(bank_active[o_ram_bs] == 3'b111); assert(bank_row[o_ram_bs] == $past(f_this_row)); assert(o_ram_bs == $past(f_this_bank)); assert(o_ram_addr[0] == 1'b0); end `F_READ: begin assert(!$past(r_we)); assert(bank_active[o_ram_bs] == 3'b111); assert(bank_row[o_ram_bs] == $past(f_this_row)); assert(o_ram_bs == $past(f_this_bank)); assert(o_ram_addr[0] == 1'b0); end `F_REFRESH: begin // When giving a reset command, *all* banks must be inactive assert( (bank_active[0] == 3'h0) &&(bank_active[1] == 3'h0) &&(bank_active[2] == 3'h0) &&(bank_active[3] == 3'h0) ); end default: assert((o_ram_cs_n)||(f_cmd[3:0] == `F_NOOP_S)); endcase integer f_k; always @(posedge i_clk) if ((f_past_valid)&&(!$past(maintenance_mode))) begin for(f_k=0; f_k<4; f_k=f_k+1) if (((f_cmd[3:0] != `F_BANK_ACTIVATE_S)) ||(o_ram_bs != f_k[1:0])) assert($stable(bank_row[f_k[1:0]])); end always @(posedge i_clk) if ((f_past_valid)&&(!$past(maintenance_mode)) &&($past(f_cmd) != `F_READ) &&($past(f_cmd) != `F_WRITE) ) begin if (($past(r_pending))&&($past(i_wb_cyc))) assert($stable(f_pending)); end always @(posedge i_clk) if ((f_past_valid)&&(!maintenance_mode)) if ((r_pending)&&(f_cmd != `F_READ)&&(f_cmd != `F_WRITE)) assert(o_wb_stall); always @(posedge i_clk) if ((f_past_valid)&&(!$past(maintenance_mode))) casez($past(f_cmd)) `F_BANK_ACTIVATE: begin assert(bank_active[$past(o_ram_bs)] == 3'b110); assert(bank_row[$past(o_ram_bs)] == $past(o_ram_addr)); end `F_BANK_PRECHARGE: begin assert(bank_active[$past(o_ram_bs)] == 3'b001); end `F_PRECHARGE_ALL: begin assert(bank_active[0][2] == 1'b0); assert(bank_active[1][2] == 1'b0); assert(bank_active[2][2] == 1'b0); assert(bank_active[3][2] == 1'b0); end // `F_WRITE: // `F_READ: `F_REFRESH: begin assert(r_barrell_ack == 0); end default: begin end endcase always @(posedge i_clk) if ((f_past_valid)&&(!$past(maintenance_mode))) begin assert(bank_active[0][1:0] == $past(bank_active[0][2:1])); assert(bank_active[1][1:0] == $past(bank_active[1][2:1])); assert(bank_active[2][1:0] == $past(bank_active[2][2:1])); assert(bank_active[3][1:0] == $past(bank_active[3][2:1])); end always @(*) `ifdef VERIFIC if (in_refresh) `else if ((in_refresh)||(maintenance_mode)) `endif begin assert(bank_active[0] == 0); assert(bank_active[1] == 0); assert(bank_active[2] == 0); assert(bank_active[3] == 0); end always @(posedge i_clk) if ((f_past_valid)&&($past(o_wb_ack))) assert(!o_wb_ack); reg [3:0] f_acks_pending; always @(*) begin f_acks_pending = 0; for(f_k=0; f_k