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

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [wbm2axilite.v] - Blame information for rev 16

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 16 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    wbm2axilite.v (Wishbone master to AXI slave, pipelined)
4
//
5
// Project:     Pipelined Wishbone to AXI converter
6
//
7
// Purpose:     Convert from a wishbone master to an AXI lite interface.  The
8
//              big difference is that AXI lite doesn't support bursting,
9
//      or transaction ID's.  This actually makes the task a *LOT* easier.
10
//
11
// Creator:     Dan Gisselquist, Ph.D.
12
//              Gisselquist Technology, LLC
13
//
14
////////////////////////////////////////////////////////////////////////////////
15
//
16
// Copyright (C) 2018-2019, Gisselquist Technology, LLC
17
//
18
// This file is part of the pipelined Wishbone to AXI converter project, a
19
// project that contains multiple bus bridging designs and formal bus property
20
// sets.
21
//
22
// The bus bridge designs and property sets are free RTL designs: you can
23
// redistribute them and/or modify any of them under the terms of the GNU
24
// Lesser General Public License as published by the Free Software Foundation,
25
// either version 3 of the License, or (at your option) any later version.
26
//
27
// The bus bridge designs and property sets are distributed in the hope that
28
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
29
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
30
// GNU Lesser General Public License for more details.
31
//
32
// You should have received a copy of the GNU Lesser General Public License
33
// along with these designs.  (It's in the $(ROOT)/doc directory.  Run make
34
// with no target there if the PDF file isn't present.)  If not, see
35
// <http://www.gnu.org/licenses/> for a copy.
36
//
37
// License:     LGPL, v3, as defined and found on www.gnu.org,
38
//              http://www.gnu.org/licenses/lgpl.html
39
//
40
////////////////////////////////////////////////////////////////////////////////
41
//
42
//
43
`default_nettype        none
44
//
45
module wbm2axilite (
46
        i_clk, i_reset,
47
        // AXI write address channel signals
48
        i_axi_awready, o_axi_awaddr, o_axi_awcache, o_axi_awprot, o_axi_awvalid,
49
        // AXI write data channel signals
50
        i_axi_wready, o_axi_wdata, o_axi_wstrb, o_axi_wvalid,
51
        // AXI write response channel signals
52
        i_axi_bresp, i_axi_bvalid, o_axi_bready,
53
        // AXI read address channel signals
54
        i_axi_arready, o_axi_araddr, o_axi_arcache, o_axi_arprot, o_axi_arvalid,
55
        // AXI read data channel signals   
56
        i_axi_rresp, i_axi_rvalid, i_axi_rdata, o_axi_rready,
57
        // We'll share the clock and the reset
58
        i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel,
59
                o_wb_ack, o_wb_stall, o_wb_data, o_wb_err);
60
 
61
        localparam C_AXI_DATA_WIDTH     =  32;// Width of the AXI R&W data
62
        parameter C_AXI_ADDR_WIDTH      =  28;// AXI Address width
63
        localparam DW                   =  C_AXI_DATA_WIDTH;// Wishbone data width
64
        parameter AW                    =  C_AXI_ADDR_WIDTH-2;// WB addr width (log wordsize)
65
        input   wire                    i_clk;  // System clock
66
        input   wire                    i_reset;// Reset signal,drives AXI rst
67
 
68
// AXI write address channel signals
69
        input   wire                    i_axi_awready;//Slave is ready to accept
70
        output  reg     [C_AXI_ADDR_WIDTH-1:0]   o_axi_awaddr;   // Write address
71
        output  wire    [3:0]            o_axi_awcache;  // Write Cache type
72
        output  wire    [2:0]            o_axi_awprot;   // Write Protection type
73
        output  reg                     o_axi_awvalid;  // Write address valid
74
 
75
// AXI write data channel signals
76
        input   wire                    i_axi_wready;  // Write data ready
77
        output  reg     [C_AXI_DATA_WIDTH-1:0]   o_axi_wdata;    // Write data
78
        output  reg     [C_AXI_DATA_WIDTH/8-1:0] o_axi_wstrb;    // Write strobes
79
        output  reg                     o_axi_wvalid;   // Write valid
80
 
81
// AXI write response channel signals
82
        input   wire [1:0]               i_axi_bresp;    // Write response
83
        input   wire                    i_axi_bvalid;  // Write reponse valid
84
        output  wire                    o_axi_bready;  // Response ready
85
 
86
// AXI read address channel signals
87
        input   wire                    i_axi_arready;  // Read address ready
88
        output  reg     [C_AXI_ADDR_WIDTH-1:0]   o_axi_araddr;   // Read address
89
        output  wire    [3:0]            o_axi_arcache;  // Read Cache type
90
        output  wire    [2:0]            o_axi_arprot;   // Read Protection type
91
        output  reg                     o_axi_arvalid;  // Read address valid
92
 
93
// AXI read data channel signals   
94
        input   wire    [1:0]            i_axi_rresp;   // Read response
95
        input   wire                    i_axi_rvalid;  // Read reponse valid
96
        input wire [C_AXI_DATA_WIDTH-1:0] i_axi_rdata;    // Read data
97
        output  wire                    o_axi_rready;  // Read Response ready
98
 
99
        // We'll share the clock and the reset
100
        input   wire                    i_wb_cyc;
101
        input   wire                    i_wb_stb;
102
        input   wire                    i_wb_we;
103
        input   wire    [(AW-1):0]       i_wb_addr;
104
        input   wire    [(DW-1):0]       i_wb_data;
105
        input   wire    [(DW/8-1):0]     i_wb_sel;
106
        output  reg                     o_wb_ack;
107
        output  wire                    o_wb_stall;
108
        output  reg     [(DW-1):0]       o_wb_data;
109
        output  reg                     o_wb_err;
110
 
111
//*****************************************************************************
112
// Local Parameter declarations
113
//*****************************************************************************
114
 
115
        localparam      LG_AXI_DW       = ( C_AXI_DATA_WIDTH ==   8) ? 3
116
                                        : ((C_AXI_DATA_WIDTH ==  16) ? 4
117
                                        : ((C_AXI_DATA_WIDTH ==  32) ? 5
118
                                        : ((C_AXI_DATA_WIDTH ==  64) ? 6
119
                                        : ((C_AXI_DATA_WIDTH == 128) ? 7
120
                                        : 8))));
121
 
122
        localparam      LG_WB_DW        = ( DW ==   8) ? 3
123
                                        : ((DW ==  16) ? 4
124
                                        : ((DW ==  32) ? 5
125
                                        : ((DW ==  64) ? 6
126
                                        : ((DW == 128) ? 7
127
                                        : 8))));
128
        localparam      LGFIFOLN = 5;
129
        localparam      FIFOLN = (1<<LGFIFOLN);
130
 
131
 
132
//*****************************************************************************
133
// Internal register and wire declarations
134
//*****************************************************************************
135
 
136
// Things we're not changing ...
137
        assign o_axi_awcache = 4'h3;    // Normal: no cache, no buffer
138
        assign o_axi_arcache = 4'h3;    // Normal: no cache, no buffer
139
        assign o_axi_awprot  = 3'b000;  // Unpriviledged, unsecure, data access
140
        assign o_axi_arprot  = 3'b000;  // Unpriviledged, unsecure, data access
141
 
142
        reg     full_fifo, err_state, axi_reset_state, wb_we;
143
        reg     [3:0]    reset_count;
144
        reg                     pending;
145
        reg     [LGFIFOLN-1:0]   outstanding, err_pending;
146
 
147
 
148
// Master bridge logic
149
        assign  o_wb_stall = (full_fifo)
150
                        ||((!i_wb_we)&&( wb_we)&&(pending))
151
                        ||(( i_wb_we)&&(!wb_we)&&(pending))
152
                        ||(err_state)||(axi_reset_state)
153
                        ||(o_axi_arvalid)&&(!i_axi_arready)
154
                        ||(o_axi_awvalid)&&(!i_axi_awready)
155
                        ||(o_axi_wvalid)&&(!i_axi_wready);
156
 
157
        initial axi_reset_state = 1'b1;
158
        initial reset_count = 4'hf;
159
        always @(posedge i_clk)
160
        if (i_reset)
161
        begin
162
                axi_reset_state <= 1'b1;
163
                if (reset_count > 0)
164
                        reset_count <= reset_count - 1'b1;
165
        end else if ((axi_reset_state)&&(reset_count > 0))
166
                reset_count <= reset_count - 1'b1;
167
        else begin
168
                axi_reset_state <= 1'b0;
169
                reset_count <= 4'hf;
170
        end
171
 
172
        // Count outstanding transactions
173
        initial pending = 0;
174
        initial outstanding = 0;
175
        always @(posedge i_clk)
176
        if ((i_reset)||(axi_reset_state))
177
        begin
178
                pending <= 0;
179
                outstanding <= 0;
180
                full_fifo <= 0;
181
        end else if ((err_state)||(!i_wb_cyc))
182
        begin
183
                pending <= 0;
184
                outstanding <= 0;
185
                full_fifo <= 0;
186
        end else case({ ((i_wb_stb)&&(!o_wb_stall)), (o_wb_ack) })
187
        2'b01: begin
188
                outstanding <= outstanding - 1'b1;
189
                pending <= (outstanding >= 2);
190
                full_fifo <= 1'b0;
191
                end
192
        2'b10: begin
193
                outstanding <= outstanding + 1'b1;
194
                pending <= 1'b1;
195
                full_fifo <= (outstanding >= {{(LGFIFOLN-2){1'b1}},2'b01});;
196
                end
197
        default: begin end
198
        endcase
199
 
200
        always @(posedge i_clk)
201
        if ((i_wb_stb)&&(!o_wb_stall))
202
                wb_we <= i_wb_we;
203
 
204
        //
205
        //
206
        // Write address logic
207
        //
208
        initial o_axi_awvalid = 0;
209
        always @(posedge i_clk)
210
        if (i_reset)
211
                o_axi_awvalid <= 0;
212
        else
213
                o_axi_awvalid <= (!o_wb_stall)&&(i_wb_stb)&&(i_wb_we)
214
                        ||(o_axi_awvalid)&&(!i_axi_awready);
215
 
216
        always @(posedge i_clk)
217
        if (!o_wb_stall)
218
                o_axi_awaddr <= { i_wb_addr, 2'b00 };
219
 
220
        //
221
        //
222
        // Read address logic
223
        //
224
        initial o_axi_arvalid = 1'b0;
225
        always @(posedge i_clk)
226
        if (i_reset)
227
                o_axi_arvalid <= 1'b0;
228
        else
229
                o_axi_arvalid <= (!o_wb_stall)&&(i_wb_stb)&&(!i_wb_we)
230
                        ||((o_axi_arvalid)&&(!i_axi_arready));
231
        always @(posedge i_clk)
232
        if (!o_wb_stall)
233
                o_axi_araddr <= { i_wb_addr, 2'b00 };
234
 
235
        //
236
        //
237
        // Write data logic
238
        //
239
        always @(posedge i_clk)
240
        if (!o_wb_stall)
241
        begin
242
                o_axi_wdata <= i_wb_data;
243
                o_axi_wstrb <= i_wb_sel;
244
        end
245
 
246
        initial o_axi_wvalid = 0;
247
        always @(posedge i_clk)
248
        if (i_reset)
249
                o_axi_wvalid <= 0;
250
        else
251
                o_axi_wvalid <= ((!o_wb_stall)&&(i_wb_stb)&&(i_wb_we))
252
                        ||((o_axi_wvalid)&&(!i_axi_wready));
253
 
254
        initial o_wb_ack = 1'b0;
255
        always @(posedge i_clk)
256
        if ((i_reset)||(!i_wb_cyc)||(err_state))
257
                o_wb_ack <= 1'b0;
258
        else if (err_state)
259
                o_wb_ack <= 1'b0;
260
        else if ((i_axi_bvalid)&&(!i_axi_bresp[1]))
261
                o_wb_ack <= 1'b1;
262
        else if ((i_axi_rvalid)&&(!i_axi_rresp[1]))
263
                o_wb_ack <= 1'b1;
264
        else
265
                o_wb_ack <= 1'b0;
266
 
267
        always @(posedge i_clk)
268
                o_wb_data <= i_axi_rdata;
269
 
270
        // Read data channel / response logic
271
        assign  o_axi_rready = 1'b1;
272
        assign  o_axi_bready = 1'b1;
273
 
274
        initial o_wb_err = 1'b0;
275
        always @(posedge i_clk)
276
        if ((i_reset)||(!i_wb_cyc)||(err_state))
277
                o_wb_err <= 1'b0;
278
        else if ((i_axi_bvalid)&&(i_axi_bresp[1]))
279
                o_wb_err <= 1'b1;
280
        else if ((i_axi_rvalid)&&(i_axi_rresp[1]))
281
                o_wb_err <= 1'b1;
282
        else
283
                o_wb_err <= 1'b0;
284
 
285
        initial err_state = 1'b0;
286
        always @(posedge i_clk)
287
        if (i_reset)
288
                err_state <= 0;
289
        else if ((i_axi_bvalid)&&(i_axi_bresp[1]))
290
                err_state <= 1'b1;
291
        else if ((i_axi_rvalid)&&(i_axi_rresp[1]))
292
                err_state <= 1'b1;
293
        else if ((pending)&&(!i_wb_cyc))
294
                err_state <= 1'b1;
295
        else if (err_pending == 0)
296
                err_state <= 0;
297
 
298
        initial err_pending = 0;
299
        always @(posedge i_clk)
300
        if (i_reset)
301
                err_pending <= 0;
302
        else case({ ((i_wb_stb)&&(!o_wb_stall)),
303
                                        ((i_axi_bvalid)||(i_axi_rvalid)) })
304
        2'b01: err_pending <= err_pending - 1'b1;
305
        2'b10: err_pending <= err_pending + 1'b1;
306
        default: begin end
307
        endcase
308
 
309
        // Make verilator happy
310
        // verilator lint_off UNUSED
311
        wire    [2:0]    unused;
312
        assign  unused = { i_wb_cyc, i_axi_bresp[0], i_axi_rresp[0] };
313
        // verilator lint_on  UNUSED
314
 
315
/////////////////////////////////////////////////////////////////////////
316
//
317
//
318
//
319
// Formal methods section
320
//
321
// These are only relevant when *proving* that this translator works
322
//
323
//
324
//
325
/////////////////////////////////////////////////////////////////////////
326
`ifdef  FORMAL
327
        reg     f_past_valid;
328
//
329
`define ASSUME  assume
330
`define ASSERT  assert
331
 
332
        // Parameters
333
        initial assert(DW == 32);
334
        initial assert(C_AXI_ADDR_WIDTH == AW+2);
335
        //
336
 
337
        //
338
        // Setup
339
        //
340
        initial f_past_valid = 1'b0;
341
        always @(posedge i_clk)
342
                f_past_valid <= 1'b1;
343
 
344
        always @(*)
345
        if (!f_past_valid)
346
                `ASSUME(i_reset);
347
 
348
        //////////////////////////////////////////////
349
        //
350
        //
351
        // Assumptions about the WISHBONE inputs
352
        //
353
        //
354
        //////////////////////////////////////////////
355
        assume property(f_past_valid || i_reset);
356
 
357
        wire    [(LGFIFOLN-1):0] f_wb_nreqs, f_wb_nacks,f_wb_outstanding;
358
        fwb_slave #(.DW(DW),.AW(AW),
359
                        .F_MAX_STALL(0),
360
                        .F_MAX_ACK_DELAY(0),
361
                        .F_LGDEPTH(LGFIFOLN),
362
                        .F_MAX_REQUESTS(FIFOLN-2))
363
                f_wb(i_clk, i_reset, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr,
364
                                        i_wb_data, i_wb_sel,
365
                                o_wb_ack, o_wb_stall, o_wb_data, o_wb_err,
366
                        f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
367
 
368
        wire    [(LGFIFOLN-1):0] f_axi_rd_outstanding,
369
                                        f_axi_wr_outstanding,
370
                                        f_axi_awr_outstanding;
371
 
372
        faxil_master #(
373
                // .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
374
                .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
375
                .F_LGDEPTH(LGFIFOLN),
376
                .F_AXI_MAXWAIT(3),
377
                .F_OPT_HAS_CACHE(1'b1),
378
                .F_AXI_MAXDELAY(3))
379
                f_axil(.i_clk(i_clk),
380
                        .i_axi_reset_n((!i_reset)&&(!axi_reset_state)),
381
                        // Write address channel
382
                        .i_axi_awready(i_axi_awready),
383
                        .i_axi_awaddr( o_axi_awaddr),
384
                        .i_axi_awcache(o_axi_awcache),
385
                        .i_axi_awprot( o_axi_awprot),
386
                        .i_axi_awvalid(o_axi_awvalid),
387
                        // Write data channel
388
                        .i_axi_wready( i_axi_wready),
389
                        .i_axi_wdata(  o_axi_wdata),
390
                        .i_axi_wstrb(  o_axi_wstrb),
391
                        .i_axi_wvalid( o_axi_wvalid),
392
                        // Write response channel
393
                        .i_axi_bresp(  i_axi_bresp),
394
                        .i_axi_bvalid( i_axi_bvalid),
395
                        .i_axi_bready( o_axi_bready),
396
                        // Read address channel
397
                        .i_axi_arready(i_axi_arready),
398
                        .i_axi_araddr( o_axi_araddr),
399
                        .i_axi_arcache(o_axi_arcache),
400
                        .i_axi_arprot( o_axi_arprot),
401
                        .i_axi_arvalid(o_axi_arvalid),
402
                        // Read data channel
403
                        .i_axi_rresp(  i_axi_rresp),
404
                        .i_axi_rvalid( i_axi_rvalid),
405
                        .i_axi_rdata(  i_axi_rdata),
406
                        .i_axi_rready( o_axi_rready),
407
                        // Counts
408
                        .f_axi_rd_outstanding( f_axi_rd_outstanding),
409
                        .f_axi_wr_outstanding( f_axi_wr_outstanding),
410
                        .f_axi_awr_outstanding( f_axi_awr_outstanding)
411
                );
412
 
413
        //////////////////////////////////////////////
414
        //
415
        //
416
        // Assumptions about the AXI inputs
417
        //
418
        //
419
        //////////////////////////////////////////////
420
 
421
 
422
        //////////////////////////////////////////////
423
        //
424
        //
425
        // Assertions about the AXI4 ouputs
426
        //
427
        //
428
        //////////////////////////////////////////////
429
 
430
        // Write response channel
431
        always @(posedge i_clk)
432
                // We keep bready high, so the other condition doesn't
433
                // need to be checked
434
                assert(o_axi_bready);
435
 
436
        // AXI read data channel signals
437
        always @(posedge i_clk)
438
                // We keep o_axi_rready high, so the other condition's
439
                // don't need to be checked here
440
                assert(o_axi_rready);
441
 
442
        //
443
        // Let's look into write requests
444
        //
445
        initial assert(!o_axi_awvalid);
446
        initial assert(!o_axi_wvalid);
447
        always @(posedge i_clk)
448
        if ((!f_past_valid)||($past(i_reset))||($past(axi_reset_state)))
449
        begin
450
                assert(!o_axi_awvalid);
451
                assert(!o_axi_wvalid);
452
        end
453
 
454
        always @(posedge i_clk)
455
        if ((f_past_valid)&&(!$past(i_reset))
456
                &&($past((i_wb_stb)&&(i_wb_we)&&(!o_wb_stall))))
457
        begin
458
                // Following any write request that we accept, awvalid
459
                // and wvalid should both be true
460
                assert(o_axi_awvalid);
461
                assert(o_axi_wvalid);
462
                assert(wb_we);
463
        end else if ((f_past_valid)&&($past(i_reset)))
464
        begin
465
                if ($past(i_axi_awready))
466
                        assert(!o_axi_awvalid);
467
                if ($past(i_axi_wready))
468
                        assert(!o_axi_wvalid);
469
        end
470
 
471
        //
472
        // AXI write address channel
473
        //
474
        always @(posedge i_clk)
475
        if ((f_past_valid)&&($past((i_wb_stb)&&(i_wb_we)&&(!o_wb_stall))))
476
                assert(o_axi_awaddr == { $past(i_wb_addr[AW-1:0]), 2'b00 });
477
 
478
        //
479
        // AXI write data channel
480
        //
481
        always @(posedge i_clk)
482
        if ((f_past_valid)&&($past(i_wb_stb)&&(i_wb_we)&&(!$past(o_wb_stall))))
483
        begin
484
                assert(o_axi_wdata == $past(i_wb_data));
485
                assert(o_axi_wstrb == $past(i_wb_sel));
486
        end
487
 
488
        //
489
        // AXI read address channel
490
        //
491
        initial assert(!o_axi_arvalid);
492
        always @(posedge i_clk)
493
        if ((f_past_valid)&&(!$past(i_reset))
494
                &&($past((i_wb_stb)&&(!i_wb_we)&&(!o_wb_stall))))
495
        begin
496
                assert(o_axi_arvalid);
497
                assert(o_axi_araddr == { $past(i_wb_addr), 2'b00 });
498
        end
499
        //
500
 
501
        //
502
        // AXI write response channel
503
        //
504
 
505
        //
506
        // AXI read data channel signals
507
        //
508
        always @(posedge i_clk)
509
        if ((f_past_valid)&&(($past(i_reset))||($past(axi_reset_state))))
510
        begin
511
                // Relate err_pending to outstanding
512
                assert(outstanding == 0);
513
                assert(err_pending == 0);
514
        end else if (!err_state)
515
                assert(err_pending == outstanding - ((o_wb_ack)||(o_wb_err)));
516
 
517
        always @(posedge i_clk)
518
        if ((f_past_valid)&&(($past(i_reset))||($past(axi_reset_state))))
519
        begin
520
                assert(f_axi_awr_outstanding == 0);
521
                assert(f_axi_wr_outstanding == 0);
522
                assert(f_axi_rd_outstanding == 0);
523
 
524
                assert(f_wb_outstanding == 0);
525
                assert(!pending);
526
                assert(outstanding == 0);
527
                assert(err_pending == 0);
528
        end else if (wb_we)
529
        begin
530
                case({o_axi_awvalid,o_axi_wvalid})
531
                2'b00: begin
532
                        `ASSERT(f_axi_awr_outstanding   == err_pending);
533
                        `ASSERT(f_axi_wr_outstanding    == err_pending);
534
                        end
535
                2'b01: begin
536
                        `ASSERT(f_axi_awr_outstanding   == err_pending);
537
                        `ASSERT(f_axi_wr_outstanding +1 == err_pending);
538
                        end
539
                2'b10: begin
540
                        `ASSERT(f_axi_awr_outstanding+1 == err_pending);
541
                        `ASSERT(f_axi_wr_outstanding    == err_pending);
542
                        end
543
                2'b11: begin
544
                        `ASSERT(f_axi_awr_outstanding+1 == err_pending);
545
                        `ASSERT(f_axi_wr_outstanding +1 == err_pending);
546
                        end
547
                endcase
548
 
549
                //
550
                `ASSERT(!o_axi_arvalid);
551
                `ASSERT(f_axi_rd_outstanding == 0);
552
        end else begin
553
                if (!o_axi_arvalid)
554
                        `ASSERT(f_axi_rd_outstanding == err_pending);
555
                else
556
                        `ASSERT(f_axi_rd_outstanding+1 == err_pending);
557
 
558
                `ASSERT(!o_axi_awvalid);
559
                `ASSERT(!o_axi_wvalid);
560
                `ASSERT(f_axi_awr_outstanding == 0);
561
                `ASSERT(f_axi_wr_outstanding == 0);
562
        end
563
 
564
        always @(*)
565
        if ((!i_reset)&&(i_wb_cyc)&&(!err_state))
566
                `ASSERT(f_wb_outstanding == outstanding);
567
 
568
        always @(posedge i_clk)
569
        if ((f_past_valid)&&(err_state))
570
                `ASSERT((o_wb_err)||(f_wb_outstanding == 0));
571
 
572
        always @(posedge i_clk)
573
                `ASSERT(pending == (outstanding != 0));
574
        //
575
        // Make sure we only create one request at a time
576
        always @(posedge i_clk)
577
                `ASSERT((!o_axi_arvalid)||(!o_axi_wvalid));
578
        always @(posedge i_clk)
579
                `ASSERT((!o_axi_arvalid)||(!o_axi_awvalid));
580
        always @(posedge i_clk)
581
        if (wb_we)
582
                `ASSERT(!o_axi_arvalid);
583
        else
584
                `ASSERT((!o_axi_awvalid)&&(!o_axi_wvalid));
585
 
586
        always @(*)
587
        if (&outstanding[LGFIFOLN-1:1])
588
                `ASSERT(full_fifo);
589
        always @(*)
590
                assert(outstanding < {(LGFIFOLN){1'b1}});
591
 
592
        // AXI cover results
593
        always @(*)
594
                cover(i_axi_bvalid && o_axi_bready);
595
        always @(*)
596
                cover(i_axi_rvalid && o_axi_rready);
597
 
598
        always @(posedge i_clk)
599
                cover(i_axi_bvalid && o_axi_bready
600
                        && $past(i_axi_bvalid && o_axi_bready)
601
                        && $past(i_axi_bvalid && o_axi_bready,2));
602
 
603
        always @(posedge i_clk)
604
                cover(i_axi_rvalid && o_axi_rready
605
                        && $past(i_axi_rvalid && o_axi_rready)
606
                        && $past(i_axi_rvalid && o_axi_rready,2));
607
 
608
        // AXI cover requests
609
        always @(posedge i_clk)
610
                cover(o_axi_arvalid && i_axi_arready
611
                        && $past(o_axi_arvalid && i_axi_arready)
612
                        && $past(o_axi_arvalid && i_axi_arready,2));
613
 
614
        always @(posedge i_clk)
615
                cover(o_axi_awvalid && i_axi_awready
616
                        && $past(o_axi_awvalid && i_axi_awready)
617
                        && $past(o_axi_awvalid && i_axi_awready,2));
618
 
619
        always @(posedge i_clk)
620
                cover(o_axi_wvalid && i_axi_wready
621
                        && $past(o_axi_wvalid && i_axi_wready)
622
                        && $past(o_axi_wvalid && i_axi_wready,2));
623
 
624
        always @(*)
625
                cover(i_axi_rvalid && o_axi_rready);
626
 
627
        // Wishbone cover results
628
        always @(*)
629
                cover(i_wb_cyc && o_wb_ack);
630
 
631
        always @(posedge i_clk)
632
                cover(i_wb_cyc && o_wb_ack
633
                        && $past(o_wb_ack)&&$past(o_wb_ack,2));
634
 
635
`endif
636
endmodule

powered by: WebSVN 2.1.0

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