URL https://opencores.org/ocsvn/qspiflash/qspiflash/trunk

Subversion Repositories qspiflash

[/] [qspiflash/] [trunk/] [rtl/] [llqspi.v] - Blame information for rev 19

Go to most recent revision | Details | Compare with Previous | View Log


////////////////////////////////////////////////////////////////////////////////
//
// Filename:    llqspi.v
//
// Project:     Wishbone Controlled Quad SPI Flash Controller
//
// Purpose:     Reads/writes a word (user selectable number of bytes) of data
//              to/from a Quad SPI port.  The port is understood to be 
//              a normal SPI port unless the driver requests four bit mode.
//              When not in use, unlike our previous SPI work, no bits will
//              toggle.
//
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015,2017, 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
// <http://www.gnu.org/licenses/> 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 QSPI_IDLE       3'h0
`define QSPI_START      3'h1
`define QSPI_BITS       3'h2
`define QSPI_READY      3'h3
`define QSPI_HOLDING    3'h4
`define QSPI_STOP       3'h5
`define QSPI_STOP_B     3'h6
 
// Modes
`define QSPI_MOD_SPI    2'b00
`define QSPI_MOD_QOUT   2'b10
`define QSPI_MOD_QIN    2'b11
 
// Which level of formal proofs will we be doing?  As a component, or a
// top-level?
`ifdef  LLQSPI_TOP
`define ASSUME  assume
`else
`define ASSUME  assert
`endif
//
module  llqspi(i_clk,
                // Module interface
                i_wr, i_hold, i_word, i_len, i_spd, i_dir,
                        o_word, o_valid, o_busy,
                // QSPI interface
                o_sck, o_cs_n, o_mod, o_dat, i_dat);
        input   wire            i_clk;
        // Chip interface
        //      Can send info
        //              i_dir = 1, i_spd = 0, i_hold = 0, i_wr = 1,
        //                      i_word = { 1'b0, 32'info to send },
        //                      i_len = # of bytes in word-1
        input   wire            i_wr, i_hold;
        input   wire    [31:0]   i_word;
        input   wire    [1:0]    i_len;  // 0=>8bits, 1=>16 bits, 2=>24 bits, 3=>32 bits
        input   wire            i_spd; // 0 -> normal QPI, 1 -> QSPI
        input   wire            i_dir; // 0 -> read, 1 -> write to SPI
        output  reg     [31:0]   o_word;
        output  reg             o_valid, o_busy;
        // Interface with the QSPI lines
        output  reg             o_sck;
        output  reg             o_cs_n;
        output  reg     [1:0]    o_mod;
        output  reg     [3:0]    o_dat;
        input   wire    [3:0]    i_dat;
 
        // output       wire    [22:0]  o_dbg;
        // assign       o_dbg = { state, spi_len,
                // o_busy, o_valid, o_cs_n, o_sck, o_mod, o_dat, i_dat };
 
        // Timing:
        //
        //      Tick    Clk     BSY/WR  CS_n    BIT/MO  STATE
        //       0      1       0/0     1        -      
        //       1      1       0/1     1        -
        //       2      1       1/0     0         -      QSPI_START
        //       3      0        1/0     0         -      QSPI_START
        //       4      0        1/0     0         0      QSPI_BITS
        //       5      1       1/0     0         0      QSPI_BITS
        //       6      0        1/0     0         1      QSPI_BITS
        //       7      1       1/0     0         1      QSPI_BITS
        //       8      0        1/0     0         2      QSPI_BITS
        //       9      1       1/0     0         2      QSPI_BITS
        //      10      0        1/0     0         3      QSPI_BITS
        //      11      1       1/0     0         3      QSPI_BITS
        //      12      0        1/0     0         4      QSPI_BITS
        //      13      1       1/0     0         4      QSPI_BITS
        //      14      0        1/0     0         5      QSPI_BITS
        //      15      1       1/0     0         5      QSPI_BITS
        //      16      0        1/0     0         6      QSPI_BITS
        //      17      1       1/1     0         6      QSPI_BITS
        //      18      0        1/1     0         7      QSPI_READY
        //      19      1       0/1     0         7      QSPI_READY
        //      20      0        1/0/V   0         8      QSPI_BITS
        //      21      1       1/0     0         8      QSPI_BITS
        //      22      0        1/0     0         9      QSPI_BITS
        //      23      1       1/0     0         9      QSPI_BITS
        //      24      0        1/0     0        10      QSPI_BITS
        //      25      1       1/0     0        10      QSPI_BITS
        //      26      0        1/0     0        11      QSPI_BITS
        //      27      1       1/0     0        11      QSPI_BITS
        //      28      0        1/0     0        12      QSPI_BITS
        //      29      1       1/0     0        12      QSPI_BITS
        //      30      0        1/0     0        13      QSPI_BITS
        //      31      1       1/0     0        13      QSPI_BITS
        //      32      0        1/0     0        14      QSPI_BITS
        //      33      1       1/0     0        14      QSPI_BITS
        //      34      0        1/0     0        15      QSPI_READY
        //      35      1       1/0     0        15      QSPI_READY
        //      36      1       1/0/V   0         -      QSPI_STOP
        //      37      1       1/0     0         -      QSPI_STOPB
        //      38      1       1/0     1        -      QSPI_IDLE
        //      39      1       0/0     1        -
        // Now, let's switch from single bit to quad mode
        //      40      1       0/0     1        -      QSPI_IDLE
        //      41      1       0/1     1        -      QSPI_IDLE
        //      42      1       1/0     0         -      QSPI_START
        //      43      0        1/0     0         -      QSPI_START
        //      44      0        1/0     0         0      QSPI_BITS
        //      45      1       1/0     0         0      QSPI_BITS
        //      46      0        1/0     0         1      QSPI_BITS
        //      47      1       1/0     0         1      QSPI_BITS
        //      48      0        1/0     0         2      QSPI_BITS
        //      49      1       1/0     0         2      QSPI_BITS
        //      50      0        1/0     0         3      QSPI_BITS
        //      51      1       1/0     0         3      QSPI_BITS
        //      52      0        1/0     0         4      QSPI_BITS
        //      53      1       1/0     0         4      QSPI_BITS
        //      54      0        1/0     0         5      QSPI_BITS
        //      55      1       1/0     0         5      QSPI_BITS
        //      56      0        1/0     0         6      QSPI_BITS
        //      57      1       1/1/QR  0         6      QSPI_BITS
        //      58      0        1/1/QR  0         7      QSPI_READY
        //      59      1       0/1/QR  0         7      QSPI_READY
        //      60      0        1/0/?/V 0         8-11   QSPI_BITS
        //      61      1       1/0/?   0         8-11   QSPI_BITS
        //      62      0        1/0/?   0         12-15  QSPI_BITS
        //      63      1       1/0/?   0         12-15  QSPI_BITS
        //      64      1       1/0/?/V 0        -       QSPI_STOP
        //      65      1       1/0/?   0        -       QSPI_STOPB
        //      66      1       1/0/?   1       -       QSPI_IDLE
        //      67      1       0/0     1       -       QSPI_IDLE
        // Now let's try something entirely in Quad read mode, from the
        // beginning
        //      68      1       0/1/QR  1       -       QSPI_IDLE
        //      69      1       1/0     0        -       QSPI_START
        //      70      0        1/0     0        -       QSPI_START
        //      71      0        1/0     0        0-3     QSPI_BITS
        //      72      1       1/0     0        0-3     QSPI_BITS
        //      73      0        1/1/QR  0        4-7     QSPI_BITS
        //      74      1       0/1/QR  0        4-7     QSPI_BITS
        //      75      0        1/?/?/V 0        8-11    QSPI_BITS
        //      76      1       1/?/?   0        8-11    QSPI_BITS
        //      77      0        1/1/QR  0        12-15   QSPI_BITS
        //      78      1       0/1/QR  0        12-15   QSPI_BITS
        //      79      0        1/?/?/V 0        16-19   QSPI_BITS
        //      80      1       1/0     0        16-19   QSPI_BITS
        //      81      0        1/0     0        20-23   QSPI_BITS
        //      82      1       1/0     0        20-23   QSPI_BITS
        //      83      1       1/0/V   0        -       QSPI_STOP
        //      84      1       1/0     0        -       QSPI_STOPB
        //      85      1       1/0     1       -       QSPI_IDLE
        //      86      1       0/0     1       -       QSPI_IDLE
 
        wire    i_miso;
        assign  i_miso = i_dat[1];
 
        reg             r_spd, r_dir;
        reg     [5:0]    spi_len;
        reg     [31:0]   r_word;
        reg     [30:0]   r_input;
        reg     [2:0]    state;
        initial state = `QSPI_IDLE;
        initial o_sck   = 1'b1;
        initial o_cs_n  = 1'b1;
        initial o_dat   = 4'hd;
        initial o_valid = 1'b0;
        initial o_busy  = 1'b0;
        initial r_input = 31'h000;
        initial o_mod   = `QSPI_MOD_SPI;
        initial o_word  = 0;
        always @(posedge i_clk)
                if ((state == `QSPI_IDLE)&&(o_sck))
                begin
                        o_cs_n <= 1'b1;
                        o_valid <= 1'b0;
                        o_busy  <= 1'b0;
                        o_mod <= `QSPI_MOD_SPI;
                        r_word <= i_word;
                        r_spd <= i_spd;
                        r_dir <= i_dir;
                        if ((i_wr)&&(!o_busy))
                        begin
                                state <= `QSPI_START;
                                spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8;
                                o_cs_n <= 1'b0;
                                // o_sck <= 1'b1;
                                o_busy <= 1'b1;
                        end
                end else if (state == `QSPI_START)
                begin // We come in here with sck high, stay here 'til sck is low
                        o_sck <= 1'b0;
                        if (o_sck == 1'b0)
                        begin
                                state <= `QSPI_BITS;
                                spi_len<= spi_len - ( (r_spd)? 6'h4 : 6'h1 );
                                if (r_spd)
                                        r_word <= { r_word[27:0], 4'h0 };
                                else
                                        r_word <= { r_word[30:0], 1'b0 };
                        end
                        o_mod <= (r_spd) ? { 1'b1, r_dir } : `QSPI_MOD_SPI;
                        o_cs_n <= 1'b0;
                        o_busy <= 1'b1;
                        o_valid <= 1'b0;
                        if (r_spd)
                                o_dat <= r_word[31:28];
                        else
                                o_dat <= { 3'b110, r_word[31] };
                end else if (!o_sck)
                begin
                        o_sck <= 1'b1;
                        o_busy <= ((state != `QSPI_READY)||(!i_wr));
                        o_valid <= 1'b0;
                end else if (state == `QSPI_BITS)
                begin
                        // Should enter into here with at least a spi_len
                        // of one, perhaps more
                        o_sck <= 1'b0;
                        o_busy <= 1'b1;
                        if (r_spd)
                        begin
                                o_dat <= r_word[31:28];
                                r_word <= { r_word[27:0], 4'h0 };
                                spi_len <= spi_len - 6'h4;
                                if (spi_len == 6'h4)
                                        state <= `QSPI_READY;
                        end else begin
                                o_dat <= { 3'b110, r_word[31] };
                                r_word <= { r_word[30:0], 1'b0 };
                                spi_len <= spi_len - 6'h1;
                                if (spi_len == 6'h1)
                                        state <= `QSPI_READY;
                        end
 
                        o_valid <= 1'b0;
                        if (!o_mod[1])
                                r_input <= { r_input[29:0], i_miso };
                        else if (o_mod[1])
                                r_input <= { r_input[26:0], i_dat };
                end else if (state == `QSPI_READY)
                begin
                        o_valid <= 1'b0;
                        o_cs_n <= 1'b0;
                        o_busy <= 1'b1;
                        // This is the state on the last clock (both low and
                        // high clocks) of the data.  Data is valid during
                        // this state.  Here we chose to either STOP or
                        // continue and transmit more.
                        o_sck <= (i_hold); // No clocks while holding
                        r_spd <= i_spd;
                        r_dir <= i_dir;
                        if (i_spd)
                        begin
                                r_word <= { i_word[27:0], 4'h0 };
                                spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h4;
                        end else begin
                                r_word <= { i_word[30:0], 1'b0 };
                                spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h1;
                        end
                        if((!o_busy)&&(i_wr))// Acknowledge a new request
                        begin
                                state <= `QSPI_BITS;
                                o_busy <= 1'b1;
                                o_sck <= 1'b0;
 
                                // Read the new request off the bus
                                // Set up the first bits on the bus
                                o_mod <= (i_spd) ? { 1'b1, i_dir } : `QSPI_MOD_SPI;
                                if (i_spd)
                                        o_dat <= i_word[31:28];
                                else
                                        o_dat <= { 3'b110, i_word[31] };
 
                        end else begin
                                o_sck <= 1'b1;
                                state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
                                o_busy <= (!i_hold);
                        end
 
                        // Read a bit upon any transition
                        o_valid <= 1'b1;
                        if (!o_mod[1])
                        begin
                                r_input <= { r_input[29:0], i_miso };
                                o_word  <= { r_input[30:0], i_miso };
                        end else if (o_mod[1])
                        begin
                                r_input <= { r_input[26:0], i_dat };
                                o_word  <= { r_input[27:0], i_dat };
                        end
                end else if (state == `QSPI_HOLDING)
                begin
                        // We need this state so that the o_valid signal
                        // can get strobed with our last result.  Otherwise
                        // we could just sit in READY waiting for a new command.
                        //
                        // Incidentally, the change producing this state was
                        // the result of a nasty race condition.  See the
                        // commends in wbqspiflash for more details.
                        //
                        o_valid <= 1'b0;
                        o_cs_n <= 1'b0;
                        o_busy <= 1'b0;
                        r_spd <= i_spd;
                        r_dir <= i_dir;
                        if (i_spd)
                        begin
                                r_word <= { i_word[27:0], 4'h0 };
                                spi_len<= { 1'b0, i_len, 3'b100 };
                        end else begin
                                r_word <= { i_word[30:0], 1'b0 };
                                spi_len<= { 1'b0, i_len, 3'b111 };
                        end
                        if((!o_busy)&&(i_wr))// Acknowledge a new request
                        begin
                                state  <= `QSPI_BITS;
                                o_busy <= 1'b1;
                                o_sck  <= 1'b0;
 
                                // Read the new request off the bus
                                // Set up the first bits on the bus
                                o_mod<=(i_spd)?{ 1'b1, i_dir } : `QSPI_MOD_SPI;
                                if (i_spd)
                                        o_dat <= i_word[31:28];
                                else
                                        o_dat <= { 3'b110, i_word[31] };
                        end else begin
                                o_sck <= 1'b1;
                                state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
                                o_busy <= (!i_hold);
                        end
                end else if (state == `QSPI_STOP)
                begin
                        o_sck   <= 1'b1; // Stop the clock
                        o_valid <= 1'b0; // Output may have just been valid, but no more
                        o_busy  <= 1'b1; // Still busy till port is clear
                        state <= `QSPI_STOP_B;
                        o_mod <= `QSPI_MOD_SPI;
                end else if (state == `QSPI_STOP_B)
                begin
                        o_cs_n <= 1'b1;
                        o_sck <= 1'b1;
                        // Do I need this????
                        // spi_len <= 3; // Minimum CS high time before next cmd
                        state <= `QSPI_IDLE;
                        o_valid <= 1'b0;
                        o_busy <= 1'b1;
                        o_mod <= `QSPI_MOD_SPI;
                end else begin // Invalid states, should never get here
                        state   <= `QSPI_STOP;
                        o_valid <= 1'b0;
                        o_busy  <= 1'b1;
                        o_cs_n  <= 1'b1;
                        o_sck   <= 1'b1;
                        o_mod   <= `QSPI_MOD_SPI;
                        o_dat   <= 4'hd;
                end
 
`ifdef  FORMAL
        reg     prev_i_clk, past_valid;
 
        initial `ASSUME(i_clk == 1'b0);
        initial prev_i_clk  = 1;
        always @($global_clock)
        begin
                prev_i_clk  <= i_clk;
                `ASSUME(i_clk != prev_i_clk);
        end
 
        reg     past_valid;
        initial past_valid = 1'b0;
        always @(posedge i_clk)
                past_valid <= 1'b1;
 
        /*
        always @(*)
                if (!$stable(i_spd))
                        assert($rose(i_clk));
        */
 
        always @(posedge i_clk) begin
                if ((past_valid)&&($past(i_wr))&&($past(o_busy)))
                begin
                        // any time i_wr and o_busy are true, nothing changes
                        // of spd, len, word or dir
                        `ASSUME(i_wr);
                        `ASSUME(i_spd  == $past(i_spd));
                        `ASSUME(i_len  == $past(i_len));
                        `ASSUME(i_word == $past(i_word));
                        `ASSUME(i_dir  == $past(i_dir));
                        `ASSUME(i_hold == $past(i_hold));
                end
                if ((past_valid)&&($past(i_wr))&&($past(o_busy))&&($past(state == `QSPI_IDLE)))
                        assert($past(state)==state);
                if (i_hold == $past(i_hold))
                        assert($stable(i_hold));
        end
 
        always @(*) begin
                if (o_mod == `QSPI_MOD_QOUT)
                        `ASSUME(i_dat == o_dat);
                if (o_mod == `QSPI_MOD_SPI)
                        `ASSUME(i_dat[3:2] == 2'b11);
                if (o_mod == `QSPI_MOD_SPI)
                        `ASSUME(i_dat[0] == o_dat[0]);
        end
 
        initial `ASSUME(i_wr == 1'b0);
        initial `ASSUME(i_word == 0);
 
        always @($global_clock)
        if (!$rose(i_clk))
        begin
                `ASSUME($stable(i_wr));
                //
                `ASSUME($stable(i_len));
                `ASSUME($stable(i_dir));
                `ASSUME($stable(i_spd));
                `ASSUME($stable(i_word));
                //
                `ASSUME($stable(i_hold));
        end
 
        always @($global_clock)
        if (!$fell(o_sck))
                assume($stable(i_dat));
 
        // This is ... not as believable.  There might be a delay here.
        // For now, we'll just assume (not necessarily true) that the
        // output
        always @(posedge i_clk)
                if (past_valid)
                `ASSUME( (i_dat == $past(i_dat)) || (o_sck != $past(o_sck)) );
 
        reg     f_last_sck;
        always @(posedge i_clk)
                f_last_sck <= o_sck;
 
        reg     [31:0]   f_shiftreg, f_goal;
        initial f_shiftreg = 0;
        initial f_goal = 0;
        always @(posedge i_clk)
                if ((o_sck)&&(!f_last_sck))
                begin
                        if (o_mod == `QSPI_MOD_QOUT)
                                f_shiftreg <= { f_shiftreg[28:0], o_dat };
                        else if (o_mod == `QSPI_MOD_SPI)
                                f_shiftreg <= { f_shiftreg[30:0], o_dat[0] };
                end
 
        reg     [5:0]    f_nsent, f_vsent;
        reg     [2:0]    f_nbits_r;
        wire    [5:0]    f_nbits;
        always @(posedge i_clk)
                if ((i_wr)&&(!o_busy))
                begin
                        f_goal <= i_word;
                        f_nbits_r <= { 1'b0, i_len } + 3'h1;
                end
        assign  f_nbits = { f_nbits_r, 3'b000 };
        always @(posedge i_clk)
                if ((!o_sck)||(!o_cs_n))
                        assert(f_nbits != 0);
 
        always @(posedge i_clk)
                if (o_cs_n)
                        f_nsent <= 0;
                else if ((!o_busy)&&(i_wr))
                        f_nsent <= 0;
                else if ((!f_last_sck)&&(o_sck))
                begin
                        if (o_mod == `QSPI_MOD_SPI)
                                f_nsent <= f_nsent + 6'h1;
                        else
                                f_nsent <= f_nsent + 6'h4;
                end
        always @(posedge i_clk)
                if (o_cs_n)
                        f_vsent <= 0;
                else
                        f_vsent <= f_nsent;
        always @(posedge i_clk)
                if ((!o_cs_n)&&(state == `QSPI_BITS)&&(!o_sck))
                begin
                        if (o_mod != `QSPI_MOD_SPI)
                                assert(f_nsent + spi_len + 6'h4 == f_nbits);
                        else
                                assert(f_nsent + spi_len + 6'h1 == f_nbits);
                end
 
        always @(posedge i_clk)
                assert((o_busy)||(f_goal[(f_nbits-1):0] == f_shiftreg[(f_nbits-1):0]));
 
        always @(posedge i_clk) begin
                // We are only ever in one of three speed modes, fourth mode
                // isn't allowed
                assert( (o_mod == `QSPI_MOD_SPI)
                        ||(o_mod == `QSPI_MOD_QIN)
                        ||(o_mod == `QSPI_MOD_QOUT));
 
                if ((past_valid)&&($past(i_wr))&&(!$past(o_busy)))
                begin
                        // Any accepted request leaves us in an active state
                        assert(!o_cs_n);
 
                        // Any accepted request allows us to set our speed
                        assert(r_spd == $past(i_spd));
                end
 
                // We're either busy, or idle with the clock high
                //   or pausing (upon a request) mid-transaction
                assert((o_busy)
                        ||((state == `QSPI_IDLE)&&(o_sck)&&(o_cs_n))
                        ||((state == `QSPI_READY)&&(o_sck)&&(!o_cs_n))
                        ||((state == `QSPI_HOLDING)&&(o_sck)&&(!o_cs_n))
                        );
 
                // Anytime CS is idle, SCK is high
                if (o_cs_n)
                        assert(o_sck);
 
 
                // What can we assert about i_hold?
 
                // When i_hold is asserted before a transaction completes,
                // the transaction will "hold" and wait for a next input.
                // i.e. the clock will stop
 
                // First assert that o_busy will be deasserted any time the
                // currently requested word has been sent
                //
                //if ((($past(i_wr))||(i_hold))
                //              &&(f_nsent == f_nbits)&&(!o_sck)&&(!o_cs_n))
                //      assert(!o_busy);
 
 
                // First, assert of i_hold that !o_busy will be set.
                if ((past_valid)&&($past(i_hold))&&(f_nsent == f_nbits)&&(!o_cs_n))
                begin
                        assert((!o_busy)||(o_sck));
                end
                if ((past_valid)&&($past(i_hold))&&(!$past(i_wr))
                        &&(!$past(o_busy))&&(!$past(o_cs_n)))
                begin
                        assert(!o_cs_n);
                        assert($past(o_sck)==o_sck);
                end
 
                // DATA only changes on the falling edge of SCK
                if ((past_valid)&&(o_sck))
                        assert(o_dat==$past(o_dat));
 
                // Valid is only ever true for one clock
                if ((past_valid)&&(o_valid))
                        assert(!$past(o_valid));
 
                // Valid is only ever true after receiving a full number of bits
                if ((past_valid)&&(o_valid))
                begin
                        if ((!$past(i_wr))||($past(o_busy)))
                                assert(f_nsent == f_nbits);
                end
 
                // In SPI mode, the top bits of o_dat are always 3'b110
                //
                // This should be true, but there's a problem holding this
                // true
                // assert( (o_mod != `QSPI_MOD_SPI)||(o_dat[3:1] == 3'b110) );
 
                // Either valid is true (this clock), or our output word is
                // identical to what it was on the last clock
                if (past_valid)
                        assert((o_valid) || (o_word == $past(o_word)));
        end
`endif
 
endmodule

Line No.	Rev	Author	Line
1	16	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
2	2	dgisselq	`//`
3			`// Filename: llqspi.v`
4			`//`
5	3	dgisselq	`// Project: Wishbone Controlled Quad SPI Flash Controller`
6	2	dgisselq	`//`
7			`// Purpose: Reads/writes a word (user selectable number of bytes) of data`
8			`// to/from a Quad SPI port. The port is understood to be`
9			`// a normal SPI port unless the driver requests four bit mode.`
10			`// When not in use, unlike our previous SPI work, no bits will`
11			`// toggle.`
12			`//`
13	16	dgisselq	`// Creator: Dan Gisselquist, Ph.D.`
14	8	dgisselq	`// Gisselquist Technology, LLC`
15	2	dgisselq	`//`
16	16	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
17	2	dgisselq	`//`
18	16	dgisselq	`// Copyright (C) 2015,2017, Gisselquist Technology, LLC`
19	2	dgisselq	`//`
20	3	dgisselq	`// This program is free software (firmware): you can redistribute it and/or`
21			`// modify it under the terms of the GNU General Public License as published`
22			`// by the Free Software Foundation, either version 3 of the License, or (at`
23			`// your option) any later version.`
24			`//`
25			`// This program is distributed in the hope that it will be useful, but WITHOUT`
26			`// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or`
27			`// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License`
28			`// for more details.`
29			`//`
30			`// You should have received a copy of the GNU General Public License along`
31	16	dgisselq	`// with this program. (It's in the $(ROOT)/doc directory. Run make with no`
32	3	dgisselq	`// target there if the PDF file isn't present.) If not, see`
33			`// <http://www.gnu.org/licenses/> for a copy.`
34			`//`
35			`// License: GPL, v3, as defined and found on www.gnu.org,`
36			`// http://www.gnu.org/licenses/gpl.html`
37			`//`
38			`//`
39	16	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
40	14	dgisselq	`//`
41			`//`
42			`default_nettype none
43			`//`
44	4	dgisselq	`define QSPI_IDLE 3'h0
45			`define QSPI_START 3'h1
46			`define QSPI_BITS 3'h2
47			`define QSPI_READY 3'h3
48			`define QSPI_HOLDING 3'h4
49			`define QSPI_STOP 3'h5
50			`define QSPI_STOP_B 3'h6
51	2	dgisselq
52			`// Modes`
53			`define QSPI_MOD_SPI 2'b00
54			`define QSPI_MOD_QOUT 2'b10
55			`define QSPI_MOD_QIN 2'b11
56
57	19	dgisselq	`// Which level of formal proofs will we be doing? As a component, or a`
58			`// top-level?`
59			`ifdef LLQSPI_TOP
60			`define ASSUME assume
61			`else
62			`define ASSUME assert
63			`endif
64			`//`
65	2	dgisselq	`module llqspi(i_clk,`
66			`// Module interface`
67			`i_wr, i_hold, i_word, i_len, i_spd, i_dir,`
68			`o_word, o_valid, o_busy,`
69			`// QSPI interface`
70	3	dgisselq	`o_sck, o_cs_n, o_mod, o_dat, i_dat);`
71	14	dgisselq	`input wire i_clk;`
72	2	dgisselq	`// Chip interface`
73			`// Can send info`
74			`// i_dir = 1, i_spd = 0, i_hold = 0, i_wr = 1,`
75			`// i_word = { 1'b0, 32'info to send },`
76			`// i_len = # of bytes in word-1`
77	14	dgisselq	`input wire i_wr, i_hold;`
78			`input wire [31:0] i_word;`
79			`input wire [1:0] i_len; // 0=>8bits, 1=>16 bits, 2=>24 bits, 3=>32 bits`
80			`input wire i_spd; // 0 -> normal QPI, 1 -> QSPI`
81			`input wire i_dir; // 0 -> read, 1 -> write to SPI`
82	2	dgisselq	`output reg [31:0] o_word;`
83			`output reg o_valid, o_busy;`
84			`// Interface with the QSPI lines`
85			`output reg o_sck;`
86			`output reg o_cs_n;`
87			`output reg [1:0] o_mod;`
88			`output reg [3:0] o_dat;`
89	19	dgisselq	`input wire [3:0] i_dat;`
90	2	dgisselq
91	7	dgisselq	`// output wire [22:0] o_dbg;`
92			`// assign o_dbg = { state, spi_len,`
93			`// o_busy, o_valid, o_cs_n, o_sck, o_mod, o_dat, i_dat };`
94
95	2	dgisselq	`// Timing:`
96			`//`
97			`// Tick Clk BSY/WR CS_n BIT/MO STATE`
98			`// 0 1 0/0 1 -`
99			`// 1 1 0/1 1 -`
100			`// 2 1 1/0 0 - QSPI_START`
101			`// 3 0 1/0 0 - QSPI_START`
102			`// 4 0 1/0 0 0 QSPI_BITS`
103			`// 5 1 1/0 0 0 QSPI_BITS`
104			`// 6 0 1/0 0 1 QSPI_BITS`
105			`// 7 1 1/0 0 1 QSPI_BITS`
106			`// 8 0 1/0 0 2 QSPI_BITS`
107			`// 9 1 1/0 0 2 QSPI_BITS`
108			`// 10 0 1/0 0 3 QSPI_BITS`
109			`// 11 1 1/0 0 3 QSPI_BITS`
110			`// 12 0 1/0 0 4 QSPI_BITS`
111			`// 13 1 1/0 0 4 QSPI_BITS`
112			`// 14 0 1/0 0 5 QSPI_BITS`
113			`// 15 1 1/0 0 5 QSPI_BITS`
114			`// 16 0 1/0 0 6 QSPI_BITS`
115			`// 17 1 1/1 0 6 QSPI_BITS`
116			`// 18 0 1/1 0 7 QSPI_READY`
117			`// 19 1 0/1 0 7 QSPI_READY`
118			`// 20 0 1/0/V 0 8 QSPI_BITS`
119			`// 21 1 1/0 0 8 QSPI_BITS`
120			`// 22 0 1/0 0 9 QSPI_BITS`
121			`// 23 1 1/0 0 9 QSPI_BITS`
122			`// 24 0 1/0 0 10 QSPI_BITS`
123			`// 25 1 1/0 0 10 QSPI_BITS`
124			`// 26 0 1/0 0 11 QSPI_BITS`
125			`// 27 1 1/0 0 11 QSPI_BITS`
126			`// 28 0 1/0 0 12 QSPI_BITS`
127			`// 29 1 1/0 0 12 QSPI_BITS`
128			`// 30 0 1/0 0 13 QSPI_BITS`
129			`// 31 1 1/0 0 13 QSPI_BITS`
130			`// 32 0 1/0 0 14 QSPI_BITS`
131			`// 33 1 1/0 0 14 QSPI_BITS`
132			`// 34 0 1/0 0 15 QSPI_READY`
133			`// 35 1 1/0 0 15 QSPI_READY`
134			`// 36 1 1/0/V 0 - QSPI_STOP`
135			`// 37 1 1/0 0 - QSPI_STOPB`
136			`// 38 1 1/0 1 - QSPI_IDLE`
137			`// 39 1 0/0 1 -`
138			`// Now, let's switch from single bit to quad mode`
139			`// 40 1 0/0 1 - QSPI_IDLE`
140			`// 41 1 0/1 1 - QSPI_IDLE`
141			`// 42 1 1/0 0 - QSPI_START`
142			`// 43 0 1/0 0 - QSPI_START`
143			`// 44 0 1/0 0 0 QSPI_BITS`
144			`// 45 1 1/0 0 0 QSPI_BITS`
145			`// 46 0 1/0 0 1 QSPI_BITS`
146			`// 47 1 1/0 0 1 QSPI_BITS`
147			`// 48 0 1/0 0 2 QSPI_BITS`
148			`// 49 1 1/0 0 2 QSPI_BITS`
149			`// 50 0 1/0 0 3 QSPI_BITS`
150			`// 51 1 1/0 0 3 QSPI_BITS`
151			`// 52 0 1/0 0 4 QSPI_BITS`
152			`// 53 1 1/0 0 4 QSPI_BITS`
153			`// 54 0 1/0 0 5 QSPI_BITS`
154			`// 55 1 1/0 0 5 QSPI_BITS`
155			`// 56 0 1/0 0 6 QSPI_BITS`
156			`// 57 1 1/1/QR 0 6 QSPI_BITS`
157			`// 58 0 1/1/QR 0 7 QSPI_READY`
158			`// 59 1 0/1/QR 0 7 QSPI_READY`
159			`// 60 0 1/0/?/V 0 8-11 QSPI_BITS`
160			`// 61 1 1/0/? 0 8-11 QSPI_BITS`
161			`// 62 0 1/0/? 0 12-15 QSPI_BITS`
162			`// 63 1 1/0/? 0 12-15 QSPI_BITS`
163			`// 64 1 1/0/?/V 0 - QSPI_STOP`
164			`// 65 1 1/0/? 0 - QSPI_STOPB`
165			`// 66 1 1/0/? 1 - QSPI_IDLE`
166			`// 67 1 0/0 1 - QSPI_IDLE`
167			`// Now let's try something entirely in Quad read mode, from the`
168			`// beginning`
169			`// 68 1 0/1/QR 1 - QSPI_IDLE`
170			`// 69 1 1/0 0 - QSPI_START`
171			`// 70 0 1/0 0 - QSPI_START`
172			`// 71 0 1/0 0 0-3 QSPI_BITS`
173			`// 72 1 1/0 0 0-3 QSPI_BITS`
174			`// 73 0 1/1/QR 0 4-7 QSPI_BITS`
175			`// 74 1 0/1/QR 0 4-7 QSPI_BITS`
176			`// 75 0 1/?/?/V 0 8-11 QSPI_BITS`
177			`// 76 1 1/?/? 0 8-11 QSPI_BITS`
178			`// 77 0 1/1/QR 0 12-15 QSPI_BITS`
179			`// 78 1 0/1/QR 0 12-15 QSPI_BITS`
180			`// 79 0 1/?/?/V 0 16-19 QSPI_BITS`
181			`// 80 1 1/0 0 16-19 QSPI_BITS`
182			`// 81 0 1/0 0 20-23 QSPI_BITS`
183			`// 82 1 1/0 0 20-23 QSPI_BITS`
184			`// 83 1 1/0/V 0 - QSPI_STOP`
185			`// 84 1 1/0 0 - QSPI_STOPB`
186			`// 85 1 1/0 1 - QSPI_IDLE`
187			`// 86 1 0/0 1 - QSPI_IDLE`
188
189			`wire i_miso;`
190			`assign i_miso = i_dat[1];`
191
192			`reg r_spd, r_dir;`
193			`reg [5:0] spi_len;`
194			`reg [31:0] r_word;`
195			`reg [30:0] r_input;`
196			`reg [2:0] state;`
197			initial state = `QSPI_IDLE;
198			`initial o_sck = 1'b1;`
199			`initial o_cs_n = 1'b1;`
200			`initial o_dat = 4'hd;`
201			`initial o_valid = 1'b0;`
202			`initial o_busy = 1'b0;`
203			`initial r_input = 31'h000;`
204	16	dgisselq	initial o_mod = `QSPI_MOD_SPI;
205	19	dgisselq	`initial o_word = 0;`
206	2	dgisselq	`always @(posedge i_clk)`
207			if ((state == `QSPI_IDLE)&&(o_sck))
208			`begin`
209			`o_cs_n <= 1'b1;`
210			`o_valid <= 1'b0;`
211			`o_busy <= 1'b0;`
212			o_mod <= `QSPI_MOD_SPI;
213	16	dgisselq	`r_word <= i_word;`
214			`r_spd <= i_spd;`
215			`r_dir <= i_dir;`
216	19	dgisselq	`if ((i_wr)&&(!o_busy))`
217	2	dgisselq	`begin`
218			state <= `QSPI_START;
219			`spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8;`
220			`o_cs_n <= 1'b0;`
221	16	dgisselq	`// o_sck <= 1'b1;`
222	2	dgisselq	`o_busy <= 1'b1;`
223			`end`
224			end else if (state == `QSPI_START)
225			`begin // We come in here with sck high, stay here 'til sck is low`
226			`o_sck <= 1'b0;`
227			`if (o_sck == 1'b0)`
228			`begin`
229			state <= `QSPI_BITS;
230			`spi_len<= spi_len - ( (r_spd)? 6'h4 : 6'h1 );`
231			`if (r_spd)`
232			`r_word <= { r_word[27:0], 4'h0 };`
233			`else`
234			`r_word <= { r_word[30:0], 1'b0 };`
235			`end`
236			o_mod <= (r_spd) ? { 1'b1, r_dir } : `QSPI_MOD_SPI;
237			`o_cs_n <= 1'b0;`
238			`o_busy <= 1'b1;`
239			`o_valid <= 1'b0;`
240			`if (r_spd)`
241			`o_dat <= r_word[31:28];`
242	16	dgisselq	`else`
243	2	dgisselq	`o_dat <= { 3'b110, r_word[31] };`
244	19	dgisselq	`end else if (!o_sck)`
245	2	dgisselq	`begin`
246			`o_sck <= 1'b1;`
247	19	dgisselq	o_busy <= ((state != `QSPI_READY)\|\|(!i_wr));
248	2	dgisselq	`o_valid <= 1'b0;`
249			end else if (state == `QSPI_BITS)
250			`begin`
251			`// Should enter into here with at least a spi_len`
252			`// of one, perhaps more`
253			`o_sck <= 1'b0;`
254			`o_busy <= 1'b1;`
255			`if (r_spd)`
256			`begin`
257			`o_dat <= r_word[31:28];`
258			`r_word <= { r_word[27:0], 4'h0 };`
259			`spi_len <= spi_len - 6'h4;`
260			`if (spi_len == 6'h4)`
261			state <= `QSPI_READY;
262			`end else begin`
263			`o_dat <= { 3'b110, r_word[31] };`
264			`r_word <= { r_word[30:0], 1'b0 };`
265			`spi_len <= spi_len - 6'h1;`
266			`if (spi_len == 6'h1)`
267			state <= `QSPI_READY;
268			`end`
269
270			`o_valid <= 1'b0;`
271	19	dgisselq	`if (!o_mod[1])`
272	2	dgisselq	`r_input <= { r_input[29:0], i_miso };`
273			`else if (o_mod[1])`
274			`r_input <= { r_input[26:0], i_dat };`
275			end else if (state == `QSPI_READY)
276			`begin`
277			`o_valid <= 1'b0;`
278			`o_cs_n <= 1'b0;`
279			`o_busy <= 1'b1;`
280			`// This is the state on the last clock (both low and`
281			`// high clocks) of the data. Data is valid during`
282			`// this state. Here we chose to either STOP or`
283			`// continue and transmit more.`
284	4	dgisselq	`o_sck <= (i_hold); // No clocks while holding`
285	16	dgisselq	`r_spd <= i_spd;`
286			`r_dir <= i_dir;`
287			`if (i_spd)`
288			`begin`
289			`r_word <= { i_word[27:0], 4'h0 };`
290			`spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h4;`
291			`end else begin`
292			`r_word <= { i_word[30:0], 1'b0 };`
293			`spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h1;`
294			`end`
295	19	dgisselq	`if((!o_busy)&&(i_wr))// Acknowledge a new request`
296	2	dgisselq	`begin`
297			state <= `QSPI_BITS;
298			`o_busy <= 1'b1;`
299			`o_sck <= 1'b0;`
300
301			`// Read the new request off the bus`
302			`// Set up the first bits on the bus`
303			o_mod <= (i_spd) ? { 1'b1, i_dir } : `QSPI_MOD_SPI;
304			`if (i_spd)`
305			`o_dat <= i_word[31:28];`
306	16	dgisselq	`else`
307	2	dgisselq	`o_dat <= { 3'b110, i_word[31] };`
308
309			`end else begin`
310			`o_sck <= 1'b1;`
311	4	dgisselq	state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
312	19	dgisselq	`o_busy <= (!i_hold);`
313	16	dgisselq	`end`
314	2	dgisselq
315	16	dgisselq	`// Read a bit upon any transition`
316			`o_valid <= 1'b1;`
317	19	dgisselq	`if (!o_mod[1])`
318	16	dgisselq	`begin`
319			`r_input <= { r_input[29:0], i_miso };`
320			`o_word <= { r_input[30:0], i_miso };`
321			`end else if (o_mod[1])`
322			`begin`
323			`r_input <= { r_input[26:0], i_dat };`
324			`o_word <= { r_input[27:0], i_dat };`
325	2	dgisselq	`end`
326	4	dgisselq	end else if (state == `QSPI_HOLDING)
327			`begin`
328			`// We need this state so that the o_valid signal`
329			`// can get strobed with our last result. Otherwise`
330			`// we could just sit in READY waiting for a new command.`
331			`//`
332			`// Incidentally, the change producing this state was`
333			`// the result of a nasty race condition. See the`
334			`// commends in wbqspiflash for more details.`
335			`//`
336			`o_valid <= 1'b0;`
337			`o_cs_n <= 1'b0;`
338			`o_busy <= 1'b0;`
339	19	dgisselq	`r_spd <= i_spd;`
340			`r_dir <= i_dir;`
341			`if (i_spd)`
342	4	dgisselq	`begin`
343	19	dgisselq	`r_word <= { i_word[27:0], 4'h0 };`
344			`spi_len<= { 1'b0, i_len, 3'b100 };`
345			`end else begin`
346			`r_word <= { i_word[30:0], 1'b0 };`
347			`spi_len<= { 1'b0, i_len, 3'b111 };`
348			`end`
349			`if((!o_busy)&&(i_wr))// Acknowledge a new request`
350			`begin`
351	4	dgisselq	state <= `QSPI_BITS;
352			`o_busy <= 1'b1;`
353			`o_sck <= 1'b0;`
354
355			`// Read the new request off the bus`
356			`// Set up the first bits on the bus`
357			o_mod<=(i_spd)?{ 1'b1, i_dir } : `QSPI_MOD_SPI;
358			`if (i_spd)`
359			`o_dat <= i_word[31:28];`
360	19	dgisselq	`else`
361	4	dgisselq	`o_dat <= { 3'b110, i_word[31] };`
362			`end else begin`
363			`o_sck <= 1'b1;`
364			state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
365	19	dgisselq	`o_busy <= (!i_hold);`
366	4	dgisselq	`end`
367	2	dgisselq	end else if (state == `QSPI_STOP)
368			`begin`
369			`o_sck <= 1'b1; // Stop the clock`
370			`o_valid <= 1'b0; // Output may have just been valid, but no more`
371			`o_busy <= 1'b1; // Still busy till port is clear`
372			state <= `QSPI_STOP_B;
373			o_mod <= `QSPI_MOD_SPI;
374			end else if (state == `QSPI_STOP_B)
375			`begin`
376			`o_cs_n <= 1'b1;`
377			`o_sck <= 1'b1;`
378			`// Do I need this????`
379			`// spi_len <= 3; // Minimum CS high time before next cmd`
380			state <= `QSPI_IDLE;
381			`o_valid <= 1'b0;`
382			`o_busy <= 1'b1;`
383			o_mod <= `QSPI_MOD_SPI;
384			`end else begin // Invalid states, should never get here`
385			state <= `QSPI_STOP;
386			`o_valid <= 1'b0;`
387			`o_busy <= 1'b1;`
388			`o_cs_n <= 1'b1;`
389			`o_sck <= 1'b1;`
390			o_mod <= `QSPI_MOD_SPI;
391			`o_dat <= 4'hd;`
392			`end`
393
394	19	dgisselq	`ifdef FORMAL
395			`reg prev_i_clk, past_valid;`
396
397			initial `ASSUME(i_clk == 1'b0);
398			`initial prev_i_clk = 1;`
399			`always @($global_clock)`
400			`begin`
401			`prev_i_clk <= i_clk;`
402			`ASSUME(i_clk != prev_i_clk);
403			`end`
404
405			`reg past_valid;`
406			`initial past_valid = 1'b0;`
407			`always @(posedge i_clk)`
408			`past_valid <= 1'b1;`
409
410			`/*`
411			`always @(*)`
412			`if (!$stable(i_spd))`
413			`assert($rose(i_clk));`
414			`*/`
415
416			`always @(posedge i_clk) begin`
417			`if ((past_valid)&&($past(i_wr))&&($past(o_busy)))`
418			`begin`
419			`// any time i_wr and o_busy are true, nothing changes`
420			`// of spd, len, word or dir`
421			`ASSUME(i_wr);
422			`ASSUME(i_spd == $past(i_spd));
423			`ASSUME(i_len == $past(i_len));
424			`ASSUME(i_word == $past(i_word));
425			`ASSUME(i_dir == $past(i_dir));
426			`ASSUME(i_hold == $past(i_hold));
427			`end`
428			if ((past_valid)&&($past(i_wr))&&($past(o_busy))&&($past(state == `QSPI_IDLE)))
429			`assert($past(state)==state);`
430			`if (i_hold == $past(i_hold))`
431			`assert($stable(i_hold));`
432			`end`
433
434			`always @(*) begin`
435			if (o_mod == `QSPI_MOD_QOUT)
436			`ASSUME(i_dat == o_dat);
437			if (o_mod == `QSPI_MOD_SPI)
438			`ASSUME(i_dat[3:2] == 2'b11);
439			if (o_mod == `QSPI_MOD_SPI)
440			`ASSUME(i_dat[0] == o_dat[0]);
441			`end`
442
443			initial `ASSUME(i_wr == 1'b0);
444			initial `ASSUME(i_word == 0);
445
446			`always @($global_clock)`
447			`if (!$rose(i_clk))`
448			`begin`
449			`ASSUME($stable(i_wr));
450			`//`
451			`ASSUME($stable(i_len));
452			`ASSUME($stable(i_dir));
453			`ASSUME($stable(i_spd));
454			`ASSUME($stable(i_word));
455			`//`
456			`ASSUME($stable(i_hold));
457			`end`
458
459			`always @($global_clock)`
460			`if (!$fell(o_sck))`
461			`assume($stable(i_dat));`
462
463			`// This is ... not as believable. There might be a delay here.`
464			`// For now, we'll just assume (not necessarily true) that the`
465			`// output`
466			`always @(posedge i_clk)`
467			`if (past_valid)`
468			`ASSUME( (i_dat == $past(i_dat)) \|\| (o_sck != $past(o_sck)) );
469
470			`reg f_last_sck;`
471			`always @(posedge i_clk)`
472			`f_last_sck <= o_sck;`
473
474			`reg [31:0] f_shiftreg, f_goal;`
475			`initial f_shiftreg = 0;`
476			`initial f_goal = 0;`
477			`always @(posedge i_clk)`
478			`if ((o_sck)&&(!f_last_sck))`
479			`begin`
480			if (o_mod == `QSPI_MOD_QOUT)
481			`f_shiftreg <= { f_shiftreg[28:0], o_dat };`
482			else if (o_mod == `QSPI_MOD_SPI)
483			`f_shiftreg <= { f_shiftreg[30:0], o_dat[0] };`
484			`end`
485
486			`reg [5:0] f_nsent, f_vsent;`
487			`reg [2:0] f_nbits_r;`
488			`wire [5:0] f_nbits;`
489			`always @(posedge i_clk)`
490			`if ((i_wr)&&(!o_busy))`
491			`begin`
492			`f_goal <= i_word;`
493			`f_nbits_r <= { 1'b0, i_len } + 3'h1;`
494			`end`
495			`assign f_nbits = { f_nbits_r, 3'b000 };`
496			`always @(posedge i_clk)`
497			`if ((!o_sck)\|\|(!o_cs_n))`
498			`assert(f_nbits != 0);`
499
500			`always @(posedge i_clk)`

Browse

Tools

Subversion Repositories qspiflash

[/] [qspiflash/] [trunk/] [rtl/] [llqspi.v] - Blame information for rev 19