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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [core/] [dcache.v] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    dcache.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     To provide a simple data cache for the ZipCPU.  The cache is
8
//              designed to be a drop in replacement for the pipememm memory
9
//      unit currently existing within the ZipCPU.  The goal of this unit is
10
//      to achieve single cycle read access to any memory in the last cache line
11
//      used, or two cycle access to any memory currently in the cache.
12
//
13
//      The cache separates between four types of accesses, one write and three
14
//      read access types.  The read accesses are split between those that are
15
//      not cacheable, those that are in the cache, and those that are not.
16
//
17
//      1. Write accesses always create writes to the bus.  For these reasons,
18
//              these may always be considered cache misses.
19
//
20
//              Writes to memory locations within the cache must also update
21
//              cache memory immediately, to keep the cache in synch.
22
//
23
//              It is our goal to be able to maintain single cycle write
24
//              accesses for memory bursts.
25
//
26
//      2. Read access to non-cacheable memory locations will also immediately
27
//              go to the bus, just as all write accesses go to the bus.
28
//
29
//      3. Read accesses to cacheable memory locations will immediately read
30
//              from the appropriate cache line.  However, since thee valid
31
//              line will take a second clock to read, it may take up to two
32
//              clocks to know if the memory was in cache.  For this reason,
33
//              we bypass the test for the last validly accessed cache line.
34
//
35
//              We shall design these read accesses so that reads to the cache
36
//              may take place concurrently with other writes to the bus.
37
//
38
//      Errors in cache reads will void the entire cache line.  For this reason,
39
//      cache lines must always be of a smaller in size than any associated
40
//      virtual page size--lest in the middle of reading a page a TLB miss
41
//      take place referencing only a part of the cacheable page.
42
//
43
//
44
//
45 209 dgisselq
//
46 201 dgisselq
// Creator:     Dan Gisselquist, Ph.D.
47
//              Gisselquist Technology, LLC
48
//
49
////////////////////////////////////////////////////////////////////////////////
50
//
51 209 dgisselq
// Copyright (C) 2016-2019, Gisselquist Technology, LLC
52 201 dgisselq
//
53
// This program is free software (firmware): you can redistribute it and/or
54
// modify it under the terms of  the GNU General Public License as published
55
// by the Free Software Foundation, either version 3 of the License, or (at
56
// your option) any later version.
57
//
58
// This program is distributed in the hope that it will be useful, but WITHOUT
59
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
60
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
61
// for more details.
62
//
63
// License:     GPL, v3, as defined and found on www.gnu.org,
64
//              http://www.gnu.org/licenses/gpl.html
65
//
66
//
67
////////////////////////////////////////////////////////////////////////////////
68
//
69
//
70 209 dgisselq
`default_nettype        none
71
//
72
//
73
`ifdef  FORMAL
74
`define ASSERT  assert
75
 
76
`ifdef DCACHE
77
`define ASSUME  assume
78
`else
79
`define ASSUME  assert
80
`endif
81
`endif
82
 
83
module  dcache(i_clk, i_reset, i_pipe_stb, i_lock,
84 201 dgisselq
                i_op, i_addr, i_data, i_oreg,
85
                        o_busy, o_pipe_stalled, o_valid, o_err, o_wreg,o_data,
86
                o_wb_cyc_gbl, o_wb_cyc_lcl, o_wb_stb_gbl, o_wb_stb_lcl,
87 209 dgisselq
                        o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
88
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data
89
`ifdef  FORMAL
90
                , f_nreqs, f_nacks, f_outstanding, f_pc
91
`endif
92
        );
93 201 dgisselq
        parameter       LGCACHELEN = 8,
94 209 dgisselq
                        ADDRESS_WIDTH=30,
95
                        LGNLINES=(LGCACHELEN-3), // Log of the number of separate cache lines
96 201 dgisselq
                        NAUX=5; // # of aux d-wires to keep aligned w/memops
97 209 dgisselq
        parameter [0:0]   OPT_LOCAL_BUS=1'b1;
98
        parameter [0:0]   OPT_PIPE=1'b1;
99
        parameter [0:0]   OPT_LOCK=1'b1;
100
        parameter [0:0]   OPT_DUAL_READ_PORT=1'b1;
101
        parameter       OPT_FIFO_DEPTH = 4;
102 201 dgisselq
        localparam      AW = ADDRESS_WIDTH; // Just for ease of notation below
103
        localparam      CS = LGCACHELEN; // Number of bits in a cache address
104
        localparam      LS = CS-LGNLINES; // Bits to spec position w/in cline
105 209 dgisselq
        parameter       F_LGDEPTH=1 + (((!OPT_PIPE)||(LS > OPT_FIFO_DEPTH))
106
                                        ? LS : OPT_FIFO_DEPTH);
107
        localparam      LGAUX = 3; // log_2 of the maximum number of piped data
108
        localparam      DW = 32; // Bus data width
109
        localparam      DP = OPT_FIFO_DEPTH;
110
        //
111
        localparam [1:0] DC_IDLE  = 2'b00; // Bus is idle
112
        localparam [1:0] DC_WRITE = 2'b01; // Write
113
        localparam [1:0] DC_READS = 2'b10; // Read a single value(!cachd)
114
        localparam [1:0] DC_READC = 2'b11; // Read a whole cache line
115
        //
116
        input   wire            i_clk, i_reset;
117 201 dgisselq
        // Interface from the CPU
118 209 dgisselq
        input   wire            i_pipe_stb, i_lock;
119
        input   wire [2:0]               i_op;
120
        input   wire [(DW-1):0]  i_addr;
121
        input   wire [(DW-1):0]  i_data;
122
        input   wire [(NAUX-1):0] i_oreg; // Aux data, such as reg to write to
123 201 dgisselq
        // Outputs, going back to the CPU
124 209 dgisselq
        output  reg             o_busy;
125
        output  reg             o_pipe_stalled;
126
        output  reg             o_valid, o_err;
127 201 dgisselq
        output reg [(NAUX-1):0]  o_wreg;
128 209 dgisselq
        output  reg [(DW-1):0]   o_data;
129 201 dgisselq
        // Wishbone bus master outputs
130
        output  wire            o_wb_cyc_gbl, o_wb_cyc_lcl;
131
        output  reg             o_wb_stb_gbl, o_wb_stb_lcl;
132
        output  reg             o_wb_we;
133 209 dgisselq
        output  reg [(AW-1):0]   o_wb_addr;
134
        output  reg [(DW-1):0]   o_wb_data;
135
        output  wire [(DW/8-1):0] o_wb_sel;
136 201 dgisselq
        // Wishbone bus slave response inputs
137 209 dgisselq
        input   wire                    i_wb_ack, i_wb_stall, i_wb_err;
138
        input   wire    [(DW-1):0]       i_wb_data;
139
`ifdef FORMAL
140
        output  wire [(F_LGDEPTH-1):0]   f_nreqs, f_nacks, f_outstanding;
141
        output  wire                    f_pc;
142 201 dgisselq
 
143 209 dgisselq
        reg     f_past_valid;
144
`endif
145
        //
146
        // output       reg     [31:0]          o_debug;
147 201 dgisselq
 
148 209 dgisselq
 
149 201 dgisselq
        reg     cyc, stb, last_ack, end_of_line, last_line_stb;
150 209 dgisselq
        reg     r_wb_cyc_gbl, r_wb_cyc_lcl;
151
        // npending is the number of pending non-cached operations, counted
152
        // from the i_pipe_stb to the o_wb_ack
153
        reg     [DP:0]   npending;
154 201 dgisselq
 
155
 
156
        reg     [((1<<LGNLINES)-1):0] c_v;       // One bit per cache line, is it valid?
157
        reg     [(AW-LS-1):0]    c_vtags [0:((1<<LGNLINES)-1)];
158 209 dgisselq
        reg     [(DW-1):0]       c_mem   [0:((1<<CS)-1)];
159
        reg                     set_vflag;
160
        reg     [1:0]            state;
161
        reg     [(CS-1):0]       wr_addr;
162
        reg     [(DW-1):0]       cached_idata, cached_rdata;
163
        reg     [DW-1:0] pre_data;
164
        reg                     lock_gbl, lock_lcl;
165 201 dgisselq
 
166 209 dgisselq
 
167 201 dgisselq
        // To simplify writing to the cache, and the job of the synthesizer to
168
        // recognize that a cache write needs to take place, we'll take an extra
169
        // clock to get there, and use these c_w... registers to capture the
170
        // data in the meantime.
171
        reg                     c_wr;
172 209 dgisselq
        reg     [(DW-1):0]       c_wdata;
173
        reg     [(DW/8-1):0]     c_wsel;
174 201 dgisselq
        reg     [(CS-1):0]       c_waddr;
175
 
176
        reg     [(AW-LS-1):0]    last_tag;
177 209 dgisselq
        reg                     last_tag_valid;
178 201 dgisselq
 
179
 
180
        wire    [(LGNLINES-1):0] i_cline;
181
        wire    [(CS-1):0]       i_caddr;
182
 
183 209 dgisselq
`ifdef  FORMAL
184
        reg     [F_LGDEPTH-1:0]  f_fill;
185
        reg     [AW:0]           f_return_address;
186
        reg     [AW:0]           f_pending_addr;
187
`endif
188 201 dgisselq
 
189 209 dgisselq
        assign  i_cline = i_addr[(CS+1):LS+2];
190
        assign  i_caddr = i_addr[(CS+1):2];
191
 
192 201 dgisselq
        wire    cache_miss_inow, w_cachable;
193 209 dgisselq
        assign  cache_miss_inow = (!last_tag_valid)
194
                                        ||(last_tag != i_addr[(AW+1):LS+2])
195
                                        ||(!c_v[i_cline]);
196 201 dgisselq
 
197 209 dgisselq
        wire    raw_cachable_address;
198
 
199
        iscachable chkaddress(i_addr[AW+1:2], raw_cachable_address);
200
 
201
        assign  w_cachable = ((!OPT_LOCAL_BUS)||(i_addr[(DW-1):(DW-8)]!=8'hff))
202
                &&((!i_lock)||(!OPT_LOCK))&&(raw_cachable_address);
203
 
204
        reg     r_cachable, r_svalid, r_dvalid, r_rd, r_cache_miss,
205
                r_rd_pending;
206
        reg     [(AW-1):0]               r_addr;
207 201 dgisselq
        wire    [(LGNLINES-1):0] r_cline;
208 209 dgisselq
        wire    [(CS-1):0]               r_caddr;
209
        wire    [(AW-LS-1):0]            r_ctag;
210 201 dgisselq
 
211
        assign  r_cline = r_addr[(CS-1):LS];
212
        assign  r_caddr = r_addr[(CS-1):0];
213
        assign  r_ctag  = r_addr[(AW-1):LS];
214
 
215
 
216 209 dgisselq
        reg     wr_cstb, r_iv, in_cache;
217 201 dgisselq
        reg     [(AW-LS-1):0]    r_itag;
218 209 dgisselq
        reg     [DW/8-1:0]       r_sel;
219
        reg     [(NAUX+4-1):0]   req_data;
220
        reg                     gie;
221 201 dgisselq
 
222 209 dgisselq
 
223
 
224 201 dgisselq
        //
225
        // The one-clock delayed read values from the cache.
226
        //
227
        initial r_rd = 1'b0;
228
        initial r_cachable = 1'b0;
229
        initial r_svalid = 1'b0;
230
        initial r_dvalid = 1'b0;
231 209 dgisselq
        initial r_cache_miss = 1'b0;
232
        initial r_addr = 0;
233
        initial last_tag_valid = 0;
234
        initial r_rd_pending = 0;
235 201 dgisselq
        always @(posedge i_clk)
236 209 dgisselq
        if (i_reset)
237 201 dgisselq
        begin
238 209 dgisselq
                r_rd <= 1'b0;
239
                r_cachable <= 1'b0;
240
                r_svalid <= 1'b0;
241
                r_dvalid <= 1'b0;
242
                r_cache_miss <= 1'b0;
243
                r_addr <= 0;
244
                r_rd_pending <= 0;
245
                last_tag_valid <= 0;
246
        end else begin
247 201 dgisselq
                // The single clock path
248
                // The valid for the single clock path
249
                //      Only ... we need to wait if we are currently writing
250
                //      to our cache.
251 209 dgisselq
                r_svalid<= (i_pipe_stb)&&(!i_op[0])&&(w_cachable)
252
                                &&(!cache_miss_inow)&&(!c_wr)&&(!wr_cstb);
253 201 dgisselq
 
254
                //
255
                // The two clock in-cache path
256
                //
257
                // Some preliminaries that needed to be calculated on the first
258
                // clock
259 209 dgisselq
                if ((!o_pipe_stalled)&&(!r_rd_pending))
260
                        r_addr <= i_addr[(AW+1):2];
261
                if ((!o_pipe_stalled)&&(!r_rd_pending))
262 201 dgisselq
                begin
263
                        r_iv   <= c_v[i_cline];
264
                        r_itag <= c_vtags[i_cline];
265 209 dgisselq
                        r_cachable <= (!i_op[0])&&(w_cachable)&&(i_pipe_stb);
266
                        r_rd_pending <= (i_pipe_stb)&&(!i_op[0])&&(w_cachable)
267
                                &&((cache_miss_inow)||(c_wr)||(wr_cstb));
268
                                // &&((!c_wr)||(!wr_cstb));
269 201 dgisselq
                end else begin
270
                        r_iv   <= c_v[r_cline];
271
                        r_itag <= c_vtags[r_cline];
272 209 dgisselq
                        r_rd_pending <= (r_rd_pending)
273
                                &&((!cyc)||(!i_wb_err))
274
                                &&((r_itag != r_ctag)||(!r_iv));
275 201 dgisselq
                end
276 209 dgisselq
                r_rd <= (i_pipe_stb)&&(!i_op[0]);
277 201 dgisselq
                // r_itag contains the tag we didn't have available to us on the
278
                // last clock, r_ctag is a bit select from r_addr containing a
279
                // one clock delayed address.
280 209 dgisselq
                r_dvalid <= (!r_svalid)&&(!r_dvalid)&&(r_itag == r_ctag)&&(r_iv)
281
                                                &&(r_cachable)&&(r_rd_pending);
282
                if ((r_itag == r_ctag)&&(r_iv)&&(r_cachable)&&(r_rd_pending))
283
                begin
284
                        last_tag_valid <= 1'b1;
285 201 dgisselq
                        last_tag <= r_ctag;
286 209 dgisselq
                end else if ((state == DC_READC)
287
                                &&(last_tag[CS-LS-1:0]==o_wb_addr[CS-1:LS])
288
                                &&((i_wb_ack)||(i_wb_err)))
289
                        last_tag_valid <= 1'b0;
290 201 dgisselq
 
291
                // r_cache miss takes a clock cycle.  It is only ever true for
292
                // something that should be cachable, but isn't in the cache.
293
                // A cache miss is only true _if_
294
                // 1. A read was requested
295
                // 2. It is for a cachable address, AND
296
                // 3. It isn't in the cache on the first read
297
                //      or the second read
298
                // 4. The read hasn't yet started to get this address
299
                r_cache_miss <= ((!cyc)||(o_wb_we))&&(r_cachable)
300
                                // One clock path -- miss
301
                                &&(!r_svalid)
302
                                // Two clock path -- misses as well
303
                                &&(r_rd)&&(!r_svalid)
304
                                &&((r_itag != r_ctag)||(!r_iv));
305 209 dgisselq
        end
306 201 dgisselq
 
307 209 dgisselq
        initial r_sel = 4'hf;
308
        always @(posedge i_clk)
309
        if (i_reset)
310
                r_sel <= 4'hf;
311
        else if (!o_pipe_stalled)
312
        begin
313
                casez({i_op[2:1], i_addr[1:0]})
314
                4'b0???: r_sel <= 4'b1111;
315
                4'b100?: r_sel <= 4'b1100;
316
                4'b101?: r_sel <= 4'b0011;
317
                4'b1100: r_sel <= 4'b1000;
318
                4'b1101: r_sel <= 4'b0100;
319
                4'b1110: r_sel <= 4'b0010;
320
                4'b1111: r_sel <= 4'b0001;
321
                endcase
322 201 dgisselq
        end
323
 
324 209 dgisselq
        assign  o_wb_sel = (state == DC_READC) ? 4'hf : r_sel;
325 201 dgisselq
 
326 209 dgisselq
        initial o_wb_data = 0;
327 201 dgisselq
        always @(posedge i_clk)
328 209 dgisselq
        if (i_reset)
329
                o_wb_data <= 0;
330
        else if ((!o_busy)||((stb)&&(!i_wb_stall)))
331 201 dgisselq
        begin
332 209 dgisselq
                casez(i_op[2:1])
333
                2'b0?: o_wb_data <= i_data;
334
                2'b10: o_wb_data <= { (2){i_data[15:0]} };
335
                2'b11: o_wb_data <= { (4){i_data[ 7:0]} };
336
                endcase
337
        end
338
 
339
        generate if (OPT_PIPE)
340
        begin : OPT_PIPE_FIFO
341
                reg     [NAUX+4-2:0]     fifo_data [0:((1<<OPT_FIFO_DEPTH)-1)];
342
 
343
                reg     [DP:0]           wraddr, rdaddr;
344
 
345
                always @(posedge i_clk)
346
                if (i_pipe_stb)
347
                        fifo_data[wraddr[DP-1:0]]
348
                                <= { i_oreg[NAUX-2:0], i_op[2:1], i_addr[1:0] };
349
 
350
                always @(posedge i_clk)
351
                if (i_pipe_stb)
352
                        gie <= i_oreg[NAUX-1];
353
 
354
`ifdef  NO_BKRAM
355
                reg     [NAUX+4-2:0]     r_req_data, r_last_data;
356
                reg                     single_write;
357
 
358
                always @(posedge i_clk)
359
                        r_req_data <= fifo_data[rdaddr[DP-1:0]];
360
 
361
                always @(posedge i_clk)
362
                        single_write <= (rdaddr == wraddr)&&(i_pipe_stb);
363
 
364
                always @(posedge i_clk)
365
                if (i_pipe_stb)
366
                        r_last_data <= { i_oreg[NAUX-2:0],
367
                                                i_op[2:1], i_addr[1:0] };
368
 
369
                always @(*)
370
                begin
371
                        req_data[NAUX+4-1] = gie;
372
                        // if ((r_svalid)||(state == DC_READ))
373
                        if (single_write)
374
                                req_data[NAUX+4-2:0] = r_last_data;
375
                        else
376
                                req_data[NAUX+4-2:0] = r_req_data;
377
                end
378
 
379
                always @(*)
380
                        `ASSERT(req_data == fifo_data[rdaddr[DP-1:0]]);
381
`else
382
                always @(*)
383
                        req_data[NAUX+4-2:0] = fifo_data[rdaddr[DP-1:0]];
384
                always @(*)
385
                        req_data[NAUX+4-1] = gie;
386
`endif
387
 
388
                initial wraddr = 0;
389
                always @(posedge i_clk)
390
                if ((i_reset)||((cyc)&&(i_wb_err)))
391
                        wraddr <= 0;
392
                else if (i_pipe_stb)
393
                        wraddr <= wraddr + 1'b1;
394
 
395
                initial rdaddr = 0;
396
                always @(posedge i_clk)
397
                if ((i_reset)||((cyc)&&(i_wb_err)))
398
                        rdaddr <= 0;
399
                else if ((r_dvalid)||(r_svalid))
400
                        rdaddr <= rdaddr + 1'b1;
401
                else if ((state == DC_WRITE)&&(i_wb_ack))
402
                        rdaddr <= rdaddr + 1'b1;
403
                else if ((state == DC_READS)&&(i_wb_ack))
404
                        rdaddr <= rdaddr + 1'b1;
405
 
406
`ifdef  FORMAL
407
                reg     [AW-1:0] f_fifo_addr [0:((1<<OPT_FIFO_DEPTH)-1)];
408
                reg     [F_LGDEPTH-1:0]  f_last_wraddr;
409
                reg     f_pc_pending;
410
 
411
                always @(*)
412
                begin
413
                        f_fill = 0;
414
                        f_fill[DP:0] = wraddr - rdaddr;
415
                end
416
 
417
                always @(*)
418
                        `ASSERT(f_fill <= { 1'b1, {(DP){1'b0}} });
419
 
420
                always @(*)
421
                if ((r_dvalid)||(r_svalid))
422
                begin
423
                        if (r_svalid)
424
                                `ASSERT(f_fill == 1);
425
                        else if (r_dvalid)
426
                                `ASSERT(f_fill == 1);
427
                        else
428
                                `ASSERT(f_fill == 0);
429
                end else if (r_rd_pending)
430
                        `ASSERT(f_fill == 1);
431
                else
432
                        `ASSERT(f_fill == npending);
433
 
434
 
435
                initial f_pc_pending = 0;
436
                always @(posedge i_clk)
437
                if (i_reset)
438
                        f_pc_pending <= 1'b0;
439
                else if (i_pipe_stb)
440
                        f_pc_pending <= (!i_op[0])&&(i_oreg[3:1] == 3'h7);
441
                else if (f_fill == 0)
442
                        f_pc_pending <= 1'b0;
443
                //else if ((o_valid)&&(o_wreg[3:1] == 3'h7)&&(f_fill == 0))
444
                //      f_pc_pending <= 1'b0;
445
 
446
                always @(posedge i_clk)
447
                if (f_pc_pending)
448
                        `ASSUME(!i_pipe_stb);
449
 
450
                always @(posedge i_clk)
451
                if (state == DC_WRITE)
452
                        `ASSERT(!f_pc_pending);
453
 
454
                always @(*)
455
                begin
456
                        f_last_wraddr = 0;
457
                        f_last_wraddr[DP:0] = wraddr - 1'b1;
458
                end
459
 
460
                always @(posedge i_clk)
461
                if (r_rd_pending)
462
                        `ASSERT(f_pc_pending == (fifo_data[f_last_wraddr][7:5] == 3'h7));
463
 
464
`define INSPECT_FIFO
465
                reg     [((1<<(DP+1))-1):0]      f_valid_fifo_entry;
466
 
467
                genvar  k;
468
                for(k=0; k<(1<<(DP+1)); k=k+1)
469
                begin
470
 
471
                        always @(*)
472
                        begin
473
                        f_valid_fifo_entry[k] = 1'b0;
474
                        /*
475
                        if ((rdaddr[DP] != wraddr[DP])
476
                                        &&(rdaddr[DP-1:0] == wraddr[DP-1:0]))
477
                                f_valid_fifo_entry[k] = 1'b1;
478
                        else */
479
                        if ((rdaddr < wraddr)&&(k < wraddr)
480
                                        &&(k >= rdaddr))
481
                                f_valid_fifo_entry[k] = 1'b1;
482
                        else if ((rdaddr > wraddr)&&(k >= rdaddr))
483
                                f_valid_fifo_entry[k] = 1'b1;
484
                        else if ((rdaddr > wraddr)&&(k <  wraddr))
485
                                f_valid_fifo_entry[k] = 1'b1;
486
                        end
487
 
488
`ifdef  INSPECT_FIFO
489
                        wire    [NAUX+4-2:0]     fifo_data_k;
490
 
491
                        assign  fifo_data_k = fifo_data[k[DP-1:0]];
492
                        always @(*)
493
                        if (f_valid_fifo_entry[k])
494
                        begin
495
                                if (!f_pc_pending)
496
                                        `ASSERT((o_wb_we)||(fifo_data_k[7:5] != 3'h7));
497
                                else if (k != f_last_wraddr)
498
                                        `ASSERT(fifo_data_k[7:5] != 3'h7);
499
                        end
500
`endif // INSPECT_FIFO
501
 
502
                end
503
 
504
`ifndef INSPECT_FIFO
505
                always @(posedge i_clk)
506
                if ((r_rd_pending)&&(rdaddr[DP:0] != f_last_wraddr[DP-1]))
507
                        assume(fifo_data[rdaddr][7:5] != 3'h7);
508
`endif // INSPECT_FIFO
509
 
510
                assign  f_pc = f_pc_pending;
511
 
512
                //
513
                //
514
                //
515
                always @(*)
516
                        f_pending_addr = f_fifo_addr[rdaddr];
517
 
518
                //
519
                //
520
                //
521
                always @(posedge i_clk)
522
                if (i_pipe_stb)
523
                        f_fifo_addr[wraddr[DP-1:0]] <= i_addr[AW+1:2];
524
 
525
                always @(*)
526
                begin
527
                        f_return_address[AW] = (o_wb_cyc_lcl);
528
                        f_return_address[AW-1:0] = f_fifo_addr[rdaddr];
529
                        if (state == DC_READC)
530
                                f_return_address[LS-1:0]
531
                                = (o_wb_addr[LS-1:0] - f_outstanding[LS-1:0]);
532
                end
533
 
534
`define TWIN_WRITE_TEST
535
`ifdef  TWIN_WRITE_TEST
536
                (* anyconst *)  reg     [DP:0]           f_twin_base;
537
                                reg     [DP:0]           f_twin_next;
538
                (* anyconst *)  reg     [AW+NAUX+4-2-1:0]        f_twin_first,
539
                                                        f_twin_second;
540
                // reg  [AW-1:0]        f_fifo_addr [0:((1<<OPT_FIFO_DEPTH)-1)];
541
                // reg  [NAUX+4-2:0]    fifo_data [0:((1<<OPT_FIFO_DEPTH)-1)];
542
 
543
                always @(*)     f_twin_next = f_twin_base+1;
544
 
545
                reg     f_twin_none, f_twin_single, f_twin_double, f_twin_last;
546
                reg     f_twin_valid_one, f_twin_valid_two;
547
                always @(*)
548
                begin
549
                        f_twin_valid_one = ((f_valid_fifo_entry[f_twin_base])
550
                                &&(f_twin_first == { f_fifo_addr[f_twin_base],
551
                                                fifo_data[f_twin_base] }));
552
                        f_twin_valid_two = ((f_valid_fifo_entry[f_twin_next])
553
                                &&(f_twin_second == { f_fifo_addr[f_twin_next],
554
                                                fifo_data[f_twin_next] }));
555
                end
556
 
557
                always @(*)
558
                begin
559
                        f_twin_none   =(!f_twin_valid_one)&&(!f_twin_valid_two);
560
                        f_twin_single =( f_twin_valid_one)&&(!f_twin_valid_two);
561
                        f_twin_double =( f_twin_valid_one)&&( f_twin_valid_two);
562
                        f_twin_last   =(!f_twin_valid_one)&&( f_twin_valid_two);
563
                end
564
 
565
                always @(posedge i_clk)
566
                if ((!f_past_valid)||($past(i_reset))||($past(cyc && i_wb_err)))
567
                        `ASSERT(f_twin_none);
568
                else if ($past(f_twin_none))
569
                        `ASSERT(f_twin_none || f_twin_single || f_twin_last);
570
                else if ($past(f_twin_single))
571
                        `ASSERT(f_twin_none || f_twin_single || f_twin_double || f_twin_last);
572
                else if ($past(f_twin_double))
573
                        `ASSERT(f_twin_double || f_twin_last);
574
                else if ($past(f_twin_last))
575
                        `ASSERT(f_twin_none || f_twin_single || f_twin_last);
576
 
577
`endif // TWIN_WRITE_TEST
578
 
579
                always @(*)
580
                        `ASSERT(req_data == { gie, fifo_data[rdaddr[DP-1:0]] });
581
 
582
                always @(posedge i_clk)
583
                if (r_svalid||r_dvalid || r_rd_pending)
584
                        `ASSERT(f_fill == 1);
585
                else if (f_fill > 0)
586
                        `ASSERT(cyc);
587
 
588
                always @(posedge i_clk)
589
                if (state != 0)
590
                        `ASSERT(f_fill > 0);
591
                else if (!r_svalid && !r_dvalid && !r_rd_pending)
592
                        `ASSERT(f_fill == 0);
593
 
594
`endif // FORMAL
595
 
596
                always @(posedge i_clk)
597
                        o_wreg <= req_data[(NAUX+4-1):4];
598
 
599
                /*
600
                reg     fifo_err;
601
                always @(posedge i_clk)
602
                begin
603
                        fifo_err <= 1'b0;
604
                        if ((!o_busy)&&(rdaddr != wraddr))
605
                                fifo_err <= 1'b1;
606
                        if ((!r_dvalid)&&(!r_svalid)&&(!r_rd_pending))
607
                                fifo_err <= (npending != (wraddr-rdaddr));
608
                end
609
 
610
                always @(*)
611
                o_debug = { i_pipe_stb, state, cyc, stb,        //  5b
612
                                fifo_err, i_oreg[3:0], o_wreg,          // 10b
613
                                rdaddr, wraddr,                 // 10b
614
                                i_wb_ack, i_wb_err, o_pipe_stalled, o_busy,//4b
615
                                r_svalid, r_dvalid, r_rd_pending };
616
                */
617
        end else begin : NO_FIFO
618
 
619
                always @(posedge i_clk)
620
                if (i_pipe_stb)
621
                        req_data <= { i_oreg, i_op[2:1], i_addr[1:0] };
622
 
623
                always @(*)
624
                        o_wreg = req_data[(NAUX+4-1):4];
625
 
626
                always @(*)
627
                        gie = i_oreg[NAUX-1];
628
 
629
`ifdef  FORMAL
630
                assign  f_pc = ((r_rd_pending)||(o_valid))&&(o_wreg[3:1] == 3'h7);
631
 
632
                //
633
                //
634
                //
635
                initial f_pending_addr = 0;
636
                always @(posedge i_clk)
637
                if (i_reset)
638
                        f_pending_addr <= 0;
639
                else if (i_pipe_stb)
640
                begin
641
                        f_pending_addr <= { (OPT_LOCAL_BUS)&&(&i_addr[DW-1:DW-8]),
642
                                                i_addr[(AW+1):2] };
643
                end
644
 
645
                //
646
                //
647
                always @(*)
648
                begin
649
                        f_return_address[AW]      = o_wb_cyc_lcl;
650
                        f_return_address[AW-1:LS] = o_wb_addr[AW-1:LS];
651
                end
652
                always @(*)
653
                if (state == DC_READS)
654
                        f_return_address[LS-1:0] = o_wb_addr[LS-1:0];
655
                else
656
                        f_return_address[LS-1:0]
657
                                = (o_wb_addr[LS-1:0] - f_outstanding[LS-1:0]);
658
 
659
`endif
660
                /*
661
                always @(*)
662
                o_debug = { i_pipe_stb, state, cyc, stb,        //  5b
663
                                i_oreg, o_wreg,                 // 10b
664
                                10'hb,                          // 10b
665
                                i_wb_ack, i_wb_err, o_pipe_stalled, o_busy,//4b
666
                                r_svalid, r_dvalid, r_rd_pending };
667
                */
668
 
669
                // verilator lint_off UNUSED
670
                wire    unused_no_fifo;
671
                assign  unused_no_fifo = gie;
672
                // verilator lint_on  UNUSED
673
        end endgenerate
674
 
675
 
676
        initial r_wb_cyc_gbl = 0;
677
        initial r_wb_cyc_lcl = 0;
678
        initial o_wb_stb_gbl = 0;
679
        initial o_wb_stb_lcl = 0;
680
        initial c_v = 0;
681
        initial cyc = 0;
682
        initial stb = 0;
683
        initial c_wr = 0;
684
        initial wr_cstb = 0;
685
        initial state = DC_IDLE;
686
        initial set_vflag = 1'b0;
687
        always @(posedge i_clk)
688
        if (i_reset)
689
        begin
690
                c_v <= 0;
691
                c_wr   <= 1'b0;
692
                c_wsel <= 4'hf;
693
                r_wb_cyc_gbl <= 1'b0;
694
                r_wb_cyc_lcl <= 1'b0;
695
                o_wb_stb_gbl <= 0;
696
                o_wb_stb_lcl <= 0;
697
                wr_cstb <= 1'b0;
698
                last_line_stb <= 1'b0;
699
                end_of_line <= 1'b0;
700
                state <= DC_IDLE;
701
                cyc <= 1'b0;
702
                stb <= 1'b0;
703
                state <= DC_IDLE;
704
                set_vflag <= 1'b0;
705
        end else begin
706 201 dgisselq
                // By default, update the cache from the write 1-clock ago
707 209 dgisselq
                // c_wr <= (wr_cstb)&&(wr_wtag == wr_vtag);
708
                // c_waddr <= wr_addr[(CS-1):0];
709
                c_wr <= 0;
710 201 dgisselq
 
711 209 dgisselq
                set_vflag <= 1'b0;
712
                if ((!cyc)&&(set_vflag))
713
                        c_v[c_waddr[(CS-1):LS]] <= 1'b1;
714
 
715 201 dgisselq
                wr_cstb <= 1'b0;
716
 
717 209 dgisselq
                if (!cyc)
718
                        wr_addr <= r_addr[(CS-1):0];
719
                else if (i_wb_ack)
720
                        wr_addr <= wr_addr + 1'b1;
721
                else
722
                        wr_addr <= wr_addr;
723 201 dgisselq
 
724 209 dgisselq
                if (LS <= 0)
725 201 dgisselq
                        end_of_line <= 1'b1;
726 209 dgisselq
                else if (!cyc)
727
                        end_of_line <= 1'b0;
728
                else if (!end_of_line)
729
                begin
730
                        if (i_wb_ack)
731
                                end_of_line
732
                                <= (c_waddr[(LS-1):0] == {{(LS-2){1'b1}},2'b01});
733
                        else
734
                                end_of_line
735
                                <= (c_waddr[(LS-1):0]=={{(LS-1){1'b1}}, 1'b0});
736
                end
737 201 dgisselq
 
738 209 dgisselq
                if (!cyc)
739
                        last_line_stb <= (LS <= 0);
740
                else if ((stb)&&(!i_wb_stall)&&(LS <= 1))
741 201 dgisselq
                        last_line_stb <= 1'b1;
742 209 dgisselq
                else if ((stb)&&(!i_wb_stall))
743
                        last_line_stb <= (o_wb_addr[(LS-1):1]=={(LS-1){1'b1}});
744
                else if (stb)
745
                        last_line_stb <= (o_wb_addr[(LS-1):0]=={(LS){1'b1}});
746 201 dgisselq
 
747
                //
748 209 dgisselq
                //
749
                if (state == DC_IDLE)
750 201 dgisselq
                begin
751
                        o_wb_we <= 1'b0;
752
 
753
                        cyc <= 1'b0;
754
                        stb <= 1'b0;
755
 
756
                        r_wb_cyc_gbl <= 1'b0;
757
                        r_wb_cyc_lcl <= 1'b0;
758
                        o_wb_stb_gbl <= 1'b0;
759
                        o_wb_stb_lcl <= 1'b0;
760
 
761 209 dgisselq
                        in_cache <= (i_op[0])&&(w_cachable);
762
                        if ((i_pipe_stb)&&(i_op[0]))
763 201 dgisselq
                        begin // Write  operation
764 209 dgisselq
                                state <= DC_WRITE;
765
                                o_wb_addr <= i_addr[(AW+1):2];
766 201 dgisselq
                                o_wb_we <= 1'b1;
767
 
768
                                cyc <= 1'b1;
769
                                stb <= 1'b1;
770
 
771 209 dgisselq
                                if (OPT_LOCAL_BUS)
772
                                begin
773
                                r_wb_cyc_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
774
                                r_wb_cyc_lcl <= (i_addr[DW-1:DW-8]==8'hff);
775
                                o_wb_stb_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
776
                                o_wb_stb_lcl <= (i_addr[DW-1:DW-8]==8'hff);
777
                                end else begin
778
                                        r_wb_cyc_gbl <= 1'b1;
779
                                        o_wb_stb_gbl <= 1'b1;
780
                                end
781 201 dgisselq
 
782
                        end else if (r_cache_miss)
783
                        begin
784 209 dgisselq
                                state <= DC_READC;
785
                                o_wb_addr <= { r_ctag, {(LS){1'b0}} };
786 201 dgisselq
 
787 209 dgisselq
                                c_waddr <= { r_ctag[CS-LS-1:0], {(LS){1'b0}} }-1'b1;
788 201 dgisselq
                                cyc <= 1'b1;
789
                                stb <= 1'b1;
790
                                r_wb_cyc_gbl <= 1'b1;
791
                                o_wb_stb_gbl <= 1'b1;
792 209 dgisselq
                                wr_addr[LS-1:0] <= 0;
793 201 dgisselq
                        end else if ((i_pipe_stb)&&(!w_cachable))
794
                        begin // Read non-cachable memory area
795 209 dgisselq
                                state <= DC_READS;
796
                                o_wb_addr <= i_addr[(AW+1):2];
797 201 dgisselq
 
798
                                cyc <= 1'b1;
799
                                stb <= 1'b1;
800 209 dgisselq
                                if (OPT_LOCAL_BUS)
801
                                begin
802
                                r_wb_cyc_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
803
                                r_wb_cyc_lcl <= (i_addr[DW-1:DW-8]==8'hff);
804
                                o_wb_stb_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
805
                                o_wb_stb_lcl <= (i_addr[DW-1:DW-8]==8'hff);
806
                                end else begin
807
                                r_wb_cyc_gbl <= 1'b1;
808
                                o_wb_stb_gbl <= 1'b1;
809
                                end
810 201 dgisselq
                        end // else we stay idle
811
 
812 209 dgisselq
                end else if (state == DC_READC)
813 201 dgisselq
                begin
814
                        // We enter here once we have committed to reading
815
                        // data into a cache line.
816
                        if ((stb)&&(!i_wb_stall))
817
                        begin
818
                                stb <= (!last_line_stb);
819
                                o_wb_stb_gbl <= (!last_line_stb);
820
                                o_wb_addr[(LS-1):0] <= o_wb_addr[(LS-1):0]+1'b1;
821
                        end
822
 
823 209 dgisselq
                        if ((i_wb_ack)&&(!end_of_line))
824
                                c_v[o_wb_addr[(CS-1):LS]] <= 1'b0;
825 201 dgisselq
 
826 209 dgisselq
                        c_wr    <= (i_wb_ack);
827
                        c_wdata <= i_wb_data;
828
                        c_waddr <= ((i_wb_ack)?(c_waddr+1'b1):c_waddr);
829
                        c_wsel  <= 4'hf;
830 201 dgisselq
 
831 209 dgisselq
                        set_vflag <= !i_wb_err;
832
                        if (i_wb_ack)
833
                                c_vtags[r_addr[(CS-1):LS]]
834
                                                <= r_addr[(AW-1):LS];
835 201 dgisselq
 
836
                        if (((i_wb_ack)&&(end_of_line))||(i_wb_err))
837
                        begin
838 209 dgisselq
                                state          <= DC_IDLE;
839 201 dgisselq
                                cyc <= 1'b0;
840 209 dgisselq
                                stb <= 1'b0;
841 201 dgisselq
                                r_wb_cyc_gbl <= 1'b0;
842
                                r_wb_cyc_lcl <= 1'b0;
843 209 dgisselq
                                o_wb_stb_gbl <= 1'b0;
844
                                o_wb_stb_lcl <= 1'b0;
845 201 dgisselq
                                //
846
                        end
847 209 dgisselq
                end else if (state == DC_READS)
848 201 dgisselq
                begin
849
                        // We enter here once we have committed to reading
850
                        // data that cannot go into a cache line
851
                        if ((!i_wb_stall)&&(!i_pipe_stb))
852
                        begin
853
                                stb <= 1'b0;
854
                                o_wb_stb_gbl <= 1'b0;
855
                                o_wb_stb_lcl <= 1'b0;
856
                        end
857
 
858
                        if ((!i_wb_stall)&&(i_pipe_stb))
859 209 dgisselq
                                o_wb_addr <= i_addr[(AW+1):2];
860 201 dgisselq
 
861
                        c_wr <= 1'b0;
862
 
863
                        if (((i_wb_ack)&&(last_ack))||(i_wb_err))
864
                        begin
865 209 dgisselq
                                state        <= DC_IDLE;
866 201 dgisselq
                                cyc          <= 1'b0;
867 209 dgisselq
                                stb          <= 1'b0;
868 201 dgisselq
                                r_wb_cyc_gbl <= 1'b0;
869
                                r_wb_cyc_lcl <= 1'b0;
870 209 dgisselq
                                o_wb_stb_gbl <= 1'b0;
871
                                o_wb_stb_lcl <= 1'b0;
872 201 dgisselq
                        end
873 209 dgisselq
                end else if (state == DC_WRITE)
874 201 dgisselq
                begin
875 209 dgisselq
                        c_wr    <= (stb)&&(c_v[o_wb_addr[CS-1:LS]])
876
                                &&(c_vtags[o_wb_addr[CS-1:LS]]==o_wb_addr[AW-1:LS])
877
                                &&(stb);
878 201 dgisselq
                        c_wdata <= o_wb_data;
879 209 dgisselq
                        c_waddr <= r_addr[CS-1:0];
880
                        c_wsel  <= o_wb_sel;
881 201 dgisselq
 
882
                        if ((!i_wb_stall)&&(!i_pipe_stb))
883
                        begin
884
                                stb          <= 1'b0;
885
                                o_wb_stb_gbl <= 1'b0;
886
                                o_wb_stb_lcl <= 1'b0;
887
                        end
888
 
889
                        wr_cstb  <= (stb)&&(!i_wb_stall)&&(in_cache);
890
 
891 209 dgisselq
                        if ((stb)&&(!i_wb_stall))
892
                                o_wb_addr <= i_addr[(AW+1):2];
893
 
894
                        if (((i_wb_ack)&&(last_ack)
895
                                                &&((!OPT_PIPE)||(!i_pipe_stb)))
896
                                ||(i_wb_err))
897 201 dgisselq
                        begin
898 209 dgisselq
                                state        <= DC_IDLE;
899 201 dgisselq
                                cyc          <= 1'b0;
900 209 dgisselq
                                stb          <= 1'b0;
901 201 dgisselq
                                r_wb_cyc_gbl <= 1'b0;
902
                                r_wb_cyc_lcl <= 1'b0;
903 209 dgisselq
                                o_wb_stb_gbl <= 1'b0;
904
                                o_wb_stb_lcl <= 1'b0;
905 201 dgisselq
                        end
906
                end
907
        end
908
 
909
        //
910 209 dgisselq
        // npending is the number of outstanding (non-cached) read or write
911
        // requests
912
        initial npending = 0;
913
        always @(posedge i_clk)
914
        if ((i_reset)||(!OPT_PIPE)
915
                        ||((cyc)&&(i_wb_err))
916
                        ||((!cyc)&&(!i_pipe_stb))
917
                        ||(state == DC_READC))
918
                npending <= 0;
919
        else if (r_svalid)
920
                npending <= (i_pipe_stb) ? 1:0;
921
        else case({ (i_pipe_stb), (cyc)&&(i_wb_ack) })
922
        2'b01: npending <= npending - 1'b1;
923
        2'b10: npending <= npending + 1'b1;
924
        default: begin end
925
        endcase
926
 
927
        initial last_ack = 1'b0;
928
        always @(posedge i_clk)
929
        if (i_reset)
930
                last_ack <= 1'b0;
931
        else if (state == DC_IDLE)
932
        begin
933
                last_ack <= 1'b0;
934
                if ((i_pipe_stb)&&(i_op[0]))
935
                        last_ack <= 1'b1;
936
                else if (r_cache_miss)
937
                        last_ack <= (LS == 0);
938
                else if ((i_pipe_stb)&&(!w_cachable))
939
                        last_ack <= 1'b1;
940
        end else if (state == DC_READC)
941
        begin
942
                if (i_wb_ack)
943
                        last_ack <= last_ack || (&wr_addr[LS-1:1]);
944
                else
945
                        last_ack <= last_ack || (&wr_addr[LS-1:0]);
946
        end else case({ (i_pipe_stb), (i_wb_ack) })
947
        2'b01: last_ack <= (npending <= 2);
948
        2'b10: last_ack <= (!cyc)||(npending == 0);
949
        default: begin end
950
        endcase
951
 
952
`ifdef  FORMAL
953
always @(*)
954
`ASSERT(npending <= { 1'b1, {(DP){1'b0}} });
955
 
956
`endif
957
 
958
 
959
        //
960 201 dgisselq
        // Writes to the cache
961
        //
962
        // These have been made as simple as possible.  Note that the c_wr
963
        // line has already been determined, as have the write value and address
964
        // on the last clock.  Further, this structure is defined to match the
965
        // block RAM design of as many architectures as possible.
966 209 dgisselq
        //
967 201 dgisselq
        always @(posedge i_clk)
968 209 dgisselq
        if (c_wr)
969
        begin
970
                if (c_wsel[0])
971
                        c_mem[c_waddr][7:0] <= c_wdata[7:0];
972
                if (c_wsel[1])
973
                        c_mem[c_waddr][15:8] <= c_wdata[15:8];
974
                if (c_wsel[2])
975
                        c_mem[c_waddr][23:16] <= c_wdata[23:16];
976
                if (c_wsel[3])
977
                        c_mem[c_waddr][31:24] <= c_wdata[31:24];
978
        end
979 201 dgisselq
 
980
        //
981
        // Reads from the cache
982
        //
983
        // Some architectures require that all reads be registered.  We
984
        // accomplish that here.  Whether or not the result of this read is
985
        // going to be our output will need to be determined with combinatorial
986
        // logic on the output.
987
        //
988 209 dgisselq
        generate if (OPT_DUAL_READ_PORT)
989
        begin
990 201 dgisselq
 
991 209 dgisselq
                always @(posedge i_clk)
992
                        cached_idata <= c_mem[i_caddr];
993 201 dgisselq
 
994 209 dgisselq
                always @(posedge i_clk)
995
                        cached_rdata <= c_mem[r_caddr];
996
 
997
        end else begin
998
 
999
                always @(posedge i_clk)
1000
                        cached_rdata <= c_mem[(o_busy) ? r_caddr : i_caddr];
1001
 
1002
                always @(*)
1003
                        cached_idata = cached_rdata;
1004
 
1005
        end endgenerate
1006
 
1007 201 dgisselq
// o_data can come from one of three places:
1008
// 1. The cache, assuming the data was in the last cache line
1009
// 2. The cache, second clock, assuming the data was in the cache at all
1010
// 3. The cache, after filling the cache
1011
// 4. The wishbone state machine, upon reading the value desired.
1012 209 dgisselq
        always @(*)
1013 201 dgisselq
                if (r_svalid)
1014 209 dgisselq
                        pre_data = cached_idata;
1015
                else if (state == DC_READS)
1016
                        pre_data = i_wb_data;
1017 201 dgisselq
                else
1018 209 dgisselq
                        pre_data = cached_rdata;
1019
 
1020 201 dgisselq
        always @(posedge i_clk)
1021 209 dgisselq
        casez(req_data[3:0])
1022
        4'b100?: o_data <= { 16'h0, pre_data[31:16] };
1023
        4'b101?: o_data <= { 16'h0, pre_data[15: 0] };
1024
        4'b1100: o_data <= { 24'h0, pre_data[31:24] };
1025
        4'b1101: o_data <= { 24'h0, pre_data[23:16] };
1026
        4'b1110: o_data <= { 24'h0, pre_data[15: 8] };
1027
        4'b1111: o_data <= { 24'h0, pre_data[ 7: 0] };
1028
        default o_data <= pre_data;
1029
        endcase
1030
 
1031
        initial o_valid = 1'b0;
1032 201 dgisselq
        always @(posedge i_clk)
1033 209 dgisselq
        if (i_reset)
1034
                o_valid <= 1'b0;
1035
        else if (state == DC_READS)
1036
                o_valid <= i_wb_ack;
1037
        else
1038
                o_valid <= (r_svalid)||(r_dvalid);
1039
 
1040
        initial o_err = 1'b0;
1041
        always @(posedge i_clk)
1042
        if (i_reset)
1043
                o_err <= 1'b0;
1044
        else
1045 201 dgisselq
                o_err <= (cyc)&&(i_wb_err);
1046
 
1047 209 dgisselq
        initial o_busy = 0;
1048
        always @(posedge i_clk)
1049
        if ((i_reset)||((cyc)&&(i_wb_err)))
1050
                o_busy <= 1'b0;
1051
        else if (i_pipe_stb)
1052
                o_busy <= 1'b1;
1053
        else if ((state == DC_READS)&&(i_wb_ack))
1054
                o_busy <= 1'b0;
1055
        else if ((r_rd_pending)&&(!r_dvalid))
1056
                o_busy <= 1'b1;
1057
        else if ((state == DC_WRITE)
1058
                        &&(i_wb_ack)&&(last_ack)&&(!i_pipe_stb))
1059
                o_busy <= 1'b0;
1060
        else if (cyc)
1061
                o_busy <= 1'b1;
1062
        else // if ((r_dvalid)||(r_svalid))
1063
                o_busy <= 1'b0;
1064 201 dgisselq
 
1065 209 dgisselq
        //
1066
        // We can use our FIFO addresses to pre-calculate when an ACK is going
1067
        // to be the last_noncachable_ack.
1068 201 dgisselq
 
1069 209 dgisselq
 
1070
        always @(*)
1071
        if (OPT_PIPE)
1072
                o_pipe_stalled = (cyc)&&((!o_wb_we)||(i_wb_stall)||(!stb))
1073
                                ||(r_rd_pending)||(npending[DP]);
1074
        else
1075
                o_pipe_stalled = o_busy;
1076
 
1077
        initial lock_gbl = 0;
1078
        initial lock_lcl = 0;
1079
        always @(posedge i_clk)
1080
        if (i_reset)
1081
        begin
1082
                lock_gbl <= 1'b0;
1083
                lock_lcl<= 1'b0;
1084
        end else begin
1085
                lock_gbl <= (OPT_LOCK)&&(i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
1086
                lock_lcl <= (OPT_LOCK)&&(i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
1087
        end
1088
 
1089
        assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
1090
        assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
1091
 
1092
        generate if (AW+2 < DW)
1093
        begin : UNUSED_BITS
1094
 
1095
                // Verilator lint_off UNUSED
1096
                wire    [DW-AW-2:0]      unused;
1097
                assign  unused = i_addr[DW-1:AW+1];
1098
                // Verilator lint_on  UNUSED
1099
        end endgenerate
1100
 
1101
`ifdef  FORMAL
1102
 
1103
        initial f_past_valid = 1'b0;
1104
        always @(posedge i_clk)
1105
                f_past_valid <= 1'b1;
1106
 
1107
        ////////////////////////////////////////////////
1108 201 dgisselq
        //
1109 209 dgisselq
        // Reset properties
1110 201 dgisselq
        //
1111 209 dgisselq
        ////////////////////////////////////////////////
1112 201 dgisselq
        //
1113
        //
1114 209 dgisselq
        always @(*)
1115
        if(!f_past_valid)
1116
                `ASSUME(i_reset);
1117
 
1118
        always @(posedge i_clk)
1119
        if ((!f_past_valid)||($past(i_reset)))
1120
        begin
1121
                // Insist on initial statements matching reset values
1122
                `ASSERT(r_rd == 1'b0);
1123
                `ASSERT(r_cachable == 1'b0);
1124
                `ASSERT(r_svalid == 1'b0);
1125
                `ASSERT(r_dvalid == 1'b0);
1126
                `ASSERT(r_cache_miss == 1'b0);
1127
                `ASSERT(r_addr == 0);
1128
                //
1129
                `ASSERT(c_wr == 0);
1130
                `ASSERT(c_v  == 0);
1131
                //
1132
                // assert(aux_head == 0);
1133
                // assert(aux_tail == 0);
1134
                //
1135
                `ASSERT(lock_gbl == 0);
1136
                `ASSERT(lock_lcl == 0);
1137
        end
1138
 
1139
        ////////////////////////////////////////////////
1140 201 dgisselq
        //
1141 209 dgisselq
        // Assumptions about our inputs
1142
        //
1143
        ////////////////////////////////////////////////
1144
        //
1145
        //
1146
        always @(*)
1147
        if (o_pipe_stalled)
1148
                `ASSUME(!i_pipe_stb);
1149
 
1150
        always @(*)
1151
        if (!f_past_valid)
1152
                `ASSUME(!i_pipe_stb);
1153
 
1154 201 dgisselq
        always @(posedge i_clk)
1155 209 dgisselq
        if ((f_past_valid)&&(!$past(i_reset))
1156
                &&($past(i_pipe_stb))&&($past(o_pipe_stalled)))
1157 201 dgisselq
        begin
1158 209 dgisselq
                `ASSUME($stable(i_pipe_stb));
1159
                `ASSUME($stable(i_op[0]));
1160
                `ASSUME($stable(i_addr));
1161
                if (i_op[0])
1162
                        `ASSUME($stable(i_data));
1163 201 dgisselq
        end
1164 209 dgisselq
 
1165 201 dgisselq
        always @(posedge i_clk)
1166 209 dgisselq
        if (o_err)
1167
                `ASSUME(!i_pipe_stb);
1168
 
1169
        ////////////////////////////////////////////////
1170
        //
1171
        // Wishbone properties
1172
        //
1173
        ////////////////////////////////////////////////
1174
        //
1175
        //
1176
        wire    f_cyc, f_stb;
1177
 
1178
        assign  f_cyc = (o_wb_cyc_gbl)|(o_wb_cyc_lcl);
1179
        assign  f_stb = (o_wb_stb_gbl)|(o_wb_stb_lcl);
1180
 
1181
        always @(*)
1182 201 dgisselq
        begin
1183 209 dgisselq
                // Only one interface can be active at once
1184
                `ASSERT((!o_wb_cyc_gbl)||(!o_wb_cyc_lcl));
1185
                // Strobe may only be active on the active interface
1186
                `ASSERT((r_wb_cyc_gbl)||(!o_wb_stb_gbl));
1187
                `ASSERT((r_wb_cyc_lcl)||(!o_wb_stb_lcl));
1188
                if (o_wb_stb_lcl)
1189
                begin
1190
                        if (o_wb_we)
1191
                                assert(state == DC_WRITE);
1192
                        else
1193
                                assert(state == DC_READS);
1194
                end
1195
 
1196
                if (cyc)
1197
                        assert(o_wb_we == (state == DC_WRITE));
1198 201 dgisselq
        end
1199
 
1200 209 dgisselq
        always @(posedge i_clk)
1201
        if ((f_past_valid)&&(cyc)&&($past(cyc)))
1202
        begin
1203
                `ASSERT($stable(r_wb_cyc_gbl));
1204
                `ASSERT($stable(r_wb_cyc_lcl));
1205
        end
1206
 
1207
 
1208
`ifdef  DCACHE
1209
`define FWB_MASTER      fwb_master
1210
`else
1211
`define FWB_MASTER      fwb_counter
1212
`endif
1213
 
1214
        `FWB_MASTER #(
1215
                .AW(AW), .DW(DW),
1216
                        .F_MAX_STALL(2),
1217
                        .F_MAX_ACK_DELAY(3),
1218
                        // If you need the proof to run faster, use these
1219
                        // lines instead of the two that follow
1220
                        // .F_MAX_STALL(1),
1221
                        // .F_MAX_ACK_DELAY(1),
1222
                        .F_LGDEPTH(F_LGDEPTH),
1223
                        .F_MAX_REQUESTS((OPT_PIPE) ? 0 : (1<<LS)),
1224
`ifdef  DCACHE
1225
                        .F_OPT_SOURCE(1'b1),
1226
`endif
1227
                        .F_OPT_DISCONTINUOUS(0)
1228
                ) fwb(i_clk, i_reset,
1229
                        cyc, f_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
1230
                                i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
1231
                f_nreqs, f_nacks, f_outstanding);
1232
 
1233
`ifdef  DCACHE  // Arbitrary access is specific to local dcache implementation
1234
        ////////////////////////////////////////////////
1235 201 dgisselq
        //
1236 209 dgisselq
        // Arbitrary address properties
1237
        //
1238
        ////////////////////////////////////////////////
1239
        //
1240
        //
1241
        (* anyconst *)  reg     [AW:0]           f_const_addr;
1242
        (* anyconst *)  reg                     f_const_buserr;
1243
        wire    [AW-LS-1:0]      f_const_tag, f_ctag_here, f_wb_tag;
1244
        wire    [CS-LS-1:0]      f_const_tag_addr;
1245
        reg     [DW-1:0] f_const_data;
1246
        wire    [DW-1:0] f_cmem_here;
1247
        reg                     f_pending_rd;
1248
        wire                    f_cval_in_cache;
1249 201 dgisselq
 
1250 209 dgisselq
        assign  f_const_tag    = f_const_addr[AW-1:LS];
1251
        assign  f_const_tag_addr = f_const_addr[CS-1:LS];
1252
        assign  f_cmem_here    = c_mem[f_const_addr[CS-1:0]];
1253
        assign  f_ctag_here    = c_vtags[f_const_addr[CS-1:LS]];
1254
        assign  f_wb_tag       = o_wb_addr[AW-1:LS];
1255 201 dgisselq
 
1256 209 dgisselq
        assign  f_cval_in_cache= (c_v[f_const_addr[CS-1:LS]])
1257
                                        &&(f_ctag_here == f_const_tag);
1258 201 dgisselq
 
1259 209 dgisselq
        generate if ((AW > DW - 8)&&(OPT_LOCAL_BUS))
1260
        begin : UPPER_CONST_ADDR_BITS
1261
 
1262
                always @(*)
1263
                if (f_const_addr[AW])
1264
                        assume(&f_const_addr[(AW-1):(DW-8)]);
1265
                else
1266
                        assume(!(&f_const_addr[(AW-1):(DW-8)]));
1267
        end endgenerate
1268
 
1269
        wire    [AW-1:0] wb_start;
1270
        assign  wb_start = (f_stb) ? (o_wb_addr - f_nreqs) : o_wb_addr;
1271
 
1272
        // Data changes upon request
1273 201 dgisselq
        always @(posedge i_clk)
1274
        begin
1275 209 dgisselq
                if ((i_pipe_stb)&&(i_addr[(AW+1):2] == f_const_addr[AW-1:0])
1276
                        &&(f_const_addr[AW] == ((OPT_LOCAL_BUS)
1277
                                                &&(&i_addr[(DW-1):(DW-8)])))
1278
                        &&(i_op[0]))
1279
                begin
1280
                        casez({ i_op[2:1], i_addr[1:0] })
1281
                        4'b0???: f_const_data <= i_data;
1282
                        4'b100?: f_const_data[31:16] <= i_data[15:0];
1283
                        4'b101?: f_const_data[15: 0] <= i_data[15:0];
1284
                        4'b1100: f_const_data[31:24] <= i_data[ 7:0];
1285
                        4'b1101: f_const_data[23:16] <= i_data[ 7:0];
1286
                        4'b1110: f_const_data[15: 8] <= i_data[ 7:0];
1287
                        4'b1111: f_const_data[ 7: 0] <= i_data[ 7:0];
1288
                        endcase
1289
                end
1290
 
1291
                if (f_cval_in_cache)
1292
                        assume((!i_wb_err)
1293
                                ||(!i_pipe_stb)
1294
                                ||(f_const_addr[AW-1:0] != i_addr[AW+1:2]));
1295 201 dgisselq
        end
1296
 
1297 209 dgisselq
 
1298
        always @(posedge i_clk)
1299
        if ((f_past_valid)&&(!i_reset)&&(!f_const_buserr))
1300
        begin
1301
                if ((cyc)&&(o_wb_we)&&(f_stb)
1302
                                &&(o_wb_addr[AW-1:0] == f_const_addr[AW-1:0])
1303
                                &&( o_wb_stb_lcl == f_const_addr[AW]))
1304
                begin
1305
 
1306
                        //
1307
                        // Changing our data
1308
                        //
1309
                        if (o_wb_sel[0])
1310
                                `ASSERT(o_wb_data[ 7: 0]==f_const_data[ 7: 0]);
1311
                        if (o_wb_sel[1])
1312
                                `ASSERT(o_wb_data[15: 8]==f_const_data[15: 8]);
1313
                        if (o_wb_sel[2])
1314
                                `ASSERT(o_wb_data[23:16]==f_const_data[23:16]);
1315
                        if (o_wb_sel[3])
1316
                                `ASSERT(o_wb_data[31:24]==f_const_data[31:24]);
1317
 
1318
                        // Check the data in the cache
1319
                        if ((!f_const_addr[AW])&&(c_v[f_const_tag_addr])
1320
                                &&(f_ctag_here == o_wb_addr[AW-1:LS]))
1321
                        begin
1322
                        if ((!c_wsel[0])&&(!o_wb_sel[0]))
1323
                                `ASSERT(f_cmem_here[ 7: 0]==f_const_data[ 7: 0]);
1324
                        if ((!c_wsel[1])&&(!o_wb_sel[1]))
1325
                                `ASSERT(f_cmem_here[15: 8]==f_const_data[15: 8]);
1326
                        if ((!c_wsel[2])&&(!o_wb_sel[2]))
1327
                                `ASSERT(f_cmem_here[23:16]==f_const_data[23:16]);
1328
                        if ((!c_wsel[3])&&(!o_wb_sel[3]))
1329
                                `ASSERT(f_cmem_here[31:24]==f_const_data[31:24]);
1330
 
1331
                        end
1332
                end else if ((!f_const_addr[AW])&&(c_v[f_const_tag_addr])
1333
                        &&(f_ctag_here ==f_const_addr[AW-1:LS]))
1334
                begin
1335
                        // If ...
1336
                        //   1. Our magic address is cachable
1337
                        //   2. Our magic address is associated with a valid
1338
                        //              cache line
1339
                        //   3. The cache tag matches our magic address
1340
 
1341
 
1342
                        // if ($past(cyc && i_wb_err))
1343
                        // begin
1344
                                // Ignore what happens on an error, the result
1345
                                // becomes undefined anyway
1346
                        // end else
1347
                        if ((c_wr)
1348
                                &&(c_waddr[CS-1:0] == f_const_addr[CS-1:0]))
1349
                        begin
1350
                                //
1351
                                // If we are writing to this valid cache line
1352
                                //
1353
                                if (c_wsel[3])
1354
                                        `ASSERT(c_wdata[31:24]
1355
                                                        == f_const_data[31:24]);
1356
                                else
1357
                                        `ASSERT(f_cmem_here[31:24]
1358
                                                        == f_const_data[31:24]);
1359
                                if (c_wsel[2])
1360
                                        `ASSERT(c_wdata[23:16]
1361
                                                        == f_const_data[23:16]);
1362
                                else
1363
                                        `ASSERT(f_cmem_here[23:16] == f_const_data[23:16]);
1364
                                if (c_wsel[1])
1365
                                        `ASSERT(c_wdata[15:8]
1366
                                                        == f_const_data[15:8]);
1367
                                else
1368
                                        `ASSERT(f_cmem_here[15:8] == f_const_data[15:8]);
1369
                                if (c_wsel[0])
1370
                                        `ASSERT(c_wdata[7:0]
1371
                                                        == f_const_data[7:0]);
1372
                                else
1373
                                        `ASSERT(f_cmem_here[7:0] == f_const_data[7:0]);
1374
                        end else
1375
                                `ASSERT(f_cmem_here == f_const_data);
1376
                end
1377
        end
1378
 
1379
        always @(posedge i_clk)
1380
        if ((f_past_valid)&&(state == DC_READC))
1381
        begin
1382
                `ASSERT(f_wb_tag == r_ctag);
1383
                if ((wb_start[AW-1:LS] == f_const_tag)
1384
                        &&(!c_v[f_const_tag_addr])
1385
                        &&(f_const_addr[AW] == r_wb_cyc_lcl)
1386
                        &&(f_nacks > f_const_addr[LS-1:0]))
1387
                begin
1388
                        // We are reading the cache line containing our
1389
                        // constant address f_const_addr.  Make sure the data
1390
                        // is correct.
1391
                        if ((c_wr)&&(c_waddr[CS-1:0] == f_const_addr[CS-1:0]))
1392
                                `ASSERT(c_wdata == f_const_data);
1393
                        else
1394
                                `ASSERT(f_cmem_here == f_const_data);
1395
                end
1396
 
1397
                if (f_nacks > 0)
1398
                        `ASSERT(!c_v[wb_start[CS-1:LS]]);
1399
        end
1400
 
1401
        always @(posedge i_clk)
1402
        if ((state == DC_READC)&&(f_nacks > 0))
1403
        begin
1404
                `ASSERT(c_vtags[wb_start[(CS-1):LS]] <= wb_start[(AW-1):LS]);
1405
                `ASSERT(c_vtags[wb_start[(CS-1):LS]] <= r_addr[AW-1:LS]);
1406
        end
1407
 
1408
        reg     [AW-1:0] f_cache_waddr;
1409
        wire                    f_this_cache_waddr;
1410
 
1411
        always @(*)
1412
        begin
1413
                // f_cache_waddr[AW-1:LS] = c_vtags[c_waddr[CS-1:CS-LS]];
1414
                f_cache_waddr[AW-1:LS] = wb_start[AW-1:LS];
1415
                f_cache_waddr[CS-1: 0] = c_waddr[CS-1:0];
1416
        end
1417
 
1418
        assign  f_this_cache_waddr = (!f_const_addr[AW])
1419
                                &&(f_cache_waddr == f_const_addr[AW-1:0]);
1420
        always @(posedge i_clk)
1421
        if ((f_past_valid)&&(state == DC_READC))
1422
        begin
1423
                if ((c_wr)&&(c_waddr[LS-1:0] != 0)&&(f_this_cache_waddr))
1424
                        `ASSERT(c_wdata == f_const_data);
1425
        end
1426
 
1427
        always @(posedge i_clk)
1428
        if ((OPT_PIPE)&&(o_busy)&&(i_pipe_stb))
1429
        begin
1430
                `ASSUME(i_op[0] == o_wb_we);
1431
                if (o_wb_cyc_lcl)
1432
                        assume(&i_addr[DW-1:DW-8]);
1433
                else
1434
                        assume(!(&i_addr[DW-1:DW-8]));
1435
        end
1436
 
1437
        initial f_pending_rd = 0;
1438
        always @(posedge i_clk)
1439
        if (i_reset)
1440
                f_pending_rd <= 0;
1441
        else if (i_pipe_stb)
1442
                f_pending_rd <= (!i_op[0]);
1443
        else if ((o_valid)&&((!OPT_PIPE)
1444
                ||((state != DC_READS)&&(!r_svalid)&&(!$past(i_pipe_stb)))))
1445
                f_pending_rd <= 1'b0;
1446
 
1447
        always @(*)
1448
        if ((state == DC_READC)&&(!f_stb))
1449
                `ASSERT(f_nreqs == (1<<LS));
1450
 
1451
        always @(*)
1452
        if ((state == DC_READC)&&(f_stb))
1453
                `ASSERT(f_nreqs == { 1'b0, o_wb_addr[LS-1:0] });
1454
 
1455
        always @(posedge i_clk)
1456
        if (state == DC_READC)
1457
        begin
1458
                if (($past(i_wb_ack))&&(!$past(f_stb)))
1459
                        `ASSERT(f_nacks-1 == { 1'b0, c_waddr[LS-1:0] });
1460
                else if (f_nacks > 0)
1461
                begin
1462
                        `ASSERT(f_nacks-1 == { 1'b0, c_waddr[LS-1:0] });
1463
                        `ASSERT(c_waddr[CS-1:LS] == o_wb_addr[CS-1:LS]);
1464
                end else begin
1465
                        `ASSERT(c_waddr[CS-1:LS] == o_wb_addr[CS-1:LS]-1'b1);
1466
                        `ASSERT(&c_waddr[LS-1:0]);
1467
                end
1468
        end
1469
 
1470
        always @(*)
1471
        if (r_rd_pending)
1472
                `ASSERT(r_addr == f_pending_addr[AW-1:0]);
1473
 
1474
        always @(*)
1475
        if (f_pending_addr[AW])
1476
        begin
1477
                `ASSERT(state != DC_READC);
1478
                `ASSERT((!o_wb_we)||(!o_wb_cyc_gbl));
1479
        end
1480
 
1481
        always @(posedge i_clk)
1482
        if ((f_past_valid)&&(o_valid)&&($past(f_pending_addr) == f_const_addr))
1483
        begin
1484
                if (f_const_buserr)
1485
                        `ASSERT(o_err);
1486
                else if (f_pending_rd)
1487
                begin
1488
                        casez($past(req_data[3:0]))
1489
                        4'b0???: `ASSERT(o_data ==f_const_data);
1490
                        4'b101?: `ASSERT(o_data =={16'h00,f_const_data[15: 0]});
1491
                        4'b100?: `ASSERT(o_data =={16'h00,f_const_data[31:16]});
1492
                        4'b1100: `ASSERT(o_data =={24'h00,f_const_data[31:24]});
1493
                        4'b1101: `ASSERT(o_data =={24'h00,f_const_data[23:16]});
1494
                        4'b1110: `ASSERT(o_data =={24'h00,f_const_data[15: 8]});
1495
                        4'b1111: `ASSERT(o_data =={24'h00,f_const_data[ 7: 0]});
1496
                        endcase
1497
                end
1498
        end
1499
 
1500
        wire                    f_this_return;
1501
 
1502
        assign  f_this_return = (f_return_address == f_const_addr);
1503
        always @(*)
1504
        if ((f_cyc)&&(
1505
                ((state == DC_READC)
1506
                        &&(f_return_address[AW-1:LS] == f_const_addr[AW-1:LS]))
1507
                ||(f_this_return))&&(f_cyc))
1508
        begin
1509
                if (f_const_buserr)
1510
                        assume(!i_wb_ack);
1511
                else begin
1512
                        assume(!i_wb_err);
1513
                        assume(i_wb_data == f_const_data);
1514
                end
1515
        end
1516
 
1517
        always @(posedge i_clk)
1518
        if ((f_past_valid)&&(last_tag == f_const_tag)&&(f_const_buserr)
1519
                        &&(!f_const_addr[AW]))
1520
                `ASSERT(!last_tag_valid);
1521
 
1522
        always @(*)
1523
        if (f_const_buserr)
1524
        begin
1525
                `ASSERT((!c_v[f_const_tag_addr])||(f_const_addr[AW])
1526
                        ||(f_ctag_here != f_const_tag));
1527
 
1528
                if ((state == DC_READC)&&(wb_start[AW-1:LS] == f_const_tag))
1529
                begin
1530
                        `ASSERT(f_nacks <= f_const_tag[LS-1:0]);
1531
                        if (f_nacks == f_const_tag[LS-1:0])
1532
                                assume(!i_wb_ack);
1533
                end
1534
        end
1535
 
1536
`endif  // DCACHE
1537
 
1538
        ////////////////////////////////////////////////
1539
        //
1540
        // Checking the lock
1541
        //
1542
        ////////////////////////////////////////////////
1543
        //
1544
        //
1545
 
1546
        always @(*)
1547
                `ASSERT((!lock_gbl)||(!lock_lcl));
1548
        always @(*)
1549
        if (!OPT_LOCK)
1550
                `ASSERT((!lock_gbl)&&(!lock_lcl));
1551
 
1552
        ////////////////////////////////////////////////
1553
        //
1554
        // State based properties
1555
        //
1556
        ////////////////////////////////////////////////
1557
        //
1558
        //
1559
        reg     [F_LGDEPTH-1:0]  f_rdpending;
1560
 
1561
        initial f_rdpending = 0;
1562
        always @(posedge i_clk)
1563
        if ((i_reset)||(o_err))
1564
                f_rdpending <= 0;
1565
        else case({ (i_pipe_stb)&&(!i_op[0]), o_valid })
1566
        2'b01: f_rdpending <= f_rdpending - 1'b1;
1567
        2'b10: f_rdpending <= f_rdpending + 1'b1;
1568
        default: begin end
1569
        endcase
1570
 
1571
        wire    f_wb_cachable;
1572
        iscachable #(.ADDRESS_WIDTH(AW))
1573
                f_chkwb_addr(o_wb_addr, f_wb_cachable);
1574
 
1575
 
1576
        always @(*)
1577
        if (state == DC_IDLE)
1578
        begin
1579
                `ASSERT(!r_wb_cyc_gbl);
1580
                `ASSERT(!r_wb_cyc_lcl);
1581
 
1582
                `ASSERT(!cyc);
1583
 
1584
                if ((r_rd_pending)||(r_dvalid)||(r_svalid))
1585
                        `ASSERT(o_busy);
1586
 
1587
                if (!OPT_PIPE)
1588
                begin
1589
                        if (r_rd_pending)
1590
                                `ASSERT(o_busy);
1591
                        else if (r_svalid)
1592
                                `ASSERT(o_busy);
1593
                        else if (o_valid)
1594
                                `ASSERT(!o_busy);
1595
                        else if (o_err)
1596
                                `ASSERT(!o_busy);
1597
                end
1598
        end else begin
1599
                `ASSERT(o_busy);
1600
                `ASSERT(cyc);
1601
        end
1602
 
1603
 
1604
 
1605
        always @(posedge i_clk)
1606
        if (state == DC_IDLE)
1607
        begin
1608
                if (r_svalid)
1609
                begin
1610
                        `ASSERT(!r_dvalid);
1611
                        `ASSERT(!r_rd_pending);
1612
                        if (!OPT_PIPE)
1613
                                `ASSERT(!o_valid);
1614
                        else if (o_valid)
1615
                                `ASSERT(f_rdpending == 2);
1616
                end
1617
 
1618
                if (r_dvalid)
1619
                begin
1620
                        `ASSERT(!r_rd_pending);
1621
                        `ASSERT(npending == 0);
1622
                        `ASSERT(f_rdpending == 1);
1623
                end
1624
 
1625
                if (r_rd_pending)
1626
                begin
1627
                        if ((OPT_PIPE)&&(o_valid))
1628
                                `ASSERT(f_rdpending <= 2);
1629
                        else
1630
                                `ASSERT(f_rdpending == 1);
1631
 
1632
                end else if ((OPT_PIPE)&&(o_valid)&&($past(r_dvalid|r_svalid)))
1633
                                `ASSERT(f_rdpending <= 2);
1634
                else
1635
                        `ASSERT(f_rdpending <= 1);
1636
        end
1637
 
1638
        always @(posedge i_clk)
1639
        if (state == DC_READC)
1640
        begin
1641
                `ASSERT( o_wb_cyc_gbl);
1642
                `ASSERT(!o_wb_cyc_lcl);
1643
                `ASSERT(!o_wb_we);
1644
                `ASSERT(f_wb_cachable);
1645
 
1646
                `ASSERT(r_rd_pending);
1647
                `ASSERT(r_cachable);
1648
                if (($past(cyc))&&(!$past(o_wb_stb_gbl)))
1649
                        `ASSERT(!o_wb_stb_gbl);
1650
 
1651
                if ((OPT_PIPE)&&(o_valid))
1652
                        `ASSERT(f_rdpending == 2);
1653
                else
1654
                        `ASSERT(f_rdpending == 1);
1655
        end
1656
 
1657
        always @(*)
1658
        if (state == DC_READS)
1659
        begin
1660
                `ASSERT(!o_wb_we);
1661
 
1662
                if (OPT_PIPE)
1663
                begin
1664
                        if (o_valid)
1665
                                `ASSERT((f_rdpending == npending + 1)
1666
                                        ||(f_rdpending == npending));
1667
                        else
1668
                                `ASSERT(f_rdpending == npending);
1669
                end
1670
        end else if (state == DC_WRITE)
1671
                `ASSERT(o_wb_we);
1672
 
1673
        always @(posedge i_clk)
1674
        if ((state == DC_READS)||(state == DC_WRITE))
1675
        begin
1676
                `ASSERT(o_wb_we == (state == DC_WRITE));
1677
                `ASSERT(!r_rd_pending);
1678
                if (o_wb_we)
1679
                        `ASSERT(f_rdpending == 0);
1680
 
1681
                if (OPT_PIPE)
1682
                begin
1683
                        casez({ $past(i_pipe_stb), f_stb })
1684
                        2'b00: `ASSERT(npending == f_outstanding);
1685
                        2'b1?: `ASSERT(npending == f_outstanding + 1);
1686
                        2'b01: `ASSERT(npending == f_outstanding + 1);
1687
                        endcase
1688
 
1689
                        if (state == DC_WRITE)
1690
                                `ASSERT(!o_valid);
1691
                end else
1692
                        `ASSERT(f_outstanding <= 1);
1693
        end
1694
 
1695
        always @(*)
1696
        if (OPT_PIPE)
1697
                `ASSERT(f_rdpending <= 2);
1698
        else
1699
                `ASSERT(f_rdpending <= 1);
1700
 
1701
        always @(posedge i_clk)
1702
        if ((!OPT_PIPE)&&(o_valid))
1703
                `ASSERT(f_rdpending == 1);
1704
        else if (o_valid)
1705
                `ASSERT(f_rdpending >= 1);
1706
 
1707
 
1708
        always @(*)
1709
        if ((!o_busy)&&(!o_err)&&(!o_valid))
1710
                `ASSERT(f_rdpending == 0);
1711
 
1712
        always @(*)
1713
                `ASSERT(cyc == ((r_wb_cyc_gbl)||(r_wb_cyc_lcl)));
1714
 
1715
        always @(*)
1716
        if ((!i_reset)&&(f_nreqs == f_nacks)&&(!f_stb))
1717
                `ASSERT(!cyc);
1718
 
1719
        always @(posedge i_clk)
1720
        if ((f_past_valid)&&($past(o_err)))
1721
                `ASSUME(!i_lock);
1722
        else if ((f_past_valid)&&(OPT_LOCK)&&($past(i_lock))
1723
                        &&((!$past(o_valid)) || ($past(i_pipe_stb))))
1724
                `ASSUME($stable(i_lock));
1725
 
1726
 
1727
        ////////////////////////////////////////////////
1728
        //
1729
        // Ad-hoc properties
1730
        //
1731
        ////////////////////////////////////////////////
1732
        //
1733
        //
1734
        always @(*)
1735
        if ((OPT_PIPE)&&(state == DC_WRITE)&&(!i_wb_stall)&&(stb)
1736
                        &&(!npending[DP]))
1737
                `ASSERT(!o_pipe_stalled);
1738
 
1739
        always @(posedge i_clk)
1740
        if (state == DC_WRITE)
1741
                `ASSERT(o_wb_we);
1742
        else if ((state == DC_READS)||(state == DC_READC))
1743
                `ASSERT(!o_wb_we);
1744
 
1745
        always @(*)
1746
        if (cyc)
1747
                `ASSERT(f_cyc);
1748
 
1749
        always @(posedge i_clk)
1750
        if ((f_past_valid)&&(!$past(cyc))&&(!c_wr)&&(last_tag_valid)
1751
                        &&(!r_rd_pending))
1752
                `ASSERT((c_v[last_tag[(CS-LS-1):0]])
1753
                        &&(c_vtags[last_tag[(CS-LS-1):0]] == last_tag));
1754
 
1755
        always @(*)
1756
        if (!OPT_LOCAL_BUS)
1757
        begin
1758
                `ASSERT(r_wb_cyc_lcl == 1'b0);
1759
                `ASSERT(o_wb_stb_lcl == 1'b0);
1760
                `ASSERT(lock_lcl == 1'b0);
1761
        end
1762
 
1763
        always @(posedge i_clk)
1764
        if ((state == DC_READC)&&(!stb))
1765
        begin
1766
                `ASSERT(o_wb_addr[LS-1:0] == 0);
1767
                `ASSERT(o_wb_addr[AW-1:CS] == r_addr[AW-1:CS]);
1768
        end else if ((state == DC_READC)&&(stb))
1769
        begin
1770
                `ASSERT(o_wb_addr[AW-1:CS] == r_addr[AW-1:CS]);
1771
                `ASSERT(o_wb_addr[LS-1:0] == f_nreqs[LS-1:0]);
1772
        end
1773
 
1774
        wire    [CS-1:0] f_expected_caddr;
1775
        assign  f_expected_caddr = { r_ctag[CS-LS-1:0], {(LS){1'b0}} }-1
1776
                                        + f_nacks;
1777
        always @(posedge i_clk)
1778
        if (state == DC_READC)
1779
        begin
1780
                if (LS == 0)
1781
                        `ASSERT(end_of_line);
1782
                else if (f_nacks < (1<<LS)-1)
1783
                        `ASSERT(!end_of_line);
1784
                else if (f_nacks == (1<<LS)-1)
1785
                        `ASSERT(end_of_line);
1786
                `ASSERT(f_nacks <= (1<<LS));
1787
                `ASSERT(f_nreqs <= (1<<LS));
1788
                if (f_nreqs < (1<<LS))
1789
                begin
1790
                        `ASSERT(o_wb_stb_gbl);
1791
                        `ASSERT(o_wb_addr[(LS-1):0] == f_nreqs[LS-1:0]);
1792
                end else
1793
                        `ASSERT(!f_stb);
1794
                `ASSERT((f_nreqs == 0)||(f_nacks <= f_nreqs));
1795
                `ASSERT(c_waddr == f_expected_caddr);
1796
        end
1797
 
1798
        always @(posedge i_clk)
1799
        if ((f_past_valid)&&(r_rd)&&(!$past(i_reset)))
1800
        begin
1801
                `ASSERT((o_busy)||(r_svalid));
1802
        end
1803
 
1804
        always @(posedge i_clk)
1805
        if (!$past(o_busy))
1806
                `ASSERT(!r_dvalid);
1807
 
1808
        always @(posedge i_clk)
1809
        if ((state == DC_READC)&&(c_wr))
1810
                `ASSERT(c_wsel == 4'hf);
1811
 
1812
        always @(*)
1813
        if (c_wr)
1814
                `ASSERT((c_wsel == 4'hf)
1815
                        ||(c_wsel == 4'hc)
1816
                        ||(c_wsel == 4'h3)
1817
                        ||(c_wsel == 4'h8)
1818
                        ||(c_wsel == 4'h4)
1819
                        ||(c_wsel == 4'h2)
1820
                        ||(c_wsel == 4'h1));
1821
 
1822
        always @(*)
1823
        if (!OPT_PIPE)
1824
                `ASSERT(o_pipe_stalled == o_busy);
1825
        else if (o_pipe_stalled)
1826
                `ASSERT(o_busy);
1827
 
1828
        //
1829
        // Only ever abort on reset
1830
        always @(posedge i_clk)
1831
        if ((f_past_valid)&&(!$past(i_reset))&&($past(cyc))&&(!$past(i_wb_err)))
1832
        begin
1833
                if (($past(i_pipe_stb))&&(!$past(o_pipe_stalled)))
1834
                        `ASSERT(cyc);
1835
                else if ($past(f_outstanding > 1))
1836
                        `ASSERT(cyc);
1837
                else if (($past(f_outstanding == 1))
1838
                                &&((!$past(i_wb_ack))
1839
                                        ||(($past(f_stb))
1840
                                                &&(!$past(i_wb_stall)))))
1841
                        `ASSERT(cyc);
1842
                else if (($past(f_outstanding == 0))
1843
                                &&($past(f_stb)&&(!$past(i_wb_ack))))
1844
                        `ASSERT(cyc);
1845
        end
1846
 
1847
        always @(posedge i_clk)
1848
        if ((OPT_PIPE)&&(f_past_valid)&&(!$past(i_reset))&&(state != DC_READC))
1849
        begin
1850
                if ($past(cyc && i_wb_err))
1851
                begin
1852
                        `ASSERT(npending == 0);
1853
                end else if (($past(i_pipe_stb))||($past(i_wb_stall && stb)))
1854
                        `ASSERT((npending == f_outstanding+1)
1855
                                ||(npending == f_outstanding+2));
1856
                else
1857
                        `ASSERT(npending == f_outstanding);
1858
        end
1859
 
1860
        always @(posedge i_clk)
1861
        if ((OPT_PIPE)&&(state != DC_READC)&&(state != DC_IDLE))
1862
                `ASSERT(last_ack == (npending <= 1));
1863
 
1864
        always @(*)
1865
        `ASSERT(stb == f_stb);
1866
 
1867
        always @(*)
1868
        if (r_rd_pending)
1869
                `ASSERT(!r_svalid);
1870
 
1871
        always @(*)
1872
        if (o_err)
1873
                `ASSUME(!i_pipe_stb);
1874
 
1875
        always @(*)
1876
        if (last_tag_valid)
1877
                `ASSERT(|c_v);
1878
 
1879
        always @(posedge i_clk)
1880
        if ((cyc)&&(state == DC_READC)&&($past(f_nacks > 0)))
1881
                `ASSERT(!c_v[o_wb_addr[CS-1:LS]]);
1882
 
1883
        always @(*)
1884
        if (last_tag_valid)
1885
        begin
1886
                `ASSERT((!cyc)||(o_wb_we)||(state == DC_READS)
1887
                                        ||(o_wb_addr[AW-1:LS] != last_tag));
1888
        end
1889
 
1890
        wire    f_cachable_last_tag, f_cachable_r_addr;
1891
 
1892
        iscachable #(.ADDRESS_WIDTH(AW))
1893
                fccheck_last_tag({last_tag, {(LS){1'b0}}}, f_cachable_last_tag);
1894
 
1895
        iscachable #(.ADDRESS_WIDTH(AW))
1896
                fccheck_r_cachable(r_addr, f_cachable_r_addr);
1897
 
1898
        always @(*)
1899
        if ((r_cachable)&&(r_rd_pending))
1900
        begin
1901
                `ASSERT(state != DC_WRITE);
1902
                // `ASSERT(state != DC_READS);
1903
                `ASSERT(f_cachable_r_addr);
1904
                if (cyc)
1905
                        `ASSERT(o_wb_addr[AW-1:LS] == r_addr[AW-1:LS]);
1906
        end
1907
 
1908
        always @(*)
1909
        if (last_tag_valid)
1910
        begin
1911
                `ASSERT(f_cachable_last_tag);
1912
                `ASSERT(c_v[last_tag[CS-LS-1:0]]);
1913
                `ASSERT(c_vtags[last_tag[CS-LS-1:0]]==last_tag);
1914
                `ASSERT((state != DC_READC)||(last_tag != o_wb_addr[AW-1:LS]));
1915
        end
1916
 
1917
 
1918
        ////////////////////////////////////////////////
1919
        //
1920
        // Cover statements
1921
        //
1922
        ////////////////////////////////////////////////
1923
        //
1924
        //
1925
 
1926
        always @(posedge i_clk)
1927
                cover(o_valid);
1928
 
1929
        always @(posedge i_clk)
1930
        if (f_past_valid)
1931
                cover($past(r_svalid));
1932
 
1933
        generate if (OPT_PIPE)
1934
        begin : PIPE_COVER
1935
 
1936
                wire            recent_reset;
1937
                reg     [2:0]    recent_reset_sreg;
1938
                initial recent_reset_sreg = -1;
1939
                always @(posedge i_clk)
1940
                if (i_reset)
1941
                        recent_reset_sreg <= -1;
1942
                else
1943
                        recent_reset_sreg <= { recent_reset_sreg[1:0], 1'b0 };
1944
 
1945
                assign recent_reset = (i_reset)||(|recent_reset_sreg);
1946
 
1947
                //
1948
                //
1949
                wire    f_cvr_cread = (!recent_reset)&&(i_pipe_stb)&&(!i_op[0])
1950
                                        &&(w_cachable);
1951
 
1952
                wire    f_cvr_cwrite = (!recent_reset)&&(i_pipe_stb)&&(i_op[0])
1953
                                &&(!cache_miss_inow);
1954
 
1955
                wire    f_cvr_writes = (!recent_reset)&&(i_pipe_stb)&&(i_op[0])
1956
                                        &&(!w_cachable);
1957
                wire    f_cvr_reads  = (!recent_reset)&&(i_pipe_stb)&&(!i_op[0])
1958
                                        &&(!w_cachable);
1959
                wire    f_cvr_test  = (!recent_reset)&&(cyc);
1960
 
1961
                always @(posedge i_clk)
1962
                if ((f_past_valid)&&($past(o_valid)))
1963
                        cover(o_valid);         // !
1964
 
1965
                always @(posedge i_clk)
1966
                if ((f_past_valid)&&(!$past(i_reset))&&($past(i_pipe_stb)))
1967
                        cover(i_pipe_stb);
1968
 
1969
                always @(posedge i_clk)
1970
                if ((f_past_valid)&&($past(o_valid))&&($past(o_valid,2)))
1971
                        cover(o_valid);
1972
 
1973
                always @(posedge i_clk)
1974
                        cover(($past(f_cvr_cread))&&(f_cvr_cread));
1975
 
1976
                always @(posedge i_clk)
1977
                        cover(($past(f_cvr_cwrite))&&(f_cvr_cwrite));
1978
 
1979
                always @(posedge i_clk)
1980
                        cover(($past(f_cvr_writes))&&(f_cvr_writes));
1981
 
1982
                /*
1983
                * This cover statement will never pass.  Why not?  Because
1984
                * cache reads must be separated from non-cache reads.  Hence,
1985
                * we can only allow a single non-cache read at a time, otherwise
1986
                * we'd bypass the cache read logic.
1987
                *
1988
                always @(posedge i_clk)
1989
                        cover(($past(f_cvr_reads))&&(f_cvr_reads));
1990
                */
1991
 
1992
                //
1993
                // This is unrealistic, as it depends upon the Wishbone
1994
                // acknoledging the request on the same cycle
1995
                always @(posedge i_clk)
1996
                        cover(($past(f_cvr_reads,2))&&(f_cvr_reads));
1997
 
1998
                always @(posedge i_clk)
1999
                        cover(($past(r_dvalid))&&(r_svalid));
2000
 
2001
                //
2002
                // A minimum of one clock must separate two dvalid's.
2003
                // This option is rather difficult to cover, since it means
2004
                // we must first load two separate cache lines before
2005
                // this can even be tried.
2006
                always @(posedge i_clk)
2007
                        cover(($past(r_dvalid,2))&&(r_dvalid));
2008
 
2009
                //
2010
                // This is the optimal configuration we want:
2011
                //      i_pipe_stb
2012
                //      ##1 i_pipe_stb && r_svalid
2013
                //      ##1 r_svalid && o_valid
2014
                //      ##1 o_valid
2015
                // It proves that we can handle a 2 clock delay, but that
2016
                // we can also pipelin these cache accesses, so this
2017
                // 2-clock delay becomes a 1-clock delay between pipelined
2018
                // memory reads.
2019
                //
2020
                always @(posedge i_clk)
2021
                        cover(($past(r_svalid))&&(r_svalid));
2022
 
2023
                //
2024
                // While we'd never do this (it breaks the ZipCPU's pipeline
2025
                // rules), it's nice to know we could.
2026
                //      i_pipe_stb && (!i_op[0]) // a read
2027
                //      ##1 i_pipe_stb && (i_op[0]) && r_svalid // a write
2028
                //      ##1 o_valid
2029
                always @(posedge i_clk)
2030
                        cover(($past(r_svalid))&&(f_cvr_writes));
2031
 
2032
                /* Unreachable
2033
                *
2034
                always @(posedge i_clk)
2035
                        cover(($past(f_cvr_writes))&&(o_valid));
2036
 
2037
                always @(posedge i_clk)
2038
                        cover(($past(f_cvr_writes,2))&&(o_valid));
2039
 
2040
                always @(posedge i_clk)
2041
                        cover(($past(f_cvr_writes,3))&&(o_valid));
2042
 
2043
                always @(posedge i_clk)
2044
                        cover(($past(r_dvalid,3))&&(r_dvalid));
2045
 
2046
                */
2047
 
2048
                always @(posedge i_clk)
2049
                        cover(($past(f_cvr_writes,4))&&(o_valid));
2050
 
2051
        end endgenerate
2052
 
2053
        ////////////////////////////////////////////////
2054
        //
2055
        // Carelesss assumption section
2056
        //
2057
        ////////////////////////////////////////////////
2058
        //
2059
        //
2060
 
2061
        //
2062
        // Can't jump from local to global mid lock
2063
        always @(*)
2064
        if((OPT_LOCK)&&(OPT_LOCAL_BUS))
2065
        begin
2066
                if ((i_lock)&&(o_wb_cyc_gbl)&&(i_pipe_stb))
2067
                        assume(!(&i_addr[(DW-1):(DW-8)]));
2068
                else if ((i_lock)&&(o_wb_cyc_lcl)&&(i_pipe_stb))
2069
                        assume(&i_addr[(DW-1):(DW-8)]);
2070
        end
2071
 
2072
        always @(*)
2073
        if ((OPT_PIPE)&&(o_busy || i_lock)&&(!o_pipe_stalled))
2074
        begin
2075
                if (i_pipe_stb)
2076
                        assume((!OPT_LOCAL_BUS)
2077
                                ||(f_pending_addr[AW]==(&i_addr[DW-1:DW-8])));
2078
        end
2079
 
2080
        always @(posedge i_clk)
2081
        if ((f_past_valid)&&(!$past(cyc))&&(!cyc))
2082
                assume((!i_wb_err)&&(!i_wb_ack));
2083
 
2084
`endif
2085 201 dgisselq
endmodule

powered by: WebSVN 2.1.0

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