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

Subversion Repositories zipcpu

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

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
2 49 dgisselq
//
3
// Filename:    pipemem.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     A memory unit to support a CPU, this time one supporting
8
//              pipelined wishbone memory accesses.  The goal is to be able
9
//      to issue one pipelined wishbone access per clock, and (given the memory
10
//      is fast enough) to be able to read the results back at one access per
11
//      clock.  This renders on-chip memory fast enough to handle single cycle
12
//      (pipelined) access.
13
//
14
//
15
// Creator:     Dan Gisselquist, Ph.D.
16 69 dgisselq
//              Gisselquist Technology, LLC
17 49 dgisselq
//
18 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
19 49 dgisselq
//
20 209 dgisselq
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
21 49 dgisselq
//
22
// This program is free software (firmware): you can redistribute it and/or
23
// modify it under the terms of  the GNU General Public License as published
24
// by the Free Software Foundation, either version 3 of the License, or (at
25
// your option) any later version.
26
//
27
// This program is distributed in the hope that it will be useful, but WITHOUT
28
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
29
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
30
// for more details.
31
//
32 201 dgisselq
// You should have received a copy of the GNU General Public License along
33
// with this program.  (It's in the $(ROOT)/doc directory, run make with no
34
// target there if the PDF file isn't present.)  If not, see
35
// <http://www.gnu.org/licenses/> for a copy.
36
//
37 49 dgisselq
// License:     GPL, v3, as defined and found on www.gnu.org,
38
//              http://www.gnu.org/licenses/gpl.html
39
//
40
//
41 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
42 49 dgisselq
//
43 201 dgisselq
//
44 209 dgisselq
`default_nettype        none
45
//
46
module  pipemem(i_clk, i_reset, i_pipe_stb, i_lock,
47 49 dgisselq
                i_op, i_addr, i_data, i_oreg,
48
                        o_busy, o_pipe_stalled, o_valid, o_err, o_wreg, o_result,
49
                o_wb_cyc_gbl, o_wb_cyc_lcl,
50
                        o_wb_stb_gbl, o_wb_stb_lcl,
51 201 dgisselq
                        o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
52 209 dgisselq
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data
53
`ifdef  FORMAL
54
                , f_nreqs, f_nacks, f_outstanding, f_pc
55
`endif
56
                );
57
        parameter       ADDRESS_WIDTH=30;
58
        parameter [0:0]   IMPLEMENT_LOCK=1'b1,
59
                        WITH_LOCAL_BUS=1'b1,
60
                        OPT_ZERO_ON_IDLE=1'b0,
61
                        // OPT_ALIGNMENT_ERR
62
                        OPT_ALIGNMENT_ERR=1'b0;
63
        localparam      AW=ADDRESS_WIDTH,
64
                        FLN=4;
65
        parameter [(FLN-1):0]    OPT_MAXDEPTH=4'hd;
66
        input   wire            i_clk, i_reset;
67
        input   wire            i_pipe_stb, i_lock;
68 49 dgisselq
        // CPU interface
69 209 dgisselq
        input   wire    [2:0]    i_op;
70
        input   wire    [31:0]   i_addr;
71
        input   wire    [31:0]   i_data;
72
        input   wire    [4:0]    i_oreg;
73 49 dgisselq
        // CPU outputs
74
        output  wire            o_busy;
75
        output  wire            o_pipe_stalled;
76
        output  reg             o_valid;
77
        output  reg             o_err;
78
        output  reg     [4:0]    o_wreg;
79
        output  reg     [31:0]   o_result;
80
        // Wishbone outputs
81 69 dgisselq
        output  wire            o_wb_cyc_gbl;
82
        output  reg             o_wb_stb_gbl;
83
        output  wire            o_wb_cyc_lcl;
84
        output  reg             o_wb_stb_lcl, o_wb_we;
85 49 dgisselq
        output  reg     [(AW-1):0]       o_wb_addr;
86
        output  reg     [31:0]   o_wb_data;
87 201 dgisselq
        output  reg     [3:0]    o_wb_sel;
88 49 dgisselq
        // Wishbone inputs
89 209 dgisselq
        input   wire            i_wb_ack, i_wb_stall, i_wb_err;
90
        input   wire    [31:0]   i_wb_data;
91
// Formal
92
        parameter       F_LGDEPTH=5;
93
`ifdef  FORMAL
94
        output  wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
95
        output  reg     f_pc;
96
`endif
97 49 dgisselq
 
98 209 dgisselq
 
99
        reg                     cyc;
100
        reg                     r_wb_cyc_gbl, r_wb_cyc_lcl, fifo_full;
101
        reg     [(FLN-1):0]              rdaddr, wraddr;
102
        wire    [(FLN-1):0]              nxt_rdaddr, fifo_fill;
103
        reg     [(3+5-1):0]      fifo_oreg [0:15];
104
        reg                     fifo_gie;
105 49 dgisselq
        initial rdaddr = 0;
106
        initial wraddr = 0;
107 201 dgisselq
 
108 209 dgisselq
        reg     misaligned;
109
 
110
        always  @(*)
111
        if (OPT_ALIGNMENT_ERR)
112
        begin
113
                casez({ i_op[2:1], i_addr[1:0] })
114
                4'b01?1: misaligned = i_pipe_stb;
115
                4'b0110: misaligned = i_pipe_stb;
116
                4'b10?1: misaligned = i_pipe_stb;
117
                default: misaligned = i_pipe_stb;
118
                endcase
119
        end else
120
                misaligned = 1'b0;
121
 
122 49 dgisselq
        always @(posedge i_clk)
123 209 dgisselq
                fifo_oreg[wraddr] <= { i_oreg[3:0], i_op[2:1], i_addr[1:0] };
124 201 dgisselq
 
125 49 dgisselq
        always @(posedge i_clk)
126 209 dgisselq
        if (i_pipe_stb)
127
                fifo_gie <= i_oreg[4];
128
 
129
        initial wraddr = 0;
130
        always @(posedge i_clk)
131
        if (i_reset)
132
                wraddr <= 0;
133
        else if (((i_wb_err)&&(cyc))||((i_pipe_stb)&&(misaligned)))
134 49 dgisselq
                        wraddr <= 0;
135 209 dgisselq
        else if (i_pipe_stb)
136
                wraddr <= wraddr + 1'b1;
137
 
138
        initial rdaddr = 0;
139 49 dgisselq
        always @(posedge i_clk)
140 209 dgisselq
        if (i_reset)
141
                rdaddr <= 0;
142
        else if (((i_wb_err)&&(cyc))||((i_pipe_stb)&&(misaligned)))
143
                rdaddr <= 0;
144
        else if ((i_wb_ack)&&(cyc))
145
                rdaddr <= rdaddr + 1'b1;
146
 
147
        assign  fifo_fill = wraddr - rdaddr;
148
 
149
        initial fifo_full = 0;
150
        always @(posedge i_clk)
151
        if (i_reset)
152
                fifo_full <= 0;
153
        else if (((i_wb_err)&&(cyc))||((i_pipe_stb)&&(misaligned)))
154
                fifo_full <= 0;
155
        else if (i_pipe_stb)
156
                fifo_full <= (fifo_fill >= OPT_MAXDEPTH-1);
157
        else
158
                fifo_full <= (fifo_fill >= OPT_MAXDEPTH);
159
 
160 201 dgisselq
        assign  nxt_rdaddr = rdaddr + 1'b1;
161 49 dgisselq
 
162 209 dgisselq
        wire    gbl_stb, lcl_stb, lcl_bus;
163
        assign  lcl_bus = (i_addr[31:24]==8'hff)&&(WITH_LOCAL_BUS);
164
        assign  lcl_stb = (lcl_bus)&&(!misaligned);
165
        assign  gbl_stb = ((!lcl_bus)||(!WITH_LOCAL_BUS))&&(!misaligned);
166 56 dgisselq
                        //= ((i_addr[31:8]!=24'hc00000)||(i_addr[7:5]!=3'h0));
167 49 dgisselq
 
168 56 dgisselq
        initial cyc = 0;
169 69 dgisselq
        initial r_wb_cyc_lcl = 0;
170
        initial r_wb_cyc_gbl = 0;
171 209 dgisselq
        initial o_wb_stb_lcl = 0;
172
        initial o_wb_stb_gbl = 0;
173 49 dgisselq
        always @(posedge i_clk)
174 209 dgisselq
        if (i_reset)
175
        begin
176
                r_wb_cyc_gbl <= 1'b0;
177
                r_wb_cyc_lcl <= 1'b0;
178
                o_wb_stb_gbl <= 1'b0;
179
                o_wb_stb_lcl <= 1'b0;
180
                cyc <= 1'b0;
181
        end else if (cyc)
182
        begin
183
                if (((!i_wb_stall)&&(!i_pipe_stb)&&(!misaligned))
184
                        ||(i_wb_err))
185 49 dgisselq
                begin
186 209 dgisselq
                        o_wb_stb_gbl <= 1'b0;
187
                        o_wb_stb_lcl <= 1'b0;
188
                end
189
 
190
                if (((i_wb_ack)&&(nxt_rdaddr == wraddr)
191
                                &&((!i_pipe_stb)||(misaligned)))
192
                        ||(i_wb_err))
193
                begin
194 69 dgisselq
                        r_wb_cyc_gbl <= 1'b0;
195
                        r_wb_cyc_lcl <= 1'b0;
196 49 dgisselq
                        o_wb_stb_gbl <= 1'b0;
197
                        o_wb_stb_lcl <= 1'b0;
198 56 dgisselq
                        cyc <= 1'b0;
199 209 dgisselq
                end
200
        end else if (i_pipe_stb) // New memory operation
201
        begin // Grab the wishbone
202
                r_wb_cyc_lcl <= lcl_stb;
203
                r_wb_cyc_gbl <= gbl_stb;
204
                o_wb_stb_lcl <= lcl_stb;
205
                o_wb_stb_gbl <= gbl_stb;
206
                cyc <= (!misaligned);
207
        end
208 49 dgisselq
 
209 56 dgisselq
        always @(posedge i_clk)
210 209 dgisselq
        if ((!cyc)||(!i_wb_stall))
211
        begin
212
                if ((OPT_ZERO_ON_IDLE)&&(!i_pipe_stb))
213
                        o_wb_addr <= 0;
214
                else
215 201 dgisselq
                        o_wb_addr <= i_addr[(AW+1):2];
216
 
217 209 dgisselq
                if ((OPT_ZERO_ON_IDLE)&&(!i_pipe_stb))
218
                        o_wb_sel <= 4'b0000;
219
                else casez({ i_op[2:1], i_addr[1:0] })
220
                        4'b100?: o_wb_sel <= 4'b1100;   // Op = 5
221
                        4'b101?: o_wb_sel <= 4'b0011;   // Op = 5
222
                        4'b1100: o_wb_sel <= 4'b1000;   // Op = 5
223
                        4'b1101: o_wb_sel <= 4'b0100;   // Op = 7
224
                        4'b1110: o_wb_sel <= 4'b0010;   // Op = 7
225
                        4'b1111: o_wb_sel <= 4'b0001;   // Op = 7
226
                        default: o_wb_sel <= 4'b1111;   // Op = 7
227
                endcase
228 201 dgisselq
 
229 209 dgisselq
                if ((OPT_ZERO_ON_IDLE)&&(!i_pipe_stb))
230
                        o_wb_data <= 0;
231
                else casez({ i_op[2:1], i_addr[1:0] })
232
                4'b100?: o_wb_data <= { i_data[15:0], 16'h00 };
233
                4'b101?: o_wb_data <= { 16'h00, i_data[15:0] };
234
                4'b1100: o_wb_data <= {         i_data[7:0], 24'h00 };
235
                4'b1101: o_wb_data <= {  8'h00, i_data[7:0], 16'h00 };
236
                4'b1110: o_wb_data <= { 16'h00, i_data[7:0],  8'h00 };
237
                4'b1111: o_wb_data <= { 24'h00, i_data[7:0] };
238
                default: o_wb_data <= i_data;
239
        endcase
240
        end
241 201 dgisselq
 
242 49 dgisselq
        always @(posedge i_clk)
243 209 dgisselq
        if ((i_pipe_stb)&&(!cyc))
244
                o_wb_we   <= i_op[0];
245
        else if ((OPT_ZERO_ON_IDLE)&&(!cyc))
246
                o_wb_we   <= 1'b0;
247 49 dgisselq
 
248
        initial o_valid = 1'b0;
249
        always @(posedge i_clk)
250 209 dgisselq
        if (i_reset)
251
                o_valid <= 1'b0;
252
        else
253
                o_valid <= (cyc)&&(i_wb_ack)&&(!o_wb_we);
254
 
255 49 dgisselq
        initial o_err = 1'b0;
256
        always @(posedge i_clk)
257 209 dgisselq
        if (i_reset)
258
                o_err <= 1'b0;
259
        else
260
                o_err <= ((cyc)&&(i_wb_err))||((i_pipe_stb)&&(misaligned));
261 56 dgisselq
        assign  o_busy = cyc;
262 49 dgisselq
 
263 209 dgisselq
        wire    [7:0]    w_wreg;
264 201 dgisselq
        assign  w_wreg = fifo_oreg[rdaddr];
265 49 dgisselq
        always @(posedge i_clk)
266 209 dgisselq
                o_wreg <= { fifo_gie, w_wreg[7:4] };
267 49 dgisselq
        always @(posedge i_clk)
268 209 dgisselq
        if ((OPT_ZERO_ON_IDLE)&&((!cyc)||((!i_wb_ack)&&(!i_wb_err))))
269
                o_result <= 0;
270
        else begin
271 201 dgisselq
                casez(w_wreg[3:0])
272 209 dgisselq
                4'b1100: o_result <= { 24'h00, i_wb_data[31:24] };
273
                4'b1101: o_result <= { 24'h00, i_wb_data[23:16] };
274
                4'b1110: o_result <= { 24'h00, i_wb_data[15: 8] };
275
                4'b1111: o_result <= { 24'h00, i_wb_data[ 7: 0] };
276
                4'b100?: o_result <= { 16'h00, i_wb_data[31:16] };
277
                4'b101?: o_result <= { 16'h00, i_wb_data[15: 0] };
278
                default: o_result <= i_wb_data[31:0];
279 201 dgisselq
                endcase
280 209 dgisselq
        end
281 49 dgisselq
 
282 209 dgisselq
        assign  o_pipe_stalled = ((cyc)&&(fifo_full))||((cyc)
283
                        &&((i_wb_stall)||((!o_wb_stb_lcl)&&(!o_wb_stb_gbl))));
284 69 dgisselq
 
285
        generate
286
        if (IMPLEMENT_LOCK != 0)
287
        begin
288
                reg     lock_gbl, lock_lcl;
289
 
290
                initial lock_gbl = 1'b0;
291
                initial lock_lcl = 1'b0;
292
                always @(posedge i_clk)
293 209 dgisselq
                if ((i_reset)||((i_wb_err)&&(cyc))
294
                        ||((i_pipe_stb)&&(misaligned)))
295 69 dgisselq
                begin
296 209 dgisselq
                        lock_gbl <= 1'b0;
297
                        lock_lcl <= 1'b0;
298
                end else begin
299 69 dgisselq
                        lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
300 201 dgisselq
                        lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
301 69 dgisselq
                end
302
 
303
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
304
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
305
        end else begin
306
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl);
307
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl);
308
        end endgenerate
309
 
310 209 dgisselq
        // Make verilator happy
311
        // verilator lint_off UNUSED
312
        wire    unused;
313
        assign  unused = i_lock;
314
        // verilator lint_on  UNUSED
315
 
316
`ifdef  FORMAL
317
`define ASSERT  assert
318
`ifdef  PIPEMEM
319
`define ASSUME  assume
320
`else
321
`define ASSUME  assert
322
`endif
323
 
324
        reg     f_past_valid;
325
        initial f_past_valid = 0;
326
        always @(posedge i_clk)
327
                f_past_valid = 1'b1;
328
        always @(*)
329
                if (!f_past_valid)
330
                        `ASSUME(i_reset);
331
 
332
        initial `ASSUME( i_reset);
333
        initial `ASSUME(!i_pipe_stb);
334
 
335
        wire    f_cyc, f_stb;
336
        assign  f_cyc = cyc;
337
        assign  f_stb = (o_wb_stb_gbl)||(o_wb_stb_lcl);
338
 
339
`ifdef  PIPEMEM
340
`define MASTER  fwb_master
341
`else
342
`define MASTER  fwb_counter
343
`endif
344
        `MASTER #(.AW(AW), .F_LGDEPTH(F_LGDEPTH),
345
                        // .F_MAX_REQUESTS(14), // Not quite true, can do more
346
                        .F_OPT_RMW_BUS_OPTION(IMPLEMENT_LOCK),
347
                        .F_OPT_DISCONTINUOUS(IMPLEMENT_LOCK))
348
                fwb(i_clk, i_reset,
349
                        cyc, f_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
350
                                i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
351
                        f_nreqs, f_nacks, f_outstanding);
352
 
353
 
354
        //
355
        // Assumptions about inputs
356
        //
357
        always @(posedge i_clk)
358
        if ((!f_past_valid)||($past(i_reset)))
359
        begin
360
                `ASSERT(!o_err);
361
                `ASSERT(!o_busy);
362
                `ASSERT(!o_pipe_stalled);
363
                `ASSERT(!o_valid);
364
        end
365
 
366
        always @(posedge i_clk)
367
                if (o_pipe_stalled)
368
                        `ASSUME(!i_pipe_stb);
369
 
370
        // On any pipe request, the new address is the same or plus one
371
        always @(posedge i_clk)
372
                if ((f_past_valid)&&(f_cyc)&&(!i_wb_stall)&&(i_pipe_stb))
373
                begin
374
                        `ASSUME( (i_addr[(AW+1):2] == o_wb_addr)
375
                                ||(i_addr[(AW+1):2] == o_wb_addr+1));
376
                        `ASSUME(i_op[0] == o_wb_we);
377
                end
378
 
379
        always @(posedge i_clk)
380
                if ((r_wb_cyc_gbl)&&(i_pipe_stb))
381
                        `ASSUME(gbl_stb);
382
 
383
        always @(posedge i_clk)
384
                if ((r_wb_cyc_lcl)&&(i_pipe_stb))
385
                        `ASSUME(lcl_stb);
386
 
387
        // If stb is false, then either lock is on or there are no more STB's
388
        always @(posedge i_clk)
389
                if ((f_cyc)&&(!f_stb))
390
                        `ASSUME((i_lock)||(!i_pipe_stb));
391
 
392
//always @(posedge i_clk)
393
//      if ((f_past_valid)&&($past(f_cyc))&&(!$past(i_lock)))
394
//              `ASSUME(!i_lock);
395
 
396
        wire    [3:0]    f_pipe_used;
397
        assign  f_pipe_used = wraddr - rdaddr;
398
        always @(*)
399
                `ASSERT(f_pipe_used == fifo_fill);
400
        always @(posedge i_clk)
401
        if (f_pipe_used == OPT_MAXDEPTH)
402
 
403
        begin
404
                `ASSUME(!i_pipe_stb);
405
                `ASSERT((o_busy)&&(o_pipe_stalled));
406
        end
407
 
408
        always @(*)
409
                `ASSERT(fifo_fill <= OPT_MAXDEPTH);
410
 
411
        always @(*)
412
                if (!IMPLEMENT_LOCK)
413
                        `ASSUME(!i_lock);
414
 
415
`ifndef VERILATOR
416
        always @(*)
417
                if ((WITH_LOCAL_BUS)&&(o_wb_cyc_gbl|o_wb_cyc_lcl)
418
                        &&(i_pipe_stb))
419
                begin
420
                        if (o_wb_cyc_lcl)
421
                                // `ASSUME(i_addr[31:24] == 8'hff);
422
                                assume(i_addr[31:24] == 8'hff);
423
                        else
424
                                assume(i_addr[31:24] != 8'hff);
425
                end
426
`endif
427
 
428
        always @(*)
429
                if (!WITH_LOCAL_BUS)
430
                begin
431
                        assert(!r_wb_cyc_lcl);
432
                        assert(!o_wb_cyc_lcl);
433
                        assert(!o_wb_stb_lcl);
434
                end
435
 
436
        always @(posedge i_clk)
437
                if ((f_past_valid)&&(!$past(f_cyc))&&(!$past(i_pipe_stb)))
438
                        `ASSERT(f_pipe_used == 0);
439
 
440
        always @(*)
441
        if (!f_cyc)
442
                `ASSERT(f_pipe_used == 0);
443
 
444
        always @(posedge i_clk)
445
        if (f_pipe_used >= 13)
446
                `ASSUME(!i_pipe_stb);
447
 
448
        always @(posedge i_clk)
449
        if ((f_cyc)&&(f_pipe_used >= 13))
450
                `ASSERT((o_busy)&&(o_pipe_stalled));
451
 
452
 
453
        always @(posedge i_clk)
454
                `ASSERT((!r_wb_cyc_gbl)||(!r_wb_cyc_lcl));
455
 
456
        always @(posedge i_clk)
457
                `ASSERT((!o_wb_cyc_gbl)||(!o_wb_cyc_lcl));
458
 
459
        always @(posedge i_clk)
460
                `ASSERT((!o_wb_stb_gbl)||(!o_wb_stb_lcl));
461
 
462
        always @(*)
463
                if (!WITH_LOCAL_BUS)
464
                begin
465
                        assert(!o_wb_cyc_lcl);
466
                        assert(!o_wb_stb_lcl);
467
                        if (o_wb_stb_lcl)
468
                                assert(o_wb_addr[(AW-1):22] == {(8-(30-AW)){1'b1}});
469
                end
470
 
471
        always @(posedge i_clk)
472
                if (o_wb_stb_gbl)
473
                        `ASSERT(o_wb_cyc_gbl);
474
 
475
        always @(posedge i_clk)
476
                if (o_wb_stb_lcl)
477
                        `ASSERT(o_wb_cyc_lcl);
478
 
479
        always @(posedge i_clk)
480
                `ASSERT(cyc == (r_wb_cyc_gbl|r_wb_cyc_lcl));
481
 
482
        always @(posedge i_clk)
483
                `ASSERT(cyc == (r_wb_cyc_lcl)|(r_wb_cyc_gbl));
484
        always @(posedge i_clk)
485
        if ((f_past_valid)&&(!i_reset)&&(!$past(misaligned)))
486
        begin
487
                if (f_stb)
488
                        `ASSERT(f_pipe_used == f_outstanding + 4'h1);
489
                else
490
                        `ASSERT(f_pipe_used == f_outstanding);
491
        end
492
 
493
        always @(posedge i_clk)
494
                if ((f_past_valid)&&($past(r_wb_cyc_gbl||r_wb_cyc_lcl))
495
                                &&(!$past(f_stb)))
496
                        `ASSERT(!f_stb);
497
 
498
        always @(*)
499
                `ASSERT((!lcl_stb)||(!gbl_stb));
500
 
501
        reg     [(1<<FLN)-1:0]   f_mem_used;
502
        wire    [(1<<FLN)-1:0]   f_zero;
503
        //
504
        // insist that we only ever accept memory requests for the same GIE
505
        // (i.e. 4th bit of register)
506
        //
507
        always @(*)
508
        if ((i_pipe_stb)&&(wraddr != rdaddr))
509
                `ASSUME(i_oreg[4] == fifo_gie);
510
 
511
        initial f_pc = 1'b0;
512
        always @(posedge i_clk)
513
        if(i_reset)
514
                f_pc <= 1'b0;
515
        else if (i_pipe_stb)
516
                f_pc <= (((f_pc)&&(f_cyc))
517
                                ||((!i_op[0])&&(i_oreg[3:1] == 3'h7)));
518
        else if (!f_cyc)
519
                f_pc <= 1'b0;
520
 
521
        always @(posedge i_clk)
522
        if ((f_cyc)&&(o_wb_we))
523
                `ASSERT(!f_pc);
524
 
525
        always @(*)
526
        if ((f_pc)&&(f_cyc))
527
                `ASSUME(!i_pipe_stb);
528
 
529
        always @(*)
530
        if (wraddr == rdaddr)
531
        begin
532
                `ASSERT(!r_wb_cyc_gbl);
533
                `ASSERT(!r_wb_cyc_lcl);
534
        end else if (f_cyc)
535
        begin
536
                `ASSERT(fifo_fill == f_outstanding + ((f_stb)?1:0));
537
        end
538
 
539
 
540
`define FIFOCHECK
541
`ifdef  FIFOCHECK
542
        wire    [3:0]    lastaddr = wraddr - 1'b1;
543
 
544
        integer k;
545
        always @(*)
546
        begin
547
                f_mem_used = 0;
548
                for(k = 0 ; k < (1<<FLN); k=k+1)
549
                begin
550
                        if (wraddr == rdaddr)
551
                                f_mem_used[k] = 1'b0;
552
                        else if (wraddr > rdaddr)
553
                        begin
554
                                if ((k < wraddr)&&(k >= rdaddr))
555
                                        f_mem_used[k] = 1'b1;
556
                        end else if (k < wraddr)
557
                                f_mem_used[k] = 1'b1;
558
                        else if (k >= rdaddr)
559
                                f_mem_used[k] = 1'b1;
560
                end
561
        end
562
 
563
 
564
        always @(*)
565
        begin
566
                for(k=0; k<(1<<FLN); k=k+1)
567
                if ((f_mem_used[k])&&(!o_wb_we)&&((!f_pc)||(k!=lastaddr)))
568
                        `ASSERT(fifo_oreg[k][7:5] != 3'h7);
569
        end
570
 
571
        initial assert(!fifo_full);
572
 
573
        always @(posedge i_clk)
574
                cover(cyc && !fifo_full);
575
 
576
        always @(posedge i_clk)
577
                cover((f_cyc)&&(f_stb)&&(!i_wb_stall)&&(!i_wb_ack)
578
                        &&(!o_pipe_stalled));
579
 
580
        always @(posedge i_clk)
581
        if ((f_past_valid)&&(!$past(f_stb))&&($past(f_cyc)))
582
                cover((f_cyc)&&(i_wb_ack));
583
 
584
        always @(posedge i_clk)
585
        if ((f_past_valid)&&(!$past(f_stb))&&($past(f_cyc)))
586
                cover($past(i_wb_ack)&&(i_wb_ack));
587
 
588
        always @(posedge i_clk)
589
        if ((f_past_valid)&&($past(o_valid)))
590
                cover(o_valid);
591
 
592
`endif // FIFOCHECK
593
 
594
        always @(posedge i_clk)
595
        if ((f_past_valid)&&($past(f_past_valid))&&($past(f_cyc))&&($past(f_cyc,2)))
596
                `ASSERT($stable(o_wreg[4]));
597
 
598
        always @(*)
599
                `ASSERT((!f_cyc)||(!o_valid)||(o_wreg[3:1]!=3'h7));
600
 
601
`endif // FORMAL
602 49 dgisselq
endmodule
603 209 dgisselq
//
604
//
605
// Usage (from yosys): (Before) (A,!OPTZ)       (A,OPTZ)
606
//      Cells:          302     314             391
607
//        FDRE          138     140             140
608
//        LUT1            2       2               2
609
//        LUT2           38      41              61
610
//        LUT3           13      16              33
611
//        LUT4            3       8              12
612
//        LUT5           22      10               8
613
//        LUT6           52      59              81
614
//        MUXCY           6       6               6
615
//        MUXF7          10      13              21
616
//        MUXF8           1       2              10
617
//        RAM64X1D        9       9               9
618
//        XORCY           8       8               8
619
//
620
//

powered by: WebSVN 2.1.0

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