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

Subversion Repositories qspiflash

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

Details | Compare with Previous | View Log

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

powered by: WebSVN 2.1.0

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