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

Subversion Repositories qspiflash

[/] [qspiflash/] [trunk/] [rtl/] [llqspi.v] - Diff between revs 19 and 23

Only display areas with differences | Details | Blame | View Log

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

powered by: WebSVN 2.1.0

© copyright 1999-2019 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.