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

Subversion Repositories zipcpu

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

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 205 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    dblfetch.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     This is one step beyond the simplest instruction fetch,
8
//              prefetch.v.  dblfetch.v uses memory pipelining to fetch two
9 209 dgisselq
//      (or more) instruction words in one bus cycle.  If the CPU consumes
10
//      either of these before the bus cycle completes, a new request will be
11
//      made of the bus.  In this way, we can keep the CPU filled in spite
12
//      of a (potentially) slow memory operation.  The bus request will end
13
//      when both requests have been sent and both result locations are empty.
14 205 dgisselq
//
15 209 dgisselq
//      This routine is designed to be a touch faster than the single
16
//      instruction prefetch (prefetch.v), although not as fast as the
17
//      prefetch and cache approach found elsewhere (pfcache.v).
18 205 dgisselq
//
19 209 dgisselq
//      20180222: Completely rebuilt.
20 205 dgisselq
//
21
// Creator:     Dan Gisselquist, Ph.D.
22
//              Gisselquist Technology, LLC
23
//
24
////////////////////////////////////////////////////////////////////////////////
25
//
26 209 dgisselq
// Copyright (C) 2017-2019, Gisselquist Technology, LLC
27 205 dgisselq
//
28
// This program is free software (firmware): you can redistribute it and/or
29
// modify it under the terms of  the GNU General Public License as published
30
// by the Free Software Foundation, either version 3 of the License, or (at
31
// your option) any later version.
32
//
33
// This program is distributed in the hope that it will be useful, but WITHOUT
34
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
35
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
36
// for more details.
37
//
38
// You should have received a copy of the GNU General Public License along
39
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
40
// target there if the PDF file isn't present.)  If not, see
41
// <http://www.gnu.org/licenses/> for a copy.
42
//
43
// License:     GPL, v3, as defined and found on www.gnu.org,
44
//              http://www.gnu.org/licenses/gpl.html
45
//
46
//
47
////////////////////////////////////////////////////////////////////////////////
48
//
49
//
50 209 dgisselq
`default_nettype        none
51
//
52
module  dblfetch(i_clk, i_reset, i_new_pc, i_clear_cache,
53
                        i_stall_n, i_pc, o_insn, o_pc, o_valid,
54 205 dgisselq
                o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
55
                        i_wb_ack, i_wb_stall, i_wb_err, i_wb_data,
56
                o_illegal);
57 209 dgisselq
        parameter               ADDRESS_WIDTH=30, AUX_WIDTH = 1;
58
        localparam              AW=ADDRESS_WIDTH, DW = 32;
59
        input   wire                    i_clk, i_reset, i_new_pc, i_clear_cache,
60 205 dgisselq
                                                i_stall_n;
61 209 dgisselq
        input   wire    [(AW+1):0]       i_pc;
62
        output  reg     [(DW-1):0]       o_insn;
63
        output  reg     [(AW+1):0]       o_pc;
64
        output  reg                     o_valid;
65 205 dgisselq
        // Wishbone outputs
66
        output  reg                     o_wb_cyc, o_wb_stb;
67
        output  wire                    o_wb_we;
68
        output  reg     [(AW-1):0]       o_wb_addr;
69 209 dgisselq
        output  wire    [(DW-1):0]       o_wb_data;
70 205 dgisselq
        // And return inputs
71 209 dgisselq
        input   wire                    i_wb_ack, i_wb_stall, i_wb_err;
72
        input   wire    [(DW-1):0]       i_wb_data;
73 205 dgisselq
        // And ... the result if we got an error
74
        output  reg             o_illegal;
75
 
76
        assign  o_wb_we = 1'b0;
77
        assign  o_wb_data = 32'h0000;
78
 
79 209 dgisselq
        reg     last_stb, invalid_bus_cycle;
80 205 dgisselq
 
81 209 dgisselq
        reg     [(DW-1):0]       cache_word;
82
        reg                     cache_valid;
83
        reg     [1:0]            inflight;
84
        reg                     cache_illegal;
85 205 dgisselq
 
86
        initial o_wb_cyc = 1'b0;
87
        initial o_wb_stb = 1'b0;
88
        always @(posedge i_clk)
89 209 dgisselq
                if ((i_reset)||((o_wb_cyc)&&(i_wb_err)))
90 205 dgisselq
                begin
91
                        o_wb_cyc <= 1'b0;
92
                        o_wb_stb <= 1'b0;
93
                end else if (o_wb_cyc)
94
                begin
95 209 dgisselq
                        if ((!o_wb_stb)||(!i_wb_stall))
96
                                o_wb_stb <= (!last_stb);
97 205 dgisselq
 
98 209 dgisselq
                        // Relase the bus on the second ack
99
                        if (((i_wb_ack)&&(!o_wb_stb)&&(inflight<=1))
100
                                ||((!o_wb_stb)&&(inflight == 0))
101
                                // Or any new transaction request
102
                                ||((i_new_pc)||(i_clear_cache)))
103 205 dgisselq
                        begin
104
                                o_wb_cyc <= 1'b0;
105
                                o_wb_stb <= 1'b0;
106
                        end
107
 
108 209 dgisselq
                end else if ((i_new_pc)||(invalid_bus_cycle)
109
                        ||((o_valid)&&(i_stall_n)&&(!o_illegal)))
110 205 dgisselq
                begin
111 209 dgisselq
                        // Initiate a bus cycle if ... the last bus cycle was
112
                        // aborted (bus error or new_pc), we've been given a
113
                        // new PC to go get, or we just exhausted our one
114
                        // instruction cache
115 205 dgisselq
                        o_wb_cyc <= 1'b1;
116
                        o_wb_stb <= 1'b1;
117
                end
118
 
119 209 dgisselq
        initial inflight = 2'b00;
120 205 dgisselq
        always @(posedge i_clk)
121 209 dgisselq
        if (!o_wb_cyc)
122
                inflight <= 2'b00;
123
        else begin
124
                case({ ((o_wb_stb)&&(!i_wb_stall)), i_wb_ack })
125
                2'b01:  inflight <= inflight - 1'b1;
126
                2'b10:  inflight <= inflight + 1'b1;
127
                // If neither ack nor request, then no change.  Likewise
128
                // if we have both an ack and a request, there's no change
129
                // in the number of requests in flight.
130
                default: begin end
131
                endcase
132
        end
133 205 dgisselq
 
134 209 dgisselq
        always @(*)
135
                last_stb = (inflight != 2'b00)||((o_valid)&&(!i_stall_n));
136 205 dgisselq
 
137
        initial invalid_bus_cycle = 1'b0;
138
        always @(posedge i_clk)
139 209 dgisselq
                if ((o_wb_cyc)&&(i_new_pc))
140 205 dgisselq
                        invalid_bus_cycle <= 1'b1;
141
                else if (!o_wb_cyc)
142
                        invalid_bus_cycle <= 1'b0;
143
 
144
        initial o_wb_addr = {(AW){1'b1}};
145
        always @(posedge i_clk)
146
                if (i_new_pc)
147 209 dgisselq
                        o_wb_addr <= i_pc[AW+1:2];
148
                else if ((o_wb_stb)&&(!i_wb_stall))
149 205 dgisselq
                        o_wb_addr <= o_wb_addr + 1'b1;
150
 
151 209 dgisselq
        //////////////////
152
        //
153
        // Now for the immediate output word to the CPU
154
        //
155
        //////////////////
156
 
157
        initial o_valid = 1'b0;
158 205 dgisselq
        always @(posedge i_clk)
159 209 dgisselq
                if ((i_reset)||(i_new_pc)||(i_clear_cache))
160
                        o_valid <= 1'b0;
161
                else if ((o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
162
                        o_valid <= 1'b1;
163
                else if (i_stall_n)
164
                        o_valid <= cache_valid;
165 205 dgisselq
 
166
        always @(posedge i_clk)
167 209 dgisselq
        if ((!o_valid)||(i_stall_n))
168
        begin
169
                if (cache_valid)
170
                        o_insn <= cache_word;
171
                else
172
                        o_insn <= i_wb_data;
173
        end
174 205 dgisselq
 
175 209 dgisselq
        initial o_pc[1:0] = 2'b00;
176 205 dgisselq
        always @(posedge i_clk)
177 209 dgisselq
        if (i_new_pc)
178
                o_pc <= i_pc;
179
        else if ((o_valid)&&(i_stall_n))
180
                o_pc[AW+1:2] <= o_pc[AW+1:2] + 1'b1;
181 205 dgisselq
 
182 209 dgisselq
        initial o_illegal = 1'b0;
183 205 dgisselq
        always @(posedge i_clk)
184 209 dgisselq
                if ((i_reset)||(i_new_pc)||(i_clear_cache))
185
                        o_illegal <= 1'b0;
186
                else if ((!o_valid)||(i_stall_n))
187
                begin
188
                        if (cache_valid)
189
                                o_illegal <= (o_illegal)||(cache_illegal);
190
                        else if ((o_wb_cyc)&&(i_wb_err))
191
                                o_illegal <= 1'b1;
192
                end
193
 
194
 
195
        //////////////////
196
        //
197
        // Now for the output/cached word
198
        //
199
        //////////////////
200
 
201
        initial cache_valid = 1'b0;
202
        always @(posedge i_clk)
203
                if ((i_reset)||(i_new_pc)||(i_clear_cache))
204
                        cache_valid <= 1'b0;
205 205 dgisselq
                else begin
206 209 dgisselq
                        if ((o_valid)&&(o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
207
                                cache_valid <= (!i_stall_n)||(cache_valid);
208
                        else if (i_stall_n)
209
                                cache_valid <= 1'b0;
210 205 dgisselq
                end
211
 
212
        always @(posedge i_clk)
213 209 dgisselq
                if ((o_wb_cyc)&&(i_wb_ack))
214
                        cache_word <= i_wb_data;
215
 
216
        initial cache_illegal = 1'b0;
217
        always @(posedge i_clk)
218
        if ((i_reset)||(i_clear_cache)||(i_new_pc))
219
                cache_illegal <= 1'b0;
220
        else if ((o_wb_cyc)&&(i_wb_err)&&(o_valid)&&(!i_stall_n))
221
                cache_illegal <= 1'b1;
222
//
223
// Some of these properties can be done in yosys-smtbmc, *or* Verilator
224
//
225
// Ver1lator is different from yosys, however, in that Verilator doesn't support
226
// the $past() directive.  Further, any `assume`'s turn into `assert()`s
227
// within Verilator.  We can use this to help prove that the properties
228
// of interest truly hold, and that any contracts we create or assumptions we
229
// make truly hold in practice (i.e. in simulation).
230
//
231
`ifdef  FORMAL
232
`define VERILATOR_FORMAL
233
`else
234
`ifdef  VERILATOR
235
//
236
// Define VERILATOR_FORMAL here to have Verilator check your formal properties
237
// during simulation.  assert() and assume() statements will both have the
238
// same effect within VERILATOR of causing your simulation to suddenly end.
239
//
240
// I have this property commented because it only works on the newest versions
241
// of Verilator (3.9 something and later), and I tend to still use Verilator
242
// 3.874.
243
//
244
// `define      VERILATOR_FORMAL
245
`endif
246
`endif
247
 
248
`ifdef  VERILATOR_FORMAL
249
        // Keep track of a flag telling us whether or not $past()
250
        // will return valid results
251
        reg     f_past_valid;
252
        initial f_past_valid = 1'b0;
253
        always @(posedge i_clk)
254
                f_past_valid = 1'b1;
255
 
256
        // Keep track of some alternatives to $past that can still be used
257
        // in a VERILATOR environment
258
        reg     f_past_reset, f_past_clear_cache, f_past_o_valid,
259
                f_past_stall_n;
260
 
261
        initial f_past_reset = 1'b1;
262
        initial f_past_clear_cache = 1'b0;
263
        initial f_past_o_valid = 1'b0;
264
        initial f_past_stall_n = 1'b1;
265
        always @(posedge i_clk)
266
        begin
267
                f_past_reset       <= i_reset;
268
                f_past_clear_cache <= i_clear_cache;
269
                f_past_o_valid     <= o_valid;
270
                f_past_stall_n     <= i_stall_n;
271
        end
272
`endif
273
 
274
`ifdef  FORMAL
275
//
276
//
277
// Generic setup
278
//
279
//
280
`ifdef  DBLFETCH
281
`define ASSUME  assume
282
`else
283
`define ASSUME  assert
284
`endif
285
 
286
        /////////////////////////////////////////////////
287
        //
288
        //
289
        // Assumptions about our inputs
290
        //
291
        //
292
        /////////////////////////////////////////////////
293
 
294
        always @(*)
295
        if (!f_past_valid)
296
                `ASSUME(i_reset);
297
 
298
        //
299
        // Assume that resets, new-pc commands, and clear-cache commands
300
        // are never more than pulses--one clock wide at most.
301
        //
302
        // It may be that the CPU treats us differently.  We'll only restrict
303
        // our solver to this here.
304
/*
305
        always @(posedge i_clk)
306
        if (f_past_valid)
307
        begin
308
                if (f_past_reset)
309
                        restrict(!i_reset);
310
                if ($past(i_new_pc))
311
                        restrict(!i_new_pc);
312
        end
313
*/
314
 
315
        //
316
        // Assume we start from a reset condition
317
        initial assume(i_reset);
318
 
319
        /////////////////////////////////////////////////
320
        //
321
        //
322
        // Wishbone bus properties
323
        //
324
        //
325
        /////////////////////////////////////////////////
326
 
327
        localparam      F_LGDEPTH=2;
328
        wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
329
 
330
        //
331
        // Add a bunch of wishbone-based asserts
332
        fwb_master #(.AW(AW), .DW(DW), .F_LGDEPTH(F_LGDEPTH),
333
                                .F_MAX_STALL(2),
334
                                .F_MAX_REQUESTS(0), .F_OPT_SOURCE(1),
335
                                .F_OPT_RMW_BUS_OPTION(1),
336
                                .F_OPT_DISCONTINUOUS(0))
337
                f_wbm(i_clk, i_reset,
338
                        o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, 4'h0,
339
                        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
340
                        f_nreqs, f_nacks, f_outstanding);
341
 
342
`endif
343
 
344
//
345
// Now, apply the following to Verilator *or* yosys-smtbmc
346
//
347
`ifdef  VERILATOR_FORMAL
348
        /////////////////////////////////////////////////
349
        //
350
        //
351
        // Assumptions about our interaction with the CPU
352
        //
353
        //
354
        /////////////////////////////////////////////////
355
 
356
        // Assume that any reset is either accompanied by a new address,
357
        // or a new address immediately follows it.
358
        always @(posedge i_clk)
359
                if ((f_past_valid)&&(f_past_reset))
360
                        assume(i_new_pc);
361
 
362
        always @(posedge i_clk)
363
        if (f_past_clear_cache)
364
                assume(!i_clear_cache);
365
 
366
        //
367
        //
368
        // The bottom two bits of the PC address register are always zero.
369
        // They are there to make examining traces easier, but I expect
370
        // the synthesis tool to remove them.
371
        //
372
        always @(*)
373
                assume(i_pc[1:0] == 2'b00);
374
 
375
        // Some things to know from the CPU ... there will always be a
376
        // i_new_pc request following any reset
377
        always @(posedge i_clk)
378
                if ((f_past_valid)&&(f_past_reset))
379
                        assume(i_new_pc);
380
 
381
        // There will also be a i_new_pc request following any request to clear
382
        // the cache.
383
        always @(posedge i_clk)
384
                if ((f_past_valid)&&(f_past_clear_cache))
385
                        assume(i_new_pc);
386
 
387
        always @(posedge i_clk)
388
        if (f_past_clear_cache)
389
                assume(!i_clear_cache);
390
 
391
        always @(*)
392
                assume(i_pc[1:0] == 2'b00);
393
`endif
394
 
395
`ifdef  FORMAL
396
        //
397
        // Let's make some assumptions about how long it takes our phantom
398
        // (i.e. assumed) CPU to respond.
399
        //
400
        // This delay needs to be long enough to flush out any potential
401
        // errors, yet still short enough that the formal method doesn't
402
        // take forever to solve.
403
        //
404
`ifdef  DBLFETCH
405
        localparam      F_CPU_DELAY = 4;
406
        reg     [4:0]    f_cpu_delay;
407
 
408
        // Now, let's look at the delay the CPU takes to accept an instruction.
409
        always @(posedge i_clk)
410
                // If no instruction is ready, then keep our counter at zero
411
                if ((!o_valid)||(i_stall_n))
412
                        f_cpu_delay <= 0;
413 205 dgisselq
                else
414 209 dgisselq
                        // Otherwise, count the clocks the CPU takes to respond
415
                        f_cpu_delay <= f_cpu_delay + 1'b1;
416 205 dgisselq
 
417
        always @(posedge i_clk)
418 209 dgisselq
                assume(f_cpu_delay < F_CPU_DELAY);
419
`endif
420 205 dgisselq
 
421
 
422 209 dgisselq
 
423
        /////////////////////////////////////////////////
424
        //
425
        //
426
        // Assertions about our outputs
427
        //
428
        //
429
        /////////////////////////////////////////////////
430 205 dgisselq
        always @(posedge i_clk)
431 209 dgisselq
        if ((f_past_valid)&&($past(o_wb_stb))&&(!$past(i_wb_stall))
432
                        &&(!$past(i_new_pc)))
433
                assert(o_wb_addr <= $past(o_wb_addr)+1'b1);
434 205 dgisselq
 
435 209 dgisselq
        //
436
        // Assertions about our return responses to the CPU
437
        //
438
        always @(posedge i_clk)
439
        if ((f_past_valid)&&(!$past(i_reset))
440
                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))
441
                        &&($past(o_valid))&&(!$past(i_stall_n)))
442
        begin
443
                assert($stable(o_pc));
444
                assert($stable(o_insn));
445
                assert($stable(o_valid));
446
                assert($stable(o_illegal));
447
        end
448
 
449
        // The same is true of the cache as well.
450
        always @(posedge i_clk)
451
        if ((f_past_valid)&&(!$past(i_reset))
452
                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))
453
                        &&($past(o_valid))&&(!$past(i_stall_n))
454
                        &&($past(cache_valid)))
455
        begin
456
                assert($stable(cache_valid));
457
                assert($stable(cache_word));
458
                assert($stable(cache_illegal));
459
        end
460
 
461
        // Consider it invalid to present the CPU with the same instruction
462
        // twice in a row.  Any effort to present the CPU with the same
463
        // instruction twice in a row must go through i_new_pc, and thus a
464
        // new bus cycle--hence the assertion below makes sense.
465
        always @(posedge i_clk)
466
        if ((f_past_valid)&&(!$past(i_new_pc))
467
                        &&($past(o_valid))&&($past(i_stall_n)))
468
                assert(o_pc[AW+1:2] == $past(o_pc[AW+1:2])+1'b1);
469
 
470
 
471
        //
472
        // As with i_pc[1:0], the bottom two bits of the address are unused.
473
        // Let's assert here that they remain zero.
474
        always @(*)
475
                assert(o_pc[1:0] == 2'b00);
476
 
477
        always @(posedge i_clk)
478
        if ((f_past_valid)&&(!$past(i_reset))
479
                        &&(!$past(i_new_pc))
480
                        &&(!$past(i_clear_cache))
481
                        &&($past(o_wb_cyc))&&($past(i_wb_err)))
482
                assert( ((o_valid)&&(o_illegal))
483
                        ||((cache_valid)&&(cache_illegal)) );
484
 
485
        always @(posedge i_clk)
486
        if ((f_past_valid)&&(!$past(o_illegal))&&(o_illegal))
487
                assert(o_valid);
488
 
489
        always @(posedge i_clk)
490
        if ((f_past_valid)&&(!$past(cache_illegal))&&(!cache_valid))
491
                assert(!cache_illegal);
492
 
493
        always @(posedge i_clk)
494
        if ((f_past_valid)&&($past(i_new_pc)))
495
                assert(!o_valid);
496
 
497
        always @(posedge i_clk)
498
        if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_clear_cache))
499
                        &&($past(o_valid))&&(!o_valid)&&(!o_illegal))
500
                assert((o_wb_cyc)||(invalid_bus_cycle));
501
 
502
        /////////////////////////////////////////////////
503
        //
504
        //
505
        // Our "contract" with the CPU
506
        //
507
        //
508
        /////////////////////////////////////////////////
509
        //
510
        // For any particular address, that address is associated with an
511
        // instruction and a flag regarding whether or not it is illegal.
512
        //
513
        // Any attempt to return to the CPU a value from this address,
514
        // must return the value and the illegal flag.
515
        //
516
        (* anyconst *) reg      [AW-1:0] f_const_addr;
517
        (* anyconst *) reg      [DW-1:0] f_const_insn;
518
        (* anyconst *) reg                      f_const_illegal;
519
 
520
        //
521
        // While these wires may seem like overkill, and while they make the
522
        // following logic perhaps a bit more obscure, these predicates make
523
        // it easier to follow the complex logic on a scope.  They don't
524
        // affect anything synthesized.
525
        //
526
        wire    f_this_addr, f_this_pc, f_this_req, f_this_data,
527
                f_this_insn;
528
 
529
        assign  f_this_addr = (o_wb_addr ==   f_const_addr);
530
        assign  f_this_pc   = (o_pc      == { f_const_addr, 2'b00 });
531
        assign  f_this_req  = (i_pc      == { f_const_addr, 2'b00 });
532
        assign  f_this_data = (i_wb_data ==   f_const_insn);
533
        assign  f_this_insn = (o_insn    ==   f_const_insn);
534
 
535
 
536
        //
537
        //
538
        // Here's our contract:
539
        //
540
        // Any time we return a value for the address above, it *must* be
541
        // the "right" value.
542
        //
543
        always @(*)
544
        if ((o_valid)&&(f_this_pc))
545
        begin
546
                if (f_const_illegal)
547
                        assert(o_illegal);
548
                if (!o_illegal)
549
                        assert(f_this_insn);
550
        end
551
 
552
        //
553
        // The contract will only work if we assume the return from the
554
        // bus at this address will be the right return.
555
        wire    f_this_return;
556
        assign  f_this_return = (o_wb_addr - f_outstanding == f_const_addr);
557
        always @(*)
558
        if ((o_wb_cyc)&&(f_this_return))
559
        begin
560
                if (i_wb_ack)
561
                        assume(i_wb_data == f_const_insn);
562
 
563
                if (f_const_illegal)
564
                        assume(!i_wb_ack);
565
                else
566
                        assume(!i_wb_err);
567
        end
568
 
569
        //
570
        // Here is a corrollary to our contract.  Anything in the one-word
571
        // cache must also match the contract as well.
572
        //
573
        always @(*)
574
        if ((o_pc[AW+1:2] + 1'b1 == f_const_addr)&&(cache_valid))
575
        begin
576
                if (!cache_illegal)
577
                        assert(cache_word == f_const_insn);
578
 
579
                if (f_const_illegal)
580
                        assert(cache_illegal);
581
        end
582
 
583
        always @(posedge i_clk)
584
        if ((f_past_valid)&&(!$past(cache_illegal))&&(!cache_valid))
585
                assert(!cache_illegal);
586
 
587
        ////////////////////////////////////////////////////////
588
        //
589
        //
590
        // Additional assertions necessary to pass induction
591
        //
592
        //
593
        ////////////////////////////////////////////////////////
594
        //
595
        // We have only a one word cache.  Hence, we shouldn't be asking
596
        // for more data any time we have nowhere to put it.
597
        always @(*)
598
        if (o_wb_stb)
599
                assert((!cache_valid)||(i_stall_n));
600
 
601
        always @(*)
602
        if ((o_valid)&&(cache_valid))
603
                assert((f_outstanding == 0)&&(!o_wb_stb));
604
 
605
        always @(*)
606
        if ((o_valid)&&(!i_stall_n))
607
                assert(f_outstanding < 2);
608
 
609
        always @(*)
610
        if ((!o_valid)||(i_stall_n))
611
                assert(f_outstanding <= 2);
612
 
613
        always @(posedge i_clk)
614
        if ((f_past_valid)&&($past(o_wb_cyc))&&(!$past(o_wb_stb))
615
                        &&(o_wb_cyc))
616
                assert(inflight != 0);
617
 
618
        always @(*)
619
        if ((o_wb_cyc)&&(i_wb_ack))
620
                assert(!cache_valid);
621
 
622
        always @(posedge i_clk)
623
        if (o_wb_cyc)
624
                assert(inflight == f_outstanding);
625
 
626
        wire    [AW-1:0] this_return_address,
627
                                next_pc_address;
628
        assign  this_return_address = o_wb_addr - f_outstanding;
629
        assign  next_pc_address = o_pc[AW+1:2] + 1'b1;
630
 
631
        always @(posedge i_clk)
632
        if ((f_past_valid)&&($past(o_wb_cyc))
633
                        &&(!$past(i_reset))
634
                        &&(!$past(i_new_pc))
635
                        &&(!$past(i_clear_cache))
636
                        &&(!$past(invalid_bus_cycle))
637
                        &&(($past(i_wb_ack))||($past(i_wb_err)))
638
                        &&((!$past(o_valid))||($past(i_stall_n)))
639
                        &&(!$past(cache_valid)))
640
                assert(o_pc[AW+1:2] == $past(this_return_address));
641
 
642
        always @(posedge i_clk)
643
        if ((f_past_valid)&&($past(o_wb_cyc))&&(!o_valid)&&(!$past(i_new_pc))
644
                        &&(o_wb_cyc))
645
                assert(o_pc[AW+1:2] == this_return_address);
646
 
647
        always @(posedge i_clk)
648
        if ((f_past_valid)&&($past(o_wb_cyc))
649
                        &&(!$past(cache_valid))&&(cache_valid))
650
                assert(next_pc_address == $past(this_return_address));
651
 
652
 
653
 
654
        always @(posedge i_clk)
655
        if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc))
656
        begin
657
                if ((o_valid)&&(!cache_valid))
658
                        assert(this_return_address == next_pc_address);
659
                else if (!o_valid)
660
                        assert(this_return_address == o_pc[AW+1:2]);
661
        end else if ((f_past_valid)&&(!invalid_bus_cycle)
662
                        &&(!o_wb_cyc)&&(o_valid)&&(!o_illegal)
663
                        &&(!cache_valid))
664
                assert(o_wb_addr == next_pc_address);
665
 
666
 
667
        always @(*)
668
        if (invalid_bus_cycle)
669
                assert(!o_wb_cyc);
670
        always @(*)
671
        if (cache_valid)
672
                assert(o_valid);
673
 
674
        /////////////////////////////////////////////////////
675
        //
676
        //
677
        // Cover statements
678
        //
679
        //
680
        /////////////////////////////////////////////////////
681
 
682
        always @(posedge i_clk)
683
        cover((f_past_valid)&&($past(f_nacks)==3)
684
                &&($past(i_wb_ack))&&($past(o_wb_cyc)));
685
 
686
 
687
        /////////////////////////////////////////////////////
688
        //
689
        //
690
        // Temporary simplifications
691
        //
692
        //
693
        /////////////////////////////////////////////////////
694
 
695
//      always @(*)
696
//              assume((!i_wb_err)&&(!f_const_illegal));
697
 
698
 
699
`endif  // FORMAL
700 205 dgisselq
endmodule
701 209 dgisselq
//
702
// Usage:               (this)  (prior) (old)  (S6)
703
//    Cells             374     387     585     459
704
//      FDRE            135     108     203     171
705
//      LUT1              2       3       2
706
//      LUT2              9       3       4       5
707
//      LUT3             98      76     104      71
708
//      LUT4              2       0       2       2
709
//      LUT5              3      35      35       3
710
//      LUT6              6       5      10      43
711
//      MUXCY            58      62      93      62
712
//      MUXF7             1       0       2       3
713
//      MUXF8             0       1       1
714
//      RAM64X1D          0      32      32      32
715
//      XORCY            60      64      96      64
716
//

powered by: WebSVN 2.1.0

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