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

Subversion Repositories zipcpu

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

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
2 3 dgisselq
//
3
// Filename:    memops.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     A memory unit to support a CPU.
8
//
9 209 dgisselq
//      In the interests of code simplicity, this memory operator is
10 3 dgisselq
//      susceptible to unknown results should a new command be sent to it
11
//      before it completes the last one.  Unpredictable results might then
12
//      occurr.
13
//
14 36 dgisselq
//      20150919 -- Added support for handling BUS ERR's (i.e., the WB
15
//              error signal).
16
//
17 3 dgisselq
// Creator:     Dan Gisselquist, Ph.D.
18 69 dgisselq
//              Gisselquist Technology, LLC
19 3 dgisselq
//
20 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
21 3 dgisselq
//
22 209 dgisselq
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
23 3 dgisselq
//
24
// This program is free software (firmware): you can redistribute it and/or
25
// modify it under the terms of  the GNU General Public License as published
26
// by the Free Software Foundation, either version 3 of the License, or (at
27
// your option) any later version.
28
//
29
// This program is distributed in the hope that it will be useful, but WITHOUT
30
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
31
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
32
// for more details.
33
//
34 201 dgisselq
// You should have received a copy of the GNU General Public License along
35
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
36
// target there if the PDF file isn't present.)  If not, see
37
// <http://www.gnu.org/licenses/> for a copy.
38
//
39 3 dgisselq
// License:     GPL, v3, as defined and found on www.gnu.org,
40
//              http://www.gnu.org/licenses/gpl.html
41
//
42
//
43 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
44 3 dgisselq
//
45 201 dgisselq
//
46 209 dgisselq
`default_nettype        none
47
//
48
module  memops(i_clk, i_reset, i_stb, i_lock,
49 2 dgisselq
                i_op, i_addr, i_data, i_oreg,
50 36 dgisselq
                        o_busy, o_valid, o_err, o_wreg, o_result,
51
                o_wb_cyc_gbl, o_wb_cyc_lcl,
52
                        o_wb_stb_gbl, o_wb_stb_lcl,
53 201 dgisselq
                        o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
54 209 dgisselq
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data
55
`ifdef  FORMAL
56
                , f_nreqs, f_nacks, f_outstanding
57
`endif
58
                );
59
        parameter       ADDRESS_WIDTH=30;
60
        parameter [0:0]   IMPLEMENT_LOCK=1'b1,
61
                        WITH_LOCAL_BUS=1'b1,
62
                        OPT_ALIGNMENT_ERR=1'b1,
63
                        OPT_ZERO_ON_IDLE=1'b0;
64 201 dgisselq
        localparam      AW=ADDRESS_WIDTH;
65 209 dgisselq
        input   wire            i_clk, i_reset;
66
        input   wire            i_stb, i_lock;
67 2 dgisselq
        // CPU interface
68 209 dgisselq
        input   wire    [2:0]    i_op;
69
        input   wire    [31:0]   i_addr;
70
        input   wire    [31:0]   i_data;
71
        input   wire    [4:0]    i_oreg;
72 2 dgisselq
        // CPU outputs
73
        output  wire            o_busy;
74
        output  reg             o_valid;
75 36 dgisselq
        output  reg             o_err;
76 2 dgisselq
        output  reg     [4:0]    o_wreg;
77
        output  reg     [31:0]   o_result;
78
        // Wishbone outputs
79 69 dgisselq
        output  wire            o_wb_cyc_gbl;
80
        output  reg             o_wb_stb_gbl;
81
        output  wire            o_wb_cyc_lcl;
82
        output  reg             o_wb_stb_lcl;
83
        output  reg             o_wb_we;
84 48 dgisselq
        output  reg     [(AW-1):0]       o_wb_addr;
85
        output  reg     [31:0]   o_wb_data;
86 201 dgisselq
        output  reg     [3:0]    o_wb_sel;
87 2 dgisselq
        // Wishbone inputs
88 209 dgisselq
        input   wire            i_wb_ack, i_wb_stall, i_wb_err;
89
        input   wire    [31:0]   i_wb_data;
90
// Formal
91
        parameter       F_LGDEPTH = 2;
92
`ifdef  FORMAL
93
        output  wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
94
`endif
95 2 dgisselq
 
96 209 dgisselq
        reg     misaligned;
97
 
98
        generate if (OPT_ALIGNMENT_ERR)
99
        begin : GENERATE_ALIGNMENT_ERR
100
                always @(*)
101
                casez({ i_op[2:1], i_addr[1:0] })
102
                4'b01?1: misaligned = i_stb; // Words must be halfword aligned
103
                4'b0110: misaligned = i_stb; // Words must be word aligned
104
                4'b10?1: misaligned = i_stb; // Halfwords must be aligned
105
                // 4'b11??: misaligned <= 1'b0; Byte access are never misaligned
106
                default: misaligned = 1'b0;
107
                endcase
108
        end else
109
                always @(*)     misaligned = 1'b0;
110
        endgenerate
111
 
112 69 dgisselq
        reg     r_wb_cyc_gbl, r_wb_cyc_lcl;
113 36 dgisselq
        wire    gbl_stb, lcl_stb;
114 209 dgisselq
        assign  lcl_stb = (i_stb)&&(WITH_LOCAL_BUS!=0)&&(i_addr[31:24]==8'hff)
115
                                &&(!misaligned);
116
        assign  gbl_stb = (i_stb)&&((WITH_LOCAL_BUS==0)||(i_addr[31:24]!=8'hff))
117
                                &&(!misaligned);
118 36 dgisselq
 
119 69 dgisselq
        initial r_wb_cyc_gbl = 1'b0;
120
        initial r_wb_cyc_lcl = 1'b0;
121 2 dgisselq
        always @(posedge i_clk)
122 209 dgisselq
        if (i_reset)
123
        begin
124
                r_wb_cyc_gbl <= 1'b0;
125
                r_wb_cyc_lcl <= 1'b0;
126
        end else if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
127
        begin
128
                if ((i_wb_ack)||(i_wb_err))
129 36 dgisselq
                begin
130 69 dgisselq
                        r_wb_cyc_gbl <= 1'b0;
131
                        r_wb_cyc_lcl <= 1'b0;
132 36 dgisselq
                end
133 209 dgisselq
        end else begin // New memory operation
134
                // Grab the wishbone
135
                r_wb_cyc_lcl <= (lcl_stb);
136
                r_wb_cyc_gbl <= (gbl_stb);
137
        end
138
        initial o_wb_stb_gbl = 1'b0;
139 3 dgisselq
        always @(posedge i_clk)
140 209 dgisselq
        if (i_reset)
141
                o_wb_stb_gbl <= 1'b0;
142
        else if ((i_wb_err)&&(r_wb_cyc_gbl))
143
                o_wb_stb_gbl <= 1'b0;
144
        else if (o_wb_cyc_gbl)
145
                o_wb_stb_gbl <= (o_wb_stb_gbl)&&(i_wb_stall);
146
        else
147
                // Grab wishbone on any new transaction to the gbl bus
148
                o_wb_stb_gbl <= (gbl_stb);
149
 
150
        initial o_wb_stb_lcl = 1'b0;
151 3 dgisselq
        always @(posedge i_clk)
152 209 dgisselq
        if (i_reset)
153
                o_wb_stb_lcl <= 1'b0;
154
        else if ((i_wb_err)&&(r_wb_cyc_lcl))
155
                o_wb_stb_lcl <= 1'b0;
156
        else if (o_wb_cyc_lcl)
157
                o_wb_stb_lcl <= (o_wb_stb_lcl)&&(i_wb_stall);
158
        else
159
                // Grab wishbone on any new transaction to the lcl bus
160
                o_wb_stb_lcl  <= (lcl_stb);
161 201 dgisselq
 
162
        reg     [3:0]    r_op;
163 209 dgisselq
        initial o_wb_we   = 1'b0;
164
        initial o_wb_data = 0;
165
        initial o_wb_sel  = 0;
166 36 dgisselq
        always @(posedge i_clk)
167 209 dgisselq
        if (i_stb)
168
        begin
169
                o_wb_we   <= i_op[0];
170
                if (OPT_ZERO_ON_IDLE)
171 3 dgisselq
                begin
172 201 dgisselq
                        casez({ i_op[2:1], i_addr[1:0] })
173
                        4'b100?: o_wb_data <= { i_data[15:0], 16'h00 };
174
                        4'b101?: o_wb_data <= { 16'h00, i_data[15:0] };
175
                        4'b1100: o_wb_data <= {         i_data[7:0], 24'h00 };
176
                        4'b1101: o_wb_data <= {  8'h00, i_data[7:0], 16'h00 };
177
                        4'b1110: o_wb_data <= { 16'h00, i_data[7:0],  8'h00 };
178
                        4'b1111: o_wb_data <= { 24'h00, i_data[7:0] };
179 209 dgisselq
                        default: o_wb_data <= i_data;
180
                        endcase
181
                end else
182
                        casez({ i_op[2:1], i_addr[1:0] })
183 201 dgisselq
                        4'b10??: o_wb_data <= { (2){ i_data[15:0] } };
184
                        4'b11??: o_wb_data <= { (4){ i_data[7:0] } };
185
                        default: o_wb_data <= i_data;
186
                        endcase
187
 
188 209 dgisselq
                o_wb_addr <= i_addr[(AW+1):2];
189
                casez({ i_op[2:1], i_addr[1:0] })
190
                4'b01??: o_wb_sel <= 4'b1111;
191
                4'b100?: o_wb_sel <= 4'b1100;
192
                4'b101?: o_wb_sel <= 4'b0011;
193
                4'b1100: o_wb_sel <= 4'b1000;
194
                4'b1101: o_wb_sel <= 4'b0100;
195
                4'b1110: o_wb_sel <= 4'b0010;
196
                4'b1111: o_wb_sel <= 4'b0001;
197
                default: o_wb_sel <= 4'b1111;
198
                endcase
199
                r_op <= { i_op[2:1] , i_addr[1:0] };
200
        end else if ((OPT_ZERO_ON_IDLE)&&(!o_wb_cyc_gbl)&&(!o_wb_cyc_lcl))
201
        begin
202
                o_wb_we   <= 1'b0;
203
                o_wb_addr <= 0;
204
                o_wb_data <= 32'h0;
205
                o_wb_sel  <= 4'h0;
206
        end
207 2 dgisselq
 
208
        initial o_valid = 1'b0;
209
        always @(posedge i_clk)
210 209 dgisselq
        if (i_reset)
211
                o_valid <= 1'b0;
212
        else
213
                o_valid <= (((o_wb_cyc_gbl)||(o_wb_cyc_lcl))
214
                                &&(i_wb_ack)&&(!o_wb_we));
215 36 dgisselq
        initial o_err = 1'b0;
216
        always @(posedge i_clk)
217 209 dgisselq
        if (i_reset)
218
                o_err <= 1'b0;
219
        else if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
220
                o_err <= i_wb_err;
221
        else if ((i_stb)&&(!o_busy))
222
                o_err <= misaligned;
223
        else
224
                o_err <= 1'b0;
225 2 dgisselq
 
226 209 dgisselq
        assign  o_busy = (r_wb_cyc_gbl)||(r_wb_cyc_lcl);
227
 
228 2 dgisselq
        always @(posedge i_clk)
229 209 dgisselq
        if (i_stb)
230
                o_wreg    <= i_oreg;
231 2 dgisselq
        always @(posedge i_clk)
232 209 dgisselq
        if ((OPT_ZERO_ON_IDLE)&&(!i_wb_ack))
233
                o_result <= 32'h0;
234
        else begin
235 201 dgisselq
                casez(r_op)
236
                4'b01??: o_result <= i_wb_data;
237
                4'b100?: o_result <= { 16'h00, i_wb_data[31:16] };
238
                4'b101?: o_result <= { 16'h00, i_wb_data[15: 0] };
239
                4'b1100: o_result <= { 24'h00, i_wb_data[31:24] };
240
                4'b1101: o_result <= { 24'h00, i_wb_data[23:16] };
241
                4'b1110: o_result <= { 24'h00, i_wb_data[15: 8] };
242
                4'b1111: o_result <= { 24'h00, i_wb_data[ 7: 0] };
243
                default: o_result <= i_wb_data;
244
                endcase
245 209 dgisselq
        end
246 69 dgisselq
 
247 209 dgisselq
        reg     lock_gbl, lock_lcl;
248
 
249 69 dgisselq
        generate
250
        if (IMPLEMENT_LOCK != 0)
251
        begin
252
 
253
                initial lock_gbl = 1'b0;
254
                initial lock_lcl = 1'b0;
255
 
256
                always @(posedge i_clk)
257 209 dgisselq
                if (i_reset)
258 69 dgisselq
                begin
259 209 dgisselq
                        lock_gbl <= 1'b0;
260
                        lock_lcl <= 1'b0;
261
                end else if (((i_wb_err)&&((r_wb_cyc_gbl)||(r_wb_cyc_lcl)))
262
                                ||(misaligned))
263
                begin
264
                        // Kill the lock if
265
                        //      there's a bus error, or
266
                        //      User requests a misaligned memory op
267
                        lock_gbl <= 1'b0;
268
                        lock_lcl <= 1'b0;
269
                end else begin
270
                        // Kill the lock if
271
                        //      i_lock goes down
272
                        //      User starts on the global bus, then switches
273
                        //        to local or vice versa
274
                        lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl))
275
                                        &&(!lcl_stb);
276
                        lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl))
277
                                        &&(!gbl_stb);
278 69 dgisselq
                end
279
 
280
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
281
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
282
        end else begin
283 209 dgisselq
 
284 69 dgisselq
                assign  o_wb_cyc_gbl = (r_wb_cyc_gbl);
285
                assign  o_wb_cyc_lcl = (r_wb_cyc_lcl);
286 209 dgisselq
 
287
                always @(*)
288
                        { lock_gbl, lock_lcl } = 2'b00;
289
 
290
                // Make verilator happy
291
                // verilator lint_off UNUSED
292
                wire    [2:0]    lock_unused;
293
                assign  lock_unused = { i_lock, lock_gbl, lock_lcl };
294
                // verilator lint_on  UNUSED
295
 
296 69 dgisselq
        end endgenerate
297 209 dgisselq
 
298
`ifdef  VERILATOR
299
        always @(posedge i_clk)
300
        if ((r_wb_cyc_gbl)||(r_wb_cyc_lcl))
301
                assert(!i_stb);
302
`endif
303
 
304
 
305
        // Make verilator happy
306
        // verilator lint_off UNUSED
307
        generate if (AW < 22)
308
        begin : TOO_MANY_ADDRESS_BITS
309
 
310
                wire    [(21-AW):0] unused_addr;
311
                assign  unused_addr = i_addr[23:(AW+2)];
312
 
313
        end endgenerate
314
        // verilator lint_on  UNUSED
315
 
316
`ifdef  FORMAL
317
`define ASSERT  assert
318
`ifdef  MEMOPS
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
        initial `ASSUME(!i_stb);
332
 
333
        wire    f_cyc, f_stb;
334
        assign  f_cyc = (o_wb_cyc_gbl)||(o_wb_cyc_lcl);
335
        assign  f_stb = (o_wb_stb_gbl)||(o_wb_stb_lcl);
336
 
337
`ifdef  MEMOPS
338
`define MASTER  fwb_master
339
`else
340
`define MASTER  fwb_counter
341
`endif
342
 
343
        fwb_master #(.AW(AW), .F_LGDEPTH(F_LGDEPTH),
344
                        .F_OPT_RMW_BUS_OPTION(IMPLEMENT_LOCK),
345
                        .F_OPT_DISCONTINUOUS(IMPLEMENT_LOCK))
346
                f_wb(i_clk, i_reset,
347
                        f_cyc, f_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
348
                        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
349
                        f_nreqs, f_nacks, f_outstanding);
350
 
351
 
352
        // Rule: Only one of the two CYC's may be valid, never both
353
        always @(posedge i_clk)
354
                `ASSERT((!o_wb_cyc_gbl)||(!o_wb_cyc_lcl));
355
 
356
        // Rule: Only one of the two STB's may be valid, never both
357
        always @(posedge i_clk)
358
                `ASSERT((!o_wb_stb_gbl)||(!o_wb_stb_lcl));
359
 
360
        // Rule: if WITH_LOCAL_BUS is ever false, neither the local STB nor CYC
361
        // may be valid
362
        always @(*)
363
                if (!WITH_LOCAL_BUS)
364
                begin
365
                        `ASSERT(!o_wb_cyc_lcl);
366
                        `ASSERT(!o_wb_stb_lcl);
367
                end
368
 
369
        // Rule: If the global CYC is ever true, the LCL one cannot be true
370
        // on the next clock without an intervening idle of both
371
        always @(posedge i_clk)
372
                if ((f_past_valid)&&($past(r_wb_cyc_gbl)))
373
                        `ASSERT(!r_wb_cyc_lcl);
374
 
375
        // Same for if the LCL CYC is true
376
        always @(posedge i_clk)
377
                if ((f_past_valid)&&($past(r_wb_cyc_lcl)))
378
                        `ASSERT(!r_wb_cyc_gbl);
379
 
380
        // STB can never be true unless CYC is also true
381
        always @(posedge i_clk)
382
                if (o_wb_stb_gbl)
383
                        `ASSERT(r_wb_cyc_gbl);
384
        always @(posedge i_clk)
385
                if (o_wb_stb_lcl)
386
                        `ASSERT(r_wb_cyc_lcl);
387
 
388
        // This core only ever has zero or one outstanding transaction(s)
389
        always @(posedge i_clk)
390
                if ((o_wb_stb_gbl)||(o_wb_stb_lcl))
391
                        `ASSERT(f_outstanding == 0);
392
                else
393
                        `ASSERT((f_outstanding == 0)||(f_outstanding == 1));
394
 
395
        // The LOCK function only allows up to two transactions (at most)
396
        // before CYC must be dropped.
397
        always @(posedge i_clk)
398
                if ((o_wb_stb_gbl)||(o_wb_stb_lcl))
399
                begin
400
                        if (IMPLEMENT_LOCK)
401
                                `ASSERT((f_outstanding == 0)||(f_outstanding == 1));
402
                        else
403
                                `ASSERT(f_nreqs <= 1);
404
                end
405
 
406
        always @(posedge i_clk)
407
        if ((f_past_valid)&&(o_busy))
408
        begin
409
 
410
                // If i_stb doesn't change, then neither do any of the other
411
                // inputs
412
                if (($past(i_stb))&&(i_stb))
413
                begin
414
                        `ASSUME($stable(i_op));
415
                        `ASSUME($stable(i_addr));
416
                        `ASSUME($stable(i_data));
417
                        `ASSUME($stable(i_oreg));
418
                        `ASSUME($stable(i_lock));
419
                end
420
 
421
 
422
                // No strobe's are allowed if a request is outstanding, either
423
                // having been accepted by the bus or waiting to be accepted
424
                // by the bus.
425
                if ((f_outstanding != 0)||(f_stb))
426
                        `ASSUME(!i_stb);
427
                /*
428
                if (o_busy)
429
                        assert( (!i_stb)
430
                                ||((!o_wb_stb_gbl)&&(!o_wb_stb_lcl)&&(i_lock)));
431
 
432
                if ((f_cyc)&&($past(f_cyc)))
433
                        assert($stable(r_op));
434
                */
435
        end
436
 
437
        always @(*)
438
                if (!IMPLEMENT_LOCK)
439
                        `ASSUME(!i_lock);
440
 
441
        always @(posedge i_clk)
442
                if ((f_past_valid)&&($past(f_cyc))&&($past(!i_lock)))
443
                        `ASSUME(!i_lock);
444
 
445
        // Following any i_stb request, assuming we are idle, immediately
446
        // begin a bus transaction
447
        always @(posedge i_clk)
448
        if ((f_past_valid)&&($past(i_stb))
449
                &&(!$past(f_cyc))&&(!$past(i_reset)))
450
        begin
451
                if ($past(misaligned))
452
                begin
453
                        `ASSERT(!f_cyc);
454
                        `ASSERT(!o_busy);
455
                        `ASSERT(o_err);
456
                        `ASSERT(!o_valid);
457
                end else begin
458
                        `ASSERT(f_cyc);
459
                        `ASSERT(o_busy);
460
                end
461
        end
462
 
463
        always @(posedge i_clk)
464
        if (o_busy)
465
                `ASSUME(!i_stb);
466
 
467
        always @(posedge i_clk)
468
        if (o_wb_cyc_gbl)
469
                `ASSERT((o_busy)||(lock_gbl));
470
 
471
        always @(posedge i_clk)
472
        if (o_wb_cyc_lcl)
473
                `ASSERT((o_busy)||(lock_lcl));
474
 
475
        always @(posedge i_clk)
476
                if (f_outstanding > 0)
477
                        `ASSERT(o_busy);
478
 
479
        // If a transaction ends in an error, send o_err on the output port.
480
        always @(posedge i_clk)
481
                if (f_past_valid)
482
                begin
483
                        if ($past(i_reset))
484
                                `ASSERT(!o_err);
485
                        else if (($past(f_cyc))&&($past(i_wb_err)))
486
                                `ASSERT(o_err);
487
                        else if ($past(misaligned))
488
                                `ASSERT(o_err);
489
                end
490
 
491
        // Always following a successful ACK, return an O_VALID value.
492
        always @(posedge i_clk)
493
                if (f_past_valid)
494
                begin
495
                        if ($past(i_reset))
496
                                `ASSERT(!o_valid);
497
                        else if(($past(f_cyc))&&($past(i_wb_ack))
498
                                        &&(!$past(o_wb_we)))
499
                                `ASSERT(o_valid);
500
                        else if ($past(misaligned))
501
                                `ASSERT((!o_valid)&&(o_err));
502
                        else
503
                                `ASSERT(!o_valid);
504
                end
505
 
506
        //always @(posedge i_clk)
507
        //      if ((f_past_valid)&&($past(f_cyc))&&(!$past(o_wb_we))&&($past(i_wb_ack)))
508
 
509
        /*
510
        input   wire    [2:0]   i_op;
511
        input   wire    [31:0]  i_addr;
512
        input   wire    [31:0]  i_data;
513
        input   wire    [4:0]   i_oreg;
514
        // CPU outputs
515
        output  wire            o_busy;
516
        output  reg             o_valid;
517
        output  reg             o_err;
518
        output  reg     [4:0]   o_wreg;
519
        output  reg     [31:0]  o_result;
520
        */
521
 
522
        initial o_wb_we = 1'b0;
523
        always @(posedge i_clk)
524
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_stb)))
525
        begin
526
                // On a write, assert o_wb_we should be true
527
                assert( $past(i_op[0]) == o_wb_we);
528
 
529
                // Word write
530
                if ($past(i_op[2:1]) == 2'b01)
531
                begin
532
                        `ASSERT(o_wb_sel == 4'hf);
533
                        `ASSERT(o_wb_data == $past(i_data));
534
                end
535
 
536
                // Halfword (short) write
537
                if ($past(i_op[2:1]) == 2'b10)
538
                begin
539
                        if (!$past(i_addr[1]))
540
                        begin
541
                                `ASSERT(o_wb_sel == 4'hc);
542
                                `ASSERT(o_wb_data[31:16] == $past(i_data[15:0]));
543
                        end else begin
544
                                `ASSERT(o_wb_sel == 4'h3);
545
                                `ASSERT(o_wb_data[15:0] == $past(i_data[15:0]));
546
                        end
547
                end
548
 
549
                if ($past(i_op[2:1]) == 2'b11)
550
                begin
551
                        if ($past(i_addr[1:0])==2'b00)
552
                        begin
553
                                `ASSERT(o_wb_sel == 4'h8);
554
                                `ASSERT(o_wb_data[31:24] == $past(i_data[7:0]));
555
                        end
556
 
557
                        if ($past(i_addr[1:0])==2'b01)
558
                        begin
559
                                `ASSERT(o_wb_sel == 4'h4);
560
                                `ASSERT(o_wb_data[23:16] == $past(i_data[7:0]));
561
                        end
562
                        if ($past(i_addr[1:0])==2'b10)
563
                        begin
564
                                `ASSERT(o_wb_sel == 4'h2);
565
                                `ASSERT(o_wb_data[15:8] == $past(i_data[7:0]));
566
                        end
567
                        if ($past(i_addr[1:0])==2'b11)
568
                        begin
569
                                `ASSERT(o_wb_sel == 4'h1);
570
                                `ASSERT(o_wb_data[7:0] == $past(i_data[7:0]));
571
                        end
572
                end
573
 
574
                `ASSUME($past(i_op[2:1] != 2'b00));
575
        end
576
 
577
        // This logic is fixed in the definitions of the lock(s) above
578
        // i.e., the user cna be stupid and this will still work
579
        /*
580
        always @(posedge i_clk)
581
                if ((i_lock)&&(i_stb)&&(WITH_LOCAL_BUS))
582
                begin
583
                        restrict((lock_gbl)||(i_addr[31:24] ==8'hff));
584
                        restrict((lock_lcl)||(i_addr[31:24]!==8'hff));
585
                end
586
        */
587
 
588
        always @(posedge i_clk)
589
                if (o_wb_stb_lcl)
590
                        `ASSERT(o_wb_addr[29:22] == 8'hff);
591
 
592
        always @(posedge i_clk)
593
                if ((f_past_valid)&&(!$past(i_reset))&&($past(misaligned)))
594
                begin
595
                        `ASSERT(!o_wb_cyc_gbl);
596
                        `ASSERT(!o_wb_cyc_lcl);
597
                        `ASSERT(!o_wb_stb_gbl);
598
                        `ASSERT(!o_wb_stb_lcl);
599
                        `ASSERT(o_err);
600
                        //OPT_ALIGNMENT_ERR=1'b0,
601
                        //OPT_ZERO_ON_IDLE=1'b0;
602
                end
603
 
604
        always @(posedge i_clk)
605
        if ((!f_past_valid)||($past(i_reset)))
606
                `ASSUME(!i_stb);
607
        always @(*)
608
        if (o_busy)
609
                `ASSUME(!i_stb);
610
 
611
        always @(posedge i_clk)
612
        if ((f_past_valid)&&(IMPLEMENT_LOCK)
613
                &&(!$past(i_reset))&&(!$past(i_wb_err))
614
                &&(!$past(misaligned))
615
                &&(!$past(lcl_stb))
616
                &&($past(i_lock))&&($past(lock_gbl)))
617
                assert(lock_gbl);
618
 
619
        always @(posedge i_clk)
620
        if ((f_past_valid)&&(IMPLEMENT_LOCK)
621
                        &&(!$past(i_reset))&&(!$past(i_wb_err))
622
                        &&(!$past(misaligned))
623
                        &&(!$past(lcl_stb))
624
                        &&($past(o_wb_cyc_gbl))&&($past(i_lock))
625
                        &&($past(lock_gbl)))
626
                assert(o_wb_cyc_gbl);
627
 
628
        always @(posedge i_clk)
629
        if ((f_past_valid)&&(IMPLEMENT_LOCK)
630
                        &&(!$past(i_reset))&&(!$past(i_wb_err))
631
                        &&(!$past(misaligned))
632
                        &&(!$past(gbl_stb))
633
                        &&($past(o_wb_cyc_lcl))&&($past(i_lock))
634
                        &&($past(lock_lcl)))
635
                assert(o_wb_cyc_lcl);
636
 
637
        //
638
        // Cover properties
639
        //
640
        always @(posedge i_clk)
641
                cover(i_wb_ack);
642
 
643
        // Cover a response on the same clock it is made
644
        always @(posedge i_clk)
645
                cover((o_wb_stb_gbl)&&(i_wb_ack));
646
 
647
        // Cover a response a clock later
648
        always @(posedge i_clk)
649
                cover((o_wb_stb_gbl)&&(i_wb_ack));
650
 
651
 
652
        generate if (WITH_LOCAL_BUS)
653
        begin
654
 
655
                // Same things on the local bus
656
                always @(posedge i_clk)
657
                        cover((o_wb_cyc_lcl)&&(!o_wb_stb_lcl)&&(i_wb_ack));
658
                always @(posedge i_clk)
659
                        cover((o_wb_stb_lcl)&&(i_wb_ack));
660
 
661
        end endgenerate
662
 
663
`endif
664 2 dgisselq
endmodule
665 209 dgisselq
//
666
//
667
// Usage (from yosys):
668
//              (BFOR)  (!ZOI,ALIGN)    (ZOI,ALIGN)     (!ZOI,!ALIGN)
669
//      Cells    230            226             281             225
670
//        FDRE   114            116             116             116
671
//        LUT2    17             23              76              19
672
//        LUT3     9             23              17              20
673
//        LUT4    15              4              11              14
674
//        LUT5    18             18               7              15
675
//        LUT6    33             18              54              38
676
//        MUX7    16             12                               2
677
//        MUX8     8              1                               1
678
//
679
//

powered by: WebSVN 2.1.0

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