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

Subversion Repositories zipcpu

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

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 69 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3 82 dgisselq
// Filename:    pfcache.v
4 69 dgisselq
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     Keeping our CPU fed with instructions, at one per clock and
8 209 dgisselq
//              with only a minimum number stalls.  The entire cache may also
9
//      be cleared (if necessary).
10 69 dgisselq
//
11 209 dgisselq
//      This logic is driven by a couple realities:
12
//      1. It takes a clock to read from a block RAM address, and hence a clock
13
//              to read from the cache.
14
//      2. It takes another clock to check that the tag matches
15
//
16
//              Our goal will be to avoid this second check if at all possible.
17
//              Hence, we'll test on the clock of any given request whether
18
//              or not the request matches the last tag value, and on the next
19
//              clock whether it new tag value (if it has changed).  Hence,
20
//              for anything found within the cache, there will be a one
21
//              cycle delay on any branch.
22
//
23
//
24
//      Address Words are separated into three components:
25
//      [ Tag bits ] [ Cache line number ] [ Cache position w/in the line ]
26
//
27
//      On any read from the cache, only the second two components are required.
28
//      On any read from memory, the first two components will be fixed across
29
//      the bus, and the third component will be adjusted from zero to its
30
//      maximum value.
31
//
32
//
33 69 dgisselq
// Creator:     Dan Gisselquist, Ph.D.
34
//              Gisselquist Technology, LLC
35
//
36
////////////////////////////////////////////////////////////////////////////////
37
//
38 209 dgisselq
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
39 69 dgisselq
//
40
// This program is free software (firmware): you can redistribute it and/or
41
// modify it under the terms of  the GNU General Public License as published
42
// by the Free Software Foundation, either version 3 of the License, or (at
43
// your option) any later version.
44
//
45
// This program is distributed in the hope that it will be useful, but WITHOUT
46
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
47
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
48
// for more details.
49
//
50 201 dgisselq
// You should have received a copy of the GNU General Public License along
51
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
52
// target there if the PDF file isn't present.)  If not, see
53
// <http://www.gnu.org/licenses/> for a copy.
54
//
55 69 dgisselq
// License:     GPL, v3, as defined and found on www.gnu.org,
56
//              http://www.gnu.org/licenses/gpl.html
57
//
58
//
59
////////////////////////////////////////////////////////////////////////////////
60
//
61 201 dgisselq
//
62 209 dgisselq
`default_nettype        none
63
//
64
module  pfcache(i_clk, i_reset, i_new_pc, i_clear_cache,
65 69 dgisselq
                        // i_early_branch, i_from_addr,
66 209 dgisselq
                        i_stall_n, i_pc, o_insn, o_pc, o_valid,
67 69 dgisselq
                o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
68
                        i_wb_ack, i_wb_stall, i_wb_err, i_wb_data,
69 209 dgisselq
                        o_illegal
70
`ifdef  NOT_YET_READY
71
                , i_mmu_ack, i_mmu_we, i_mmu_paddr
72
`endif
73
`ifdef  FORMAL
74
                , f_pc_wb
75
`endif
76
                );
77
`ifdef  FORMAL
78
        parameter       LGCACHELEN = 4, ADDRESS_WIDTH=30,
79
                        LGLINES=2; // Log of the number of separate cache lines
80
`else
81
        parameter       LGCACHELEN = 12, ADDRESS_WIDTH=30,
82
                        LGLINES=6; // Log of the number of separate cache lines
83
`endif
84
        localparam      CACHELEN=(1<<LGCACHELEN); //Wrd Size of our cache memory
85 194 dgisselq
        localparam      CW=LGCACHELEN;  // Short hand for LGCACHELEN
86 209 dgisselq
        localparam      LS=LGCACHELEN-LGLINES; // Size of a cache line
87 194 dgisselq
        localparam      BUSW = 32;      // Number of data lines on the bus
88
        localparam      AW=ADDRESS_WIDTH; // Shorthand for ADDRESS_WIDTH
89 69 dgisselq
        //
90 209 dgisselq
        input   wire                    i_clk, i_reset;
91
        //
92
        // The interface with the rest of the CPU
93
        input   wire                    i_new_pc;
94
        input   wire                    i_clear_cache;
95
        input   wire                    i_stall_n;
96
        input   wire    [(AW+1):0]       i_pc;
97
        output  wire    [(BUSW-1):0]     o_insn;
98
        output  wire    [(AW+1):0]       o_pc;
99
        output  wire                    o_valid;
100
        //
101
        // The wishbone bus interface
102
        output  reg                     o_wb_cyc, o_wb_stb;
103
        output  wire                    o_wb_we;
104 69 dgisselq
        output  reg     [(AW-1):0]       o_wb_addr;
105
        output  wire    [(BUSW-1):0]     o_wb_data;
106
        //
107 209 dgisselq
        input   wire                    i_wb_ack, i_wb_stall, i_wb_err;
108
        input   wire    [(BUSW-1):0]     i_wb_data;
109 69 dgisselq
        //
110 209 dgisselq
        // o_illegal will be true if this instruction was the result of a
111
        // bus error (This is also part of the CPU interface)
112 69 dgisselq
        output  reg                     o_illegal;
113 209 dgisselq
        //
114
`ifdef  NOT_YET_READY
115
        input   wire                    i_mmu_ack, i_mmu_we;
116
        input   wire    [(PAW-1):0]      i_mmu_paddr;
117
`endif
118 69 dgisselq
 
119
        // Fixed bus outputs: we read from the bus only, never write.
120
        // Thus the output data is ... irrelevant and don't care.  We set it
121
        // to zero just to set it to something.
122
        assign  o_wb_we = 1'b0;
123
        assign  o_wb_data = 0;
124
 
125 209 dgisselq
`ifdef  NOT_YET_READY
126
        // These wires will be used below as part of the cache invalidation
127
        // routine, should the MMU be used.  This allows us to snoop on the
128
        // physical side of the MMU bus, and invalidate any results should
129
        // we need to do so.
130
        wire                    mmu_inval;
131
        wire    [(PAW-CW-1):0]   mmu_mskaddr;
132
`endif
133
`ifdef  FORMAL
134
        output  wire    [AW-1:0] f_pc_wb;
135
        assign  f_pc_wb = i_pc[AW+1:2];
136
`endif
137
 
138
 
139 176 dgisselq
        wire                    r_v;
140 69 dgisselq
        reg     [(BUSW-1):0]     cache   [0:((1<<CW)-1)];
141 209 dgisselq
        reg     [(AW-CW-1):0]    cache_tags      [0:((1<<(LGLINES))-1)];
142
        reg     [((1<<(LGLINES))-1):0]   valid_mask;
143 69 dgisselq
 
144 209 dgisselq
        reg                     r_v_from_pc, r_v_from_last, r_new_request;
145
        reg                     rvsrc;
146
        wire                    w_v_from_pc, w_v_from_last;
147
        reg     [(AW+1):0]       lastpc;
148
        reg     [(CW-1):0]       wraddr;
149 176 dgisselq
        reg     [(AW-1):CW]     tagvalipc, tagvallst;
150
        wire    [(AW-1):CW]     tagval;
151 209 dgisselq
        wire    [(AW-1):LS]     lasttag;
152 129 dgisselq
        reg                     illegal_valid;
153 209 dgisselq
        reg     [(AW-1):LS]     illegal_cache;
154 69 dgisselq
 
155 176 dgisselq
        // initial      o_i = 32'h76_00_00_00;  // A NOOP instruction
156
        // initial      o_pc = 0;
157
        reg     [(BUSW-1):0]     r_pc_cache, r_last_cache;
158 209 dgisselq
        reg     [(AW+1):0]       r_pc, r_lastpc;
159
        reg                     isrc;
160
        reg     [1:0]            delay;
161
        reg                     svmask, last_ack, needload, last_addr,
162
                                bus_abort;
163
        reg     [(LGLINES-1):0]  saddr;
164
 
165
        wire                    w_advance;
166
        assign  w_advance = (i_new_pc)||((r_v)&&(i_stall_n));
167
 
168
        /////////////////////////////////////////////////
169
        //
170
        // Read the instruction from the cache
171
        //
172
        /////////////////////////////////////////////////
173
        //
174
        //
175
        // We'll read two values from the cache, the first is the value if
176
        // i_pc contains the address we want, the second is the value we'd read
177
        // if lastpc (i.e. $past(i_pc)) was the address we wanted.
178
        initial r_pc = 0;
179
        initial r_lastpc = 0;
180 69 dgisselq
        always @(posedge i_clk)
181 176 dgisselq
        begin
182
                // We don't have the logic to select what to read, we must
183
                // read both the value at i_pc and lastpc.  cache[i_pc] is
184 209 dgisselq
                // the value we return if the last cache request was in the
185
                // cache on the last clock, cacne[lastpc] is the value we
186
                // return if we've been stalled, weren't valid, or had to wait
187
                // a clock or two.
188 176 dgisselq
                //
189 209 dgisselq
                // Part of the issue here is that i_pc is going to increment
190
                // on this clock before we know whether or not the cache entry
191
                // we've just read is valid.  We can't stop this.  Hence, we
192
                // need to read from the lastpc entry.
193
                //
194
                //
195
                // Here we keep track of which answer we want/need.
196
                // If we reported a valid value to the CPU on the last clock,
197
                // and the CPU wasn't stalled, then we want to use i_pc.
198
                // Likewise if the CPU gave us an i_new_pc request, then we'll
199
                // want to return the value associated with reading the cache
200
                // at i_pc.
201
                isrc <= w_advance;
202 69 dgisselq
 
203 209 dgisselq
                // Here we read both cache entries, at i_pc and lastpc.
204
                // We'll select from among these cache possibilities on the
205
                // next clock
206
                r_pc_cache <= cache[i_pc[(CW+1):2]];
207
                r_last_cache <= cache[lastpc[(CW+1):2]];
208
                //
209
                // Let's also register(delay) the r_pc and r_lastpc values
210
                // for the next clock, so we can accurately report the address
211
                // of the cache value we just looked up.
212 176 dgisselq
                r_pc <= i_pc;
213
                r_lastpc <= lastpc;
214
        end
215
 
216 209 dgisselq
        // On our next clock, our result with either be the registered i_pc
217
        // value from the last clock (if isrc), otherwise r_lastpc
218
        assign  o_pc  = (isrc) ? r_pc : r_lastpc;
219
        // The same applies for determining what the next output instruction
220
        // will be.  We just read it in the last clock, now we just need to
221
        // select between the two possibilities we just read.
222
        assign  o_insn= (isrc) ? r_pc_cache : r_last_cache;
223
 
224
 
225
        /////////////////////////////////////////////////
226
        //
227
        // Read the tag value associated with this tcache line
228
        //
229
        /////////////////////////////////////////////////
230
        //
231
        //
232
 
233
        //
234
        // Read the tag value associated with this i_pc value
235 176 dgisselq
        initial tagvalipc = 0;
236
        always @(posedge i_clk)
237 209 dgisselq
                tagvalipc <= cache_tags[i_pc[(CW+1):LS+2]];
238
 
239
 
240
        //
241
        // Read the tag value associated with the lastpc value, from what
242
        // i_pc was when we could not tell if this value was in our cache or
243
        // not, or perhaps from when we determined that i was not in the cache.
244 176 dgisselq
        initial tagvallst = 0;
245
        always @(posedge i_clk)
246 209 dgisselq
                tagvallst <= cache_tags[lastpc[(CW+1):LS+2]];
247 69 dgisselq
 
248 209 dgisselq
        // Select from between these two values on the next clock
249
        assign  tagval = (isrc)?tagvalipc : tagvallst;
250
 
251 69 dgisselq
        // i_pc will only increment when everything else isn't stalled, thus
252
        // we can set it without worrying about that.   Doing this enables
253
        // us to work in spite of stalls.  For example, if the next address
254
        // isn't valid, but the decoder is stalled, get the next address
255
        // anyway.
256
        initial lastpc = 0;
257
        always @(posedge i_clk)
258 209 dgisselq
        if (w_advance)
259
                lastpc <= i_pc;
260 69 dgisselq
 
261 209 dgisselq
        assign  lasttag = lastpc[(AW+1):LS+2];
262 69 dgisselq
 
263 209 dgisselq
        /////////////////////////////////////////////////
264
        //
265
        // Use the tag value to determine if our output instruction will be
266
        // valid.
267
        //
268
        /////////////////////////////////////////////////
269
        //
270
        //
271
        assign  w_v_from_pc = ((i_pc[(AW+1):LS+2] == lasttag)
272
                                &&(tagval == i_pc[(AW+1):CW+2])
273
                                &&(valid_mask[i_pc[(CW+1):LS+2]]));
274
        assign  w_v_from_last = ((tagval == lastpc[(AW+1):CW+2])
275
                                &&(valid_mask[lastpc[(CW+1):LS+2]]));
276 69 dgisselq
 
277
        initial delay = 2'h3;
278
        always @(posedge i_clk)
279 209 dgisselq
        if ((i_reset)||(i_clear_cache)||(w_advance))
280
        begin
281
                // Source our valid signal from i_pc
282
                rvsrc <= 1'b1;
283
                // Delay at least two clocks before declaring that
284
                // we have an invalid result.  This will give us time
285
                // to check the tag value of what's in the cache.
286
                delay <= 2'h2;
287
        end else if ((!r_v)&&(!o_illegal)) begin
288
                // If we aren't sourcing our valid signal from the
289
                // i_pc clock, then we are sourcing it from the
290
                // lastpc clock (one clock later).  If r_v still
291
                // isn't valid, we may need to make a bus request.
292
                // Apply our timer and timeout.
293
                rvsrc <= 1'b0;
294
 
295
                // Delay is two once the bus starts, in case the
296
                // bus transaction needs to be restarted upon completion
297
                // This might happen if, after we start loading the
298
                // cache, we discover a branch.  The cache load will
299
                // still complete, but the branches address needs to be
300
                // the onen we jump to.  This may mean we need to load
301
                // the cache twice.
302
                if (o_wb_cyc)
303 69 dgisselq
                        delay <= 2'h2;
304 209 dgisselq
                else if (delay != 0)
305
                        delay <= delay + 2'b11; // i.e. delay -= 1;
306
        end else begin
307
                // After sourcing our output from i_pc, if it wasn't
308
                // accepted, source the instruction from the lastpc valid
309
                // determination instead
310
                rvsrc <= 1'b0;
311
                if (o_illegal)
312
                        delay <= 2'h2;
313
        end
314
 
315
        wire    w_invalidate_result;
316
        assign  w_invalidate_result = (i_reset)||(i_clear_cache);
317
 
318
        reg     r_prior_illegal;
319
        initial r_prior_illegal = 0;
320
        initial r_new_request = 0;
321
        initial r_v_from_pc = 0;
322
        initial r_v_from_last = 0;
323 176 dgisselq
        always @(posedge i_clk)
324 209 dgisselq
        begin
325
                r_new_request <= w_invalidate_result;
326
                r_v_from_pc   <= (w_v_from_pc)&&(!w_invalidate_result)
327
                                        &&(!o_illegal);
328
                r_v_from_last <= (w_v_from_last)&&(!w_invalidate_result);
329
 
330
                r_prior_illegal <= (o_wb_cyc)&&(i_wb_err);
331
        end
332
 
333
        // Now use rvsrc to determine which of the two valid flags we'll be
334
        // using: r_v_from_pc (the i_pc address), or r_v_from_last (the lastpc
335
        // address)
336
        assign  r_v = ((rvsrc)?(r_v_from_pc):(r_v_from_last))&&(!r_new_request);
337
        assign  o_valid = (((rvsrc)?(r_v_from_pc):(r_v_from_last))
338
                        ||(o_illegal))
339
                        &&(!i_new_pc)&&(!r_prior_illegal);
340
 
341
        /////////////////////////////////////////////////
342
        //
343
        // If the instruction isn't in our cache, then we need to load
344
        // a new cache line from memory.
345
        //
346
        /////////////////////////////////////////////////
347
        //
348
        //
349
        initial needload = 1'b0;
350 176 dgisselq
        always @(posedge i_clk)
351 209 dgisselq
        if ((i_clear_cache)||(o_wb_cyc))
352
                needload <= 1'b0;
353
        else if ((w_advance)&&(!o_illegal))
354
                needload <= 1'b0;
355
        else
356
                needload <= (delay==0)&&(!w_v_from_last)
357
                        // Prevent us from reloading an illegal address
358
                        // (i.e. one that produced a bus error) over and over
359
                        // and over again
360
                        &&((!illegal_valid)
361
                                ||(lastpc[(AW+1):LS+2] != illegal_cache));
362 69 dgisselq
 
363 209 dgisselq
        //
364
        // Working from the rule that you want to keep complex logic out of
365
        // a state machine if possible, we calculate a "last_stb" value one
366
        // clock ahead of time.  Hence, any time a request is accepted, if
367
        // last_stb is also true we'll know we need to drop the strobe line,
368
        // having finished requesting a complete cache  line.
369
        initial last_addr = 1'b0;
370
        always @(posedge i_clk)
371
        if (!o_wb_cyc)
372
                last_addr <= 1'b0;
373
        else if ((o_wb_addr[(LS-1):1] == {(LS-1){1'b1}})
374
                        &&((!i_wb_stall)|(o_wb_addr[0])))
375
                last_addr <= 1'b1;
376 69 dgisselq
 
377 209 dgisselq
        //
378
        // "last_ack" is almost identical to last_addr, save that this
379
        // will be true on the same clock as the last acknowledgment from the
380
        // bus.  The state machine logic will use this to determine when to
381
        // get off the bus and end the wishbone bus cycle.
382 176 dgisselq
        initial last_ack = 1'b0;
383
        always @(posedge i_clk)
384
                last_ack <= (o_wb_cyc)&&(
385 209 dgisselq
                                (wraddr[(LS-1):1]=={(LS-1){1'b1}})
386
                                &&((wraddr[0])||(i_wb_ack)));
387 69 dgisselq
 
388 209 dgisselq
        initial bus_abort = 1'b0;
389 176 dgisselq
        always @(posedge i_clk)
390 209 dgisselq
        if (!o_wb_cyc)
391
                bus_abort <= 1'b0;
392
        else if ((i_clear_cache)||(i_new_pc))
393
                bus_abort <= 1'b1;
394 176 dgisselq
 
395 209 dgisselq
        //
396
        // Here's the difficult piece of state machine logic--the part that
397
        // determines o_wb_cyc and o_wb_stb.  We've already moved most of the
398
        // complicated logic off of this statemachine, calculating it one cycle
399
        // early.  As a result, this is a fairly easy piece of logic.
400 69 dgisselq
        initial o_wb_cyc  = 1'b0;
401
        initial o_wb_stb  = 1'b0;
402
        always @(posedge i_clk)
403 209 dgisselq
        if ((i_reset)||(i_clear_cache))
404
        begin
405
                o_wb_cyc <= 1'b0;
406
                o_wb_stb <= 1'b0;
407
        end else if (o_wb_cyc)
408
        begin
409
                if (i_wb_err)
410 69 dgisselq
                        o_wb_stb <= 1'b0;
411 209 dgisselq
                else if ((o_wb_stb)&&(!i_wb_stall)&&(last_addr))
412
                        o_wb_stb <= 1'b0;
413 69 dgisselq
 
414 209 dgisselq
                if (((i_wb_ack)&&(last_ack))||(i_wb_err))
415
                        o_wb_cyc <= 1'b0;
416 82 dgisselq
 
417 209 dgisselq
        end else if ((needload)&&(!i_new_pc))
418
        begin
419
                o_wb_cyc  <= 1'b1;
420
                o_wb_stb  <= 1'b1;
421
        end
422 69 dgisselq
 
423 209 dgisselq
        // If we are reading from this cache line, then once we get the first
424
        // acknowledgement, this cache line has the new tag value
425
        always @(posedge i_clk)
426
        if ((o_wb_cyc)&&(i_wb_ack))
427
                cache_tags[o_wb_addr[(CW-1):LS]] <= o_wb_addr[(AW-1):CW];
428 69 dgisselq
 
429 209 dgisselq
 
430
        // On each acknowledgment, increment the address we use to write into
431
        // our cache.  Hence, this is the write address into our cache block
432
        // RAM.
433
        initial wraddr    = 0;
434 176 dgisselq
        always @(posedge i_clk)
435 209 dgisselq
        if ((o_wb_cyc)&&(i_wb_ack)&&(!last_ack))
436
                wraddr <= wraddr + 1'b1;
437
        else if (!o_wb_cyc)
438
                wraddr <= { lastpc[(CW+1):LS+2], {(LS){1'b0}} };
439
 
440
        //
441
        // The wishbone request address.  This has meaning anytime o_wb_stb
442
        // is active, and needs to be incremented any time an address is
443
        // accepted--WITH THE EXCEPTION OF THE LAST ADDRESS.  We need to keep
444
        // this steady for that last address, unless the last address returns
445
        // a bus error.  In that case, the whole cache line will be marked as
446
        // invalid--but we'll need the value of this register to know how
447
        // to do that propertly.
448
        initial o_wb_addr = {(AW){1'b0}};
449 176 dgisselq
        always @(posedge i_clk)
450 209 dgisselq
        if ((o_wb_stb)&&(!i_wb_stall)&&(!last_addr))
451
                o_wb_addr[(LS-1):0] <= o_wb_addr[(LS-1):0]+1'b1;
452
        else if (!o_wb_cyc)
453
                o_wb_addr <= { lastpc[(AW+1):LS+2], {(LS){1'b0}} };
454 176 dgisselq
 
455 209 dgisselq
        // Since it is impossible to initialize an array, our cache will start
456
        // up cache uninitialized.  We'll also never get a valid ack without
457
        // cyc being active, although we might get one on the clock after
458
        // cyc was active--so we need to test and gate on whether o_wb_cyc
459
        // is true.
460
        //
461
        // wraddr will advance forward on every clock cycle where ack is true,
462
        // hence we don't need to check i_wb_ack here.  This will work because
463
        // multiple writes to the same address, ending with a valid write,
464
        // will always yield the valid write's value only after our bus cycle
465
        // is over.
466 69 dgisselq
        always @(posedge i_clk)
467 209 dgisselq
        if (o_wb_cyc)
468
                cache[wraddr] <= i_wb_data;
469 69 dgisselq
 
470
        // VMask ... is a section loaded?
471 209 dgisselq
        // Note "svmask".  It's purpose is to delay the valid_mask setting by
472
        // one clock, so that we can insure the right value of the cache is
473
        // loaded before declaring that the cache line is valid.  Without
474
        // this, the cache line would get read, and the instruction would
475
        // read from the last cache line.
476
        initial valid_mask = 0;
477 176 dgisselq
        initial svmask = 1'b0;
478 69 dgisselq
        always @(posedge i_clk)
479 209 dgisselq
        if ((i_reset)||(i_clear_cache))
480
        begin
481
                valid_mask <= 0;
482
                svmask<= 1'b0;
483
        end else begin
484
                svmask <= ((o_wb_cyc)&&(i_wb_ack)&&(last_ack)&&(!bus_abort));
485
 
486
                if (svmask)
487
                        valid_mask[saddr] <= (!bus_abort);
488
                if ((!o_wb_cyc)&&(needload))
489
                        valid_mask[lastpc[(CW+1):LS+2]] <= 1'b0;
490
`ifdef  NOT_YET_READY
491
                //
492
                // MMU code
493
                //
494
                if (mmu_inval)
495
                        valid_mask[mmu_mskadr] <= 1'b0;
496
`endif
497
        end
498
 
499
        always @(posedge i_clk)
500
        if ((o_wb_cyc)&&(i_wb_ack))
501
                saddr <= wraddr[(CW-1):LS];
502
        // MMU code
503
        //
504
        //
505
`ifdef  NOT_YET_READY
506
        parameter       [0:0]     USE_MMU = 1'b1;
507
        generate if (USE_MMU)
508
        begin
509
                reg     [(PAW-CW-1):0]   ptag    [0:((1<<(LGLINES))-1)];
510
                reg                     mmu_pre_inval, r_mmu_inval;
511
                reg     [(PAW-CW-1):0]   mmu_pre_tag, mmu_pre_padr;
512
                reg     [(CW-LS-1):0]    r_mmu_mskadr;
513
 
514
                initial mmu_pre_inval   = 0;
515
                initial mmu_pre_tag     = 0;
516
                initial mmu_pre_padr    = 0;
517
                initial mmu_pre2_inval  = 0;
518
                initial mmu_pre2_mskadr = 0;
519
 
520
                always @(posedge i_clk)
521
                if ((o_wb_cyc)&&(!last_addr)&&(i_mmu_ack))
522
                        ptag[i_mmu_paddr[(CW-1):LS]] <= i_mmu_paddr[(PAW-1):CW];
523
 
524
                always @(posedge i_clk)
525
                if (i_reset)
526 176 dgisselq
                begin
527 209 dgisselq
                        mmu_pre_inval <= 0;
528
                        r_mmu_inval     <= 0;
529
                end else begin
530
                        mmu_pre_inval <= (i_mmu_ack)&&(i_mmu_we);
531
                        r_mmu_inval  <= (mmu_pre_inval)&&(mmu_pre_inval)
532
                                                &&(mmu_pre_tag == mmu_pre_paddr);
533 176 dgisselq
                end
534 209 dgisselq
 
535
                always @(posedge i_clk)
536
                        mmu_pre_tag   <= ptag[i_mmu_paddr[(CW-1):LS]];
537
 
538
                always @(posedge i_clk)
539
                begin
540
                        mmu_pre_padr  <= i_mmu_paddr[(PAW-1):CW];
541
 
542
                        r_mmu_mskadr <= mmu_pre_padr[(PAW-LS-1):(CW-LS)];
543 118 dgisselq
                end
544 69 dgisselq
 
545 209 dgisselq
                assign  mmu_inval  = r_mmu_inval;
546
                assign  mmu_mskadr = r_mmu_mskadr;
547
        end else begin
548
                assign  mmu_inval  = 0;
549
                assign  mmu_mskadr = 0;
550
        end endgenerate
551
`endif
552
 
553
        /////////////////////////////////////////////////
554
        //
555
        // Handle bus errors here.  If a bus read request
556
        // returns an error, then we'll mark the entire
557
        // line as having a (valid) illegal value.
558
        //
559
        /////////////////////////////////////////////////
560
        //
561
        //
562
        //
563
        //
564 69 dgisselq
        initial illegal_cache = 0;
565 71 dgisselq
        initial illegal_valid = 0;
566 69 dgisselq
        always @(posedge i_clk)
567 209 dgisselq
        if ((i_reset)||(i_clear_cache))
568
        begin
569
                illegal_cache <= 0;
570
                illegal_valid <= 0;
571
        end else if ((o_wb_cyc)&&(i_wb_err))
572
        begin
573
                illegal_cache <= o_wb_addr[(AW-1):LS];
574
                illegal_valid <= 1'b1;
575
        end
576
 
577
        initial o_illegal = 1'b0;
578
        always @(posedge i_clk)
579
        if ((i_reset)||(i_clear_cache)||(i_new_pc))
580
                o_illegal <= 1'b0;
581
        else if ((o_illegal)||((o_valid)&&(i_stall_n)))
582
                o_illegal <= 1'b0;
583
        else
584
                o_illegal <= (illegal_valid)
585
                        &&(illegal_cache == lastpc[(AW+1):LS+2]);
586
 
587
`ifdef  FORMAL
588
//
589
//
590
// Generic setup
591
//
592
//
593
`ifdef  PFCACHE
594
`define ASSUME  assume
595
`else
596
`define ASSUME  assert
597
`define STEP_CLOCK
598
`endif
599
 
600
        // Keep track of a flag telling us whether or not $past()
601
        // will return valid results
602
        reg     f_past_valid;
603
        initial f_past_valid = 1'b0;
604
        always @(posedge i_clk)
605
                f_past_valid = 1'b1;
606
        always @(*)
607
        if (!f_past_valid)
608
                `ASSUME(i_reset);
609
 
610
        /////////////////////////////////////////////////
611
        //
612
        //
613
        // Assumptions about our inputs
614
        //
615
        //
616
        /////////////////////////////////////////////////
617
 
618
 
619
`ifdef  PFCACHE
620
        //
621
        // Assume that resets, new-pc commands, and clear-cache commands
622
        // are never more than pulses--one clock wide at most.
623
        //
624
        // It may be that the CPU treats us differently.  We'll only assume
625
        // our solver to this here.
626
        always @(posedge i_clk)
627
        if (!f_past_valid)
628
        begin
629
                if ($past(i_reset))
630
                        assume(!i_reset);
631
                if ($past(i_new_pc))
632
                        assume(!i_new_pc);
633
                if ($past(i_clear_cache))
634
                        assume(!i_clear_cache);
635
        end
636
`endif
637
 
638
        //
639
        // Assume we start from a reset condition
640
        initial `ASSUME(i_reset);
641
 
642
        // Assume that any reset is either accompanied by a new address,
643
        // or a new address immediately follows it.
644
        always @(posedge i_clk)
645
        if ((f_past_valid)&&($past(i_reset)))
646
                `ASSUME(i_new_pc);
647
        //
648
        // Let's make some assumptions about how long it takes our
649
        // phantom bus and phantom CPU to respond.
650
        //
651
        // These delays need to be long enough to flush out any potential
652
        // errors, yet still short enough that the formal method doesn't
653
        // take forever to solve.
654
        //
655
        localparam      F_CPU_DELAY = 4;
656
        reg     [4:0]    f_cpu_delay;
657
 
658
        // Now, let's repeat this bit but now looking at the delay the CPU
659
        // takes to accept an instruction.
660
        always @(posedge i_clk)
661
        // If no instruction is ready, then keep our counter at zero
662
        if ((!o_valid)||(i_stall_n))
663
                f_cpu_delay <= 0;
664
        else
665
                // Otherwise, count the clocks the CPU takes to respond
666
                f_cpu_delay <= f_cpu_delay + 1'b1;
667
 
668
`ifdef  PFCACHE
669
        always @(posedge i_clk)
670
                assume(f_cpu_delay < F_CPU_DELAY);
671
`endif
672
 
673
        always @(posedge i_clk)
674
        if ($past(i_reset || i_clear_cache))
675
                assume(i_stall_n);
676
        else if ($past(i_stall_n && !o_valid))
677
                assume(i_stall_n);
678
        else if (i_new_pc)
679
                assume(i_stall_n);
680
 
681
        /////////////////////////////////////////////////
682
        //
683
        //
684
        // Assertions about our outputs
685
        //
686
        //
687
        /////////////////////////////////////////////////
688
 
689
        localparam      F_LGDEPTH=LS+1;
690
        wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
691
 
692
        fwb_master #(.AW(AW), .DW(BUSW), .F_LGDEPTH(F_LGDEPTH),
693
                        .F_MAX_STALL(2), .F_MAX_ACK_DELAY(3),
694
                        .F_MAX_REQUESTS(1<<LS), .F_OPT_SOURCE(1),
695
                        .F_OPT_RMW_BUS_OPTION(0),
696
                        .F_OPT_DISCONTINUOUS(0))
697
                f_wbm(i_clk, i_reset,
698
                        o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, 4'h0,
699
                        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
700
                        f_nreqs, f_nacks, f_outstanding);
701
 
702
        // writes are also illegal for a prefetch.
703
        always @(posedge i_clk)
704
        if (o_wb_stb)
705
                assert(!o_wb_we);
706
 
707
        always @(posedge i_clk)
708
        begin
709
                assert(f_nreqs <= (1<<LS));
710
                if ((o_wb_cyc)&&(o_wb_stb))
711
                        assert(f_nreqs == o_wb_addr[(LS-1):0]);
712
                if ((f_past_valid)&&($past(o_wb_cyc))
713
                        &&(!o_wb_stb)&&(!$past(i_wb_err || i_reset || i_clear_cache)))
714
                        assert(f_nreqs == (1<<LS));
715
        end
716
 
717
        always @(posedge i_clk)
718
        if (f_past_valid)
719
        begin
720
                if ((!o_wb_cyc)&&($past(o_wb_cyc))&&(!$past(i_reset))
721
                                &&(!$past(i_clear_cache)) &&(!$past(i_wb_err)))
722
                        assert(f_nacks == (1<<LS));
723
                else if (o_wb_cyc)
724
                        assert(f_nacks[(LS-1):0] == wraddr[(LS-1):0]);
725
        end
726
 
727
        // The last-ack line
728
        always @(posedge i_clk)
729
        if (o_wb_cyc)
730
                assert(last_ack == (f_nacks == ((1<<LS)-1)));
731
 
732
        // The valid line for whats being read
733
        always @(posedge i_clk)
734
        if (o_wb_cyc)
735
                assert(!valid_mask[o_wb_addr[CW-1:LS]]);
736
 
737
        always @(posedge i_clk)
738
        if ((illegal_valid)&&(o_wb_cyc))
739
                assert(o_wb_addr[AW-1:LS] != illegal_cache);
740
 
741
        reg     [((1<<(LGLINES))-1):0]   f_past_valid_mask;
742
        initial f_past_valid_mask = 0;
743
        always @(posedge i_clk)
744
                f_past_valid_mask = valid_mask;
745
 
746
        always @(posedge i_clk)
747
        if ((o_valid)&&($past(!o_valid || !o_illegal)))
748
                assert((!o_wb_cyc)
749
                        ||(o_wb_addr[AW-1:LS] != o_pc[AW+1:LS+2]));
750
        always @(posedge i_clk)
751
        if (illegal_valid)
752
        begin
753
                assert((!o_wb_cyc)
754
                        ||(o_wb_addr[AW-1:LS] != illegal_cache));
755
 
756
                // The illegal cache line should never be valid within our
757
                // cache
758
                assert((!valid_mask[illegal_cache[CW-1:LS]])
759
                        ||(cache_tags[illegal_cache[CW-1:LS]]
760
                                        != illegal_cache[AW-1:CW]));
761
        end
762
 
763
        /////////////////////////////////////////////////////
764
        //
765
        //
766
        // Assertions about our return responses to the CPU
767
        //
768
        //
769
        /////////////////////////////////////////////////////
770
 
771
 
772
        always @(posedge i_clk)
773
        if ((f_past_valid)&&($past(o_wb_cyc)))
774
                assert(o_wb_addr[(AW-1):LS] == $past(o_wb_addr[(AW-1):LS]));
775
 
776
        // Consider it invalid to present the CPU with the same instruction
777
        // twice in a row.
778
        always @(posedge i_clk)
779
        if ((f_past_valid)&&($past(o_valid))&&($past(i_stall_n))&&(o_valid))
780
                assert(o_pc != $past(o_pc));
781
 
782
        always @(posedge i_clk)
783
        if (o_valid)
784
        begin
785
                if (!o_illegal)
786 71 dgisselq
                begin
787 209 dgisselq
                        assert(cache_tags[o_pc[(CW+1):LS+2]] == o_pc[(AW+1):CW+2]);
788
                        assert(valid_mask[o_pc[(CW+1):LS+2]] || (o_illegal));
789
                        assert(o_insn == cache[o_pc[(CW+1):2]]);
790
                        assert((!illegal_valid)
791
                                ||((illegal_cache != o_pc[(AW+1):LS+2])));
792 71 dgisselq
                end
793 69 dgisselq
 
794 209 dgisselq
                assert(o_illegal == ($past(illegal_valid)
795
                                &&($past(illegal_cache)== o_pc[(AW+1):LS+2])));
796
        end
797
 
798
        always @(*)
799
        begin
800
                `ASSUME(i_pc[1:0] == 2'b00);
801
                assert(o_pc[1:0] == 2'b00);
802
                assert(r_pc[1:0] == 2'b00);
803
                assert(r_lastpc[1:0] == 2'b00);
804
        end
805
 
806
        reg     [(AW+1):0]       f_next_pc;
807
 
808 69 dgisselq
        always @(posedge i_clk)
809 209 dgisselq
        if ((f_past_valid)&&(!$past(i_reset)))
810
        begin
811
                if (isrc)
812
                        assert(lastpc == r_pc);
813 71 dgisselq
                else
814 209 dgisselq
                        assert(lastpc + 4== r_pc);
815
        end
816 69 dgisselq
 
817 209 dgisselq
        always @(posedge i_clk)
818
        if (i_new_pc)
819
                f_next_pc <= { i_pc[AW+1:2] + 1'b1, 2'b00 };
820
        else if ((i_stall_n)&&(r_v))
821
                f_next_pc <= { i_pc[AW+1:2] + 1'b1, 2'b00 };
822
        always @(*)
823
        if (!i_new_pc)
824
                `ASSUME(i_pc == f_next_pc);
825
 
826
        always @(posedge i_clk)
827
        if ((f_past_valid)&&(o_valid)&&($past(o_valid))
828
                &&(!$past(i_reset))
829
                &&(!$past(i_new_pc))
830
                &&(!$past(i_stall_n))
831
                &&(!o_illegal))
832
        begin
833
                assert(cache_tags[o_pc[(CW+1):LS+2]] == o_pc[(AW+1):CW+2]);
834
        end
835
 
836
        //
837
        // If an instruction is accepted, we should *always* move on to another
838
        // instruction.  The only exception is following an i_new_pc (or
839
        // other invalidator), at which point the next instruction should
840
        // be invalid.
841
        always @(posedge i_clk)
842
        if ((f_past_valid)&&($past(o_valid))&&($past(i_stall_n)))
843
        begin
844
                // Should always advance the instruction
845
                assert((!o_valid)||(o_pc != $past(o_pc)));
846
        end
847
 
848
        //
849
        // Once an instruction becomes valid, it should never become invalid
850
        // unless there's been a request for a new instruction.
851
        always @(posedge i_clk)
852
        if ((f_past_valid)&&($past(!i_reset && !i_clear_cache && !i_new_pc))
853
                &&($past(o_valid && !i_stall_n))
854
                &&(!i_new_pc))
855
        begin
856
                if ((!$past(o_illegal))&&(!$past(o_wb_cyc && i_wb_err)))
857
                begin
858
                        assert(o_valid);
859
                        assert($stable(o_illegal));
860
                        assert($stable(o_insn));
861
                end else
862
                        assert((o_illegal)||(!o_valid));
863
        end
864
`ifdef  PFCACHE
865
        /////////////////////////////////////////////////////
866
        //
867
        //
868
        // Assertions associated with a response to a known
869
        // address request
870
        //
871
        //
872
        /////////////////////////////////////////////////////
873
 
874
 
875
        (* anyconst *)  reg     [AW:0]           f_const_addr;
876
        (* anyconst *)  reg     [BUSW-1:0]       f_const_insn;
877
 
878
        wire            f_this_pc, f_this_insn, f_this_data, f_this_line,
879
                        f_this_ack, f_this_tag; // f_this_addr;
880
        assign  f_this_pc   = (o_pc == { f_const_addr[AW-1:0], 2'b00 });
881
        // assign       f_this_addr = (o_wb_addr == f_const_addr[AW-1:0] );
882
        assign  f_this_insn = (o_insn == f_const_insn);
883
        assign  f_this_data = (i_wb_data == f_const_insn);
884
        assign  f_this_line = (o_wb_addr[AW-1:LS] == f_const_addr[AW-1:LS]);
885
        assign  f_this_ack  = (f_this_line)&&(f_nacks == f_const_addr[LS-1:0]);
886
        assign  f_this_tag  = (tagval == f_const_addr[AW-1:CW]);
887
 
888
        always @(posedge i_clk)
889
        if ((o_valid)&&(f_this_pc)&&(!$past(o_illegal)))
890
        begin
891
                assert(o_illegal == f_const_addr[AW]);
892
                if (!o_illegal)
893
                begin
894
                        assert(f_this_insn);
895
                        assert(f_this_tag);
896
                end
897
        end
898
 
899
        always @(*)
900
        if ((valid_mask[f_const_addr[CW-1:LS]])
901
                        &&(cache_tags[f_const_addr[(CW-1):LS]]==f_const_addr[AW-1:CW]))
902
                assert(f_const_insn == cache[f_const_addr[CW-1:0]]);
903
        else if ((o_wb_cyc)&&(o_wb_addr[AW-1:LS] == f_const_addr[AW-1:LS])
904
                                &&(f_nacks > f_const_addr[LS-1:0]))
905
        begin
906
                assert(f_const_insn == cache[f_const_addr[CW-1:0]]);
907
        end
908
 
909
        always @(*)
910
        if (o_wb_cyc)
911
                assert(wraddr[CW-1:LS] == o_wb_addr[CW-1:LS]);
912
 
913
        always @(*)
914
        if (!f_const_addr[AW])
915
                assert((!illegal_valid)
916
                        ||(illegal_cache != f_const_addr[AW-1:LS]));
917
        else
918
                assert((cache_tags[f_const_addr[CW-1:LS]]!=f_const_addr[AW-1:CW])
919
                        ||(!valid_mask[f_const_addr[CW-1:LS]]));
920
 
921
        always @(*)
922
        if ((f_this_line)&&(o_wb_cyc))
923
        begin
924
                if (f_const_addr[AW])
925
                        assume(!i_wb_ack);
926
                else
927
                        assume(!i_wb_err);
928
 
929
                if ((f_this_ack)&&(i_wb_ack))
930
                        assume(f_this_data);
931
        end
932
 
933
        always @(*)
934
        if ((f_this_line)&&(!f_const_addr[AW]))
935
                assume(!i_wb_err);
936
 
937
        always @(*)
938
        if (!f_const_addr[AW])
939
                assume((!valid_mask[f_const_addr[CW-1:LS]])
940
                        ||(cache_tags[f_const_addr[CW-1:LS]] != f_const_addr[AW-1:CW]));
941
`endif
942
 
943
        //
944
        //
945
        // Cover properties
946
        //
947
        //
948
        reg     f_valid_legal;
949
        always @(*)
950
                f_valid_legal = o_valid && (!o_illegal);
951
        always @(posedge i_clk)         // Trace 0
952
                cover((o_valid)&&( o_illegal));
953
        always @(posedge i_clk)         // Trace 1
954
                cover(f_valid_legal);
955
        always @(posedge i_clk)         // Trace 2
956
                cover((f_valid_legal)
957
                        &&($past(!o_valid && !i_new_pc))
958
                        &&($past(i_new_pc,2)));
959
        always @(posedge i_clk)         // Trace 3
960
                cover((f_valid_legal)&&($past(i_stall_n))&&($past(i_new_pc)));
961
        always @(posedge i_clk)         // Trace 4
962
                cover((f_valid_legal)&&($past(f_valid_legal && i_stall_n)));
963
        always @(posedge i_clk)         // Trace 5
964
                cover((f_valid_legal)
965
                        &&($past(f_valid_legal && i_stall_n))
966
                        &&($past(f_valid_legal && i_stall_n,2))
967
                        &&($past(f_valid_legal && i_stall_n,3)));
968
        always @(posedge i_clk)         // Trace 6
969
                cover((f_valid_legal)
970
                        &&($past(f_valid_legal && i_stall_n))
971
                        &&($past(f_valid_legal && i_stall_n,2))
972
                        &&($past(!o_illegal && i_stall_n && i_new_pc,3))
973
                        &&($past(f_valid_legal && i_stall_n,4))
974
                        &&($past(f_valid_legal && i_stall_n,5))
975
                        &&($past(f_valid_legal && i_stall_n,6)));
976
 
977
`endif  // FORMAL
978 69 dgisselq
endmodule

powered by: WebSVN 2.1.0

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