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

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [bench/] [formal/] [faxil_slave.v] - Blame information for rev 16

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 16 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    faxil_slave.v (Formal properties of an AXI lite slave)
4
//
5
// Project:     Pipelined Wishbone to AXI converter
6
//
7
// Purpose:
8
//
9
// Creator:     Dan Gisselquist, Ph.D.
10
//              Gisselquist Technology, LLC
11
//
12
////////////////////////////////////////////////////////////////////////////////
13
//
14
// Copyright (C) 2018-2019, Gisselquist Technology, LLC
15
//
16
// This file is part of the pipelined Wishbone to AXI converter project, a
17
// project that contains multiple bus bridging designs and formal bus property
18
// sets.
19
//
20
// The bus bridge designs and property sets are free RTL designs: you can
21
// redistribute them and/or modify any of them under the terms of the GNU
22
// Lesser General Public License as published by the Free Software Foundation,
23
// either version 3 of the License, or (at your option) any later version.
24
//
25
// The bus bridge designs and property sets are distributed in the hope that
26
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
27
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
28
// GNU Lesser General Public License for more details.
29
//
30
// You should have received a copy of the GNU Lesser General Public License
31
// along with these designs.  (It's in the $(ROOT)/doc directory.  Run make
32
// with no target there if the PDF file isn't present.)  If not, see
33
// <http://www.gnu.org/licenses/> for a copy.
34
//
35
// License:     LGPL, v3, as defined and found on www.gnu.org,
36
//              http://www.gnu.org/licenses/lgpl.html
37
//
38
////////////////////////////////////////////////////////////////////////////////
39
//
40
//
41
`default_nettype        none
42
//
43
module faxil_slave #(
44
        parameter  C_AXI_DATA_WIDTH     = 32,// Fixed, width of the AXI R&W data
45
        parameter  C_AXI_ADDR_WIDTH     = 28,// AXI Address width (log wordsize)
46
        localparam DW                   = C_AXI_DATA_WIDTH,
47
        localparam AW                   = C_AXI_ADDR_WIDTH,
48
        parameter [0:0]   F_OPT_HAS_CACHE = 1'b0,
49
        parameter [0:0]   F_OPT_NO_READS  = 1'b0,
50
        parameter [0:0]   F_OPT_NO_WRITES = 1'b0,
51
        parameter [0:0]   F_OPT_BRESP = 1'b1,
52
        parameter [0:0]   F_OPT_RRESP = 1'b1,
53
        parameter [0:0]   F_OPT_ASSUME_RESET = 1'b1,
54
        parameter                               F_LGDEPTH       = 4,
55
        parameter       [(F_LGDEPTH-1):0]        F_AXI_MAXWAIT  = 12,
56
        parameter       [(F_LGDEPTH-1):0]        F_AXI_MAXDELAY = 12
57
        ) (
58
        input   wire                    i_clk,  // System clock
59
        input   wire                    i_axi_reset_n,
60
 
61
// AXI write address channel signals
62
        input   wire                    i_axi_awready,//Slave is ready to accept
63
        input   wire    [AW-1:0] i_axi_awaddr,   // Write address
64
        input   wire    [3:0]            i_axi_awcache,  // Write Cache type
65
        input   wire    [2:0]            i_axi_awprot,   // Write Protection type
66
        input   wire                    i_axi_awvalid,  // Write address valid
67
 
68
// AXI write data channel signals
69
        input   wire                    i_axi_wready,  // Write data ready
70
        input   wire    [DW-1:0] i_axi_wdata,    // Write data
71
        input   wire    [DW/8-1:0]       i_axi_wstrb,    // Write strobes
72
        input   wire                    i_axi_wvalid,   // Write valid
73
 
74
// AXI write response channel signals
75
        input   wire    [1:0]            i_axi_bresp,    // Write response
76
        input   wire                    i_axi_bvalid,  // Write reponse valid
77
        input   wire                    i_axi_bready,  // Response ready
78
 
79
// AXI read address channel signals
80
        input   wire                    i_axi_arready,  // Read address ready
81
        input   wire    [AW-1:0] i_axi_araddr,   // Read address
82
        input   wire    [3:0]            i_axi_arcache,  // Read Cache type
83
        input   wire    [2:0]            i_axi_arprot,   // Read Protection type
84
        input   wire                    i_axi_arvalid,  // Read address valid
85
 
86
// AXI read data channel signals
87
        input   wire    [1:0]            i_axi_rresp,   // Read response
88
        input   wire                    i_axi_rvalid,  // Read reponse valid
89
        input   wire    [DW-1:0] i_axi_rdata,   // Read data
90
        input   wire                    i_axi_rready,  // Read Response ready
91
        //
92
        output  reg     [(F_LGDEPTH-1):0]        f_axi_rd_outstanding,
93
        output  reg     [(F_LGDEPTH-1):0]        f_axi_wr_outstanding,
94
        output  reg     [(F_LGDEPTH-1):0]        f_axi_awr_outstanding
95
);
96
 
97
//*****************************************************************************
98
// Parameter declarations
99
//*****************************************************************************
100
 
101
//*****************************************************************************
102
// Internal register and wire declarations
103
//*****************************************************************************
104
 
105
        // wire w_fifo_full;
106
        wire    axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
107
                axi_rd_err, axi_wr_err;
108
        //
109
        assign  axi_ard_req = (i_axi_arvalid)&&(i_axi_arready);
110
        assign  axi_awr_req = (i_axi_awvalid)&&(i_axi_awready);
111
        assign  axi_wr_req  = (i_axi_wvalid )&&(i_axi_wready);
112
        //
113
        assign  axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready);
114
        assign  axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready);
115
        assign  axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
116
        assign  axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
117
 
118
`define SLAVE_ASSUME    assume
119
`define SLAVE_ASSERT    assert
120
 
121
        //
122
        // Setup
123
        //
124
        reg     f_past_valid;
125
        integer k;
126
 
127
        initial f_past_valid = 1'b0;
128
        always @(posedge i_clk)
129
                f_past_valid <= 1'b1;
130
 
131
        generate if (F_OPT_ASSUME_RESET)
132
        begin : ASSUME_INIITAL_RESET
133
                always @(*)
134
                if (!f_past_valid)
135
                        assume(!i_axi_reset_n);
136
        end else begin : ASSERT_INIITAL_RESET
137
                always @(*)
138
                if (!f_past_valid)
139
                        assert(!i_axi_reset_n);
140
        end endgenerate
141
 
142
        ////////////////////////////////////////////////////////////////////////
143
        //
144
        //
145
        // Reset properties
146
        //
147
        //
148
        ////////////////////////////////////////////////////////////////////////
149
 
150
        //
151
        // If asserted, the reset must be asserted for a minimum of 16 clocks
152
        reg     [3:0]    f_reset_length;
153
        initial f_reset_length = 0;
154
        always @(posedge i_clk)
155
        if (i_axi_reset_n)
156
                f_reset_length <= 0;
157
        else if (!(&f_reset_length))
158
                f_reset_length <= f_reset_length + 1'b1;
159
 
160
 
161
        generate if (F_OPT_ASSUME_RESET)
162
        begin : ASSUME_RESET
163
                always @(posedge i_clk)
164
                if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
165
                        assume(!i_axi_reset_n);
166
 
167
                always @(*)
168
                if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
169
                        assume(!i_axi_reset_n);
170
 
171
        end else begin : ASSERT_RESET
172
 
173
                always @(posedge i_clk)
174
                if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
175
                        assert(!i_axi_reset_n);
176
 
177
                always @(*)
178
                if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
179
                        assert(!i_axi_reset_n);
180
 
181
        end endgenerate
182
 
183
        always @(posedge i_clk)
184
        if ((!f_past_valid)||(!$past(i_axi_reset_n)))
185
        begin
186
                `SLAVE_ASSUME(!i_axi_arvalid);
187
                `SLAVE_ASSUME(!i_axi_awvalid);
188
                `SLAVE_ASSUME(!i_axi_wvalid);
189
                //
190
                `SLAVE_ASSERT(!i_axi_bvalid);
191
                `SLAVE_ASSERT(!i_axi_rvalid);
192
        end
193
 
194
        ////////////////////////////////////////////////////////////////////////
195
        //
196
        //
197
        // Constant input assumptions (cache and prot)
198
        //
199
        //
200
        ////////////////////////////////////////////////////////////////////////
201
 
202
        always @(*)
203
        if (i_axi_awvalid)
204
        begin
205
                `SLAVE_ASSUME(i_axi_awprot  == 3'h0);
206
                if (F_OPT_HAS_CACHE)
207
                        // Normal non-cachable, but bufferable
208
                        `SLAVE_ASSUME(i_axi_awcache == 4'h3);
209
                else
210
                        // No caching capability
211
                        `SLAVE_ASSUME(i_axi_awcache == 4'h0);
212
        end
213
 
214
        always @(*)
215
        if (i_axi_arvalid)
216
        begin
217
                `SLAVE_ASSUME(i_axi_arprot  == 3'h0);
218
                if (F_OPT_HAS_CACHE)
219
                        // Normal non-cachable, but bufferable
220
                        `SLAVE_ASSUME(i_axi_arcache == 4'h3);
221
                else
222
                        // No caching capability
223
                        `SLAVE_ASSUME(i_axi_arcache == 4'h0);
224
        end
225
 
226
        always @(*)
227
        if ((i_axi_bvalid)&&(!F_OPT_BRESP))
228
                `SLAVE_ASSERT(i_axi_bresp == 0);
229
        always @(*)
230
        if ((i_axi_rvalid)&&(!F_OPT_RRESP))
231
                `SLAVE_ASSERT(i_axi_rresp == 0);
232
        always @(*)
233
        if (i_axi_bvalid)
234
                `SLAVE_ASSERT(i_axi_bresp != 2'b01); // Exclusive access not allowed
235
        always @(*)
236
        if (i_axi_rvalid)
237
                `SLAVE_ASSERT(i_axi_rresp != 2'b01); // Exclusive access not allowed
238
 
239
 
240
        ////////////////////////////////////////////////////////////////////////
241
        //
242
        //
243
        // Stability assumptions
244
        //
245
        //
246
        ////////////////////////////////////////////////////////////////////////
247
 
248
        // Assume any response from the bus will not change prior to that
249
        // response being accepted
250
        always @(posedge i_clk)
251
        if ((f_past_valid)&&($past(i_axi_reset_n)))
252
        begin
253
                // Write address channel
254
                if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
255
                begin
256
                        `SLAVE_ASSUME(i_axi_awvalid);
257
                        `SLAVE_ASSUME($stable(i_axi_awaddr));
258
                end
259
 
260
                // Write data channel
261
                if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
262
                begin
263
                        `SLAVE_ASSUME(i_axi_wvalid);
264
                        `SLAVE_ASSUME($stable(i_axi_wstrb));
265
                        `SLAVE_ASSUME($stable(i_axi_wdata));
266
                end
267
 
268
                // Incoming Read address channel
269
                if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
270
                begin
271
                        `SLAVE_ASSUME(i_axi_arvalid);
272
                        `SLAVE_ASSUME($stable(i_axi_araddr));
273
                end
274
 
275
                if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
276
                begin
277
                        `SLAVE_ASSERT(i_axi_rvalid);
278
                        `SLAVE_ASSERT($stable(i_axi_rresp));
279
                        `SLAVE_ASSERT($stable(i_axi_rdata));
280
                end
281
 
282
                if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
283
                begin
284
                        `SLAVE_ASSERT(i_axi_bvalid);
285
                        `SLAVE_ASSERT($stable(i_axi_bresp));
286
                end
287
        end
288
 
289
        // Nothing should be returned or requested on the first clock
290
        initial `SLAVE_ASSUME(!i_axi_arvalid);
291
        initial `SLAVE_ASSUME(!i_axi_awvalid);
292
        initial `SLAVE_ASSUME(!i_axi_wvalid);
293
        //
294
        initial `SLAVE_ASSERT(!i_axi_bvalid);
295
        initial `SLAVE_ASSERT(!i_axi_rvalid);
296
 
297
        ////////////////////////////////////////////////////////////////////////
298
        //
299
        //
300
        // Insist upon a maximum delay before a request is accepted
301
        //
302
        //
303
        ////////////////////////////////////////////////////////////////////////
304
 
305
        generate if (F_AXI_MAXWAIT > 0)
306
        begin : CHECK_STALL_COUNT
307
                //
308
                // AXI write address channel
309
                //
310
                //
311
                reg     [(F_LGDEPTH-1):0]        f_axi_awstall,
312
                                                f_axi_wstall,
313
                                                f_axi_arstall,
314
                                                f_axi_bstall,
315
                                                f_axi_rstall;
316
 
317
                initial f_axi_awstall = 0;
318
                always @(posedge i_clk)
319
                if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready))
320
                        f_axi_awstall <= 0;
321
                else if ((f_axi_awr_outstanding >= f_axi_wr_outstanding)
322
                        &&(i_axi_awvalid && !i_axi_wvalid))
323
                        // If we are waiting for the write channel to be valid
324
                        // then don't count stalls
325
                        f_axi_awstall <= 0;
326
                else if ((!i_axi_bvalid)||(i_axi_bready))
327
                        f_axi_awstall <= f_axi_awstall + 1'b1;
328
 
329
                always @(*)
330
                        `SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT);
331
 
332
                //
333
                // AXI write data channel
334
                //
335
                //
336
                initial f_axi_wstall = 0;
337
                always @(posedge i_clk)
338
                if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready))
339
                        f_axi_wstall <= 0;
340
                else if ((f_axi_wr_outstanding >= f_axi_awr_outstanding)
341
                        &&(!i_axi_awvalid && i_axi_wvalid))
342
                        // If we are waiting for the write address channel
343
                        // to be valid, then don't count stalls
344
                        f_axi_wstall <= 0;
345
                else if ((!i_axi_bvalid)||(i_axi_bready))
346
                        f_axi_wstall <= f_axi_wstall + 1'b1;
347
 
348
                always @(*)
349
                        `SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT);
350
 
351
                //
352
                // AXI read address channel
353
                //
354
                //
355
                initial f_axi_arstall = 0;
356
                always @(posedge i_clk)
357
                if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready))
358
                        f_axi_arstall <= 0;
359
                else if ((!i_axi_rvalid)||(i_axi_rready))
360
                        f_axi_arstall <= f_axi_arstall + 1'b1;
361
 
362
                always @(*)
363
                        `SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT);
364
 
365
                // AXI write response channel
366
                initial f_axi_bstall = 0;
367
                always @(posedge i_clk)
368
                if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready))
369
                        f_axi_bstall <= 0;
370
                else
371
                        f_axi_bstall <= f_axi_bstall + 1'b1;
372
 
373
                always @(*)
374
                        `SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXWAIT);
375
 
376
                // AXI read response channel
377
                initial f_axi_rstall = 0;
378
                always @(posedge i_clk)
379
                if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready))
380
                        f_axi_rstall <= 0;
381
                else
382
                        f_axi_rstall <= f_axi_rstall + 1'b1;
383
 
384
                always @(*)
385
                        `SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXWAIT);
386
 
387
        end endgenerate
388
 
389
        ////////////////////////////////////////////////////////////////////////
390
        //
391
        //
392
        // Xilinx extensions/guarantees to the AXI protocol
393
        //
394
        //      1. The address line will never be more than two clocks ahead of
395
        //              the write data channel, and
396
        //      2. The write data channel will never be more than one clock
397
        //              ahead of the address channel.
398
        //
399
        //
400
        ////////////////////////////////////////////////////////////////////////
401
        //
402
        //
403
        // Rule number one:
404
        always @(posedge i_clk)
405
        if ((i_axi_reset_n)&&($past(i_axi_reset_n))
406
                &&($past(i_axi_awvalid && !i_axi_wvalid,2))
407
                        &&($past(f_axi_awr_outstanding>=f_axi_wr_outstanding,2))
408
                        &&(!$past(i_axi_wvalid)))
409
                `SLAVE_ASSUME(i_axi_wvalid);
410
 
411
        // Rule number two:
412
        always @(posedge i_clk)
413
        if ((i_axi_reset_n)&&(!$past(i_axi_awvalid))&&($past(i_axi_wvalid))
414
                        &&(f_axi_awr_outstanding < f_axi_wr_outstanding))
415
                `SLAVE_ASSUME(i_axi_awvalid);
416
 
417
        ////////////////////////////////////////////////////////////////////////
418
        //
419
        //
420
        // Count outstanding transactions.  With these measures, we count
421
        // once per any burst.
422
        //
423
        //
424
        ////////////////////////////////////////////////////////////////////////
425
        initial f_axi_awr_outstanding = 0;
426
        always @(posedge i_clk)
427
        if (!i_axi_reset_n)
428
                f_axi_awr_outstanding <= 0;
429
        else case({ (axi_awr_req), (axi_wr_ack) })
430
                2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1;
431
                2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
432
                default: begin end
433
        endcase
434
 
435
        initial f_axi_wr_outstanding = 0;
436
        always @(posedge i_clk)
437
        if (!i_axi_reset_n)
438
                f_axi_wr_outstanding <= 0;
439
        else case({ (axi_wr_req), (axi_wr_ack) })
440
        2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1;
441
        2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 1'b1;
442
        endcase
443
 
444
        initial f_axi_rd_outstanding = 0;
445
        always @(posedge i_clk)
446
        if (!i_axi_reset_n)
447
                f_axi_rd_outstanding <= 0;
448
        else case({ (axi_ard_req), (axi_rd_ack) })
449
        2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
450
        2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1;
451
        endcase
452
 
453
        //
454
        // Do not let the number of outstanding requests overflow
455
        always @(posedge i_clk)
456
                `SLAVE_ASSERT(f_axi_wr_outstanding  < {(F_LGDEPTH){1'b1}});
457
        always @(posedge i_clk)
458
                `SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}});
459
        always @(posedge i_clk)
460
                `SLAVE_ASSERT(f_axi_rd_outstanding  < {(F_LGDEPTH){1'b1}});
461
 
462
        //
463
        // That means that requests need to stop when we're almost full
464
        always @(posedge i_clk)
465
        if (f_axi_awr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
466
                assert(!i_axi_awvalid);
467
        always @(posedge i_clk)
468
        if (f_axi_wr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
469
                assert(!i_axi_wvalid);
470
        always @(posedge i_clk)
471
        if (f_axi_rd_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
472
                assert(!i_axi_arvalid);
473
 
474
        ////////////////////////////////////////////////////////////////////////
475
        //
476
        //
477
        // Insist that all responses are returned in less than a maximum delay
478
        // In this case, we count responses within a burst, rather than entire
479
        // bursts.
480
        //
481
        //
482
        ////////////////////////////////////////////////////////////////////////
483
        generate if (F_AXI_MAXDELAY > 0)
484
        begin : CHECK_MAX_DELAY
485
 
486
                reg     [(F_LGDEPTH-1):0]        f_axi_wr_ack_delay,
487
                                                f_axi_rd_ack_delay;
488
 
489
                initial f_axi_rd_ack_delay = 0;
490
                always @(posedge i_clk)
491
                if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0))
492
                        f_axi_rd_ack_delay <= 0;
493
                else
494
                        f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
495
 
496
                initial f_axi_wr_ack_delay = 0;
497
                always @(posedge i_clk)
498
                if ((!i_axi_reset_n)||(i_axi_bvalid)||(f_axi_wr_outstanding==0))
499
                        f_axi_wr_ack_delay <= 0;
500
                else if (f_axi_wr_outstanding > 0)
501
                        f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
502
 
503
                always @(*)
504
                        `SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY);
505
 
506
                always @(*)
507
                        `SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY);
508
 
509
        end endgenerate
510
 
511
        ////////////////////////////////////////////////////////////////////////
512
        //
513
        //
514
        // Assume acknowledgements must follow requests
515
        //
516
        // The f_axi*outstanding counters count the number of requests.  No
517
        // acknowledgment should issue without a pending request
518
        // burst.  Further, the spec is clear: you can't acknowledge something
519
        // on the same clock you get the request.  There must be at least one
520
        // clock delay.
521
        //
522
        //
523
        ////////////////////////////////////////////////////////////////////////
524
 
525
        //
526
        // AXI write response channel
527
        //
528
        always @(posedge i_clk)
529
        if (i_axi_bvalid)
530
        begin
531
                `SLAVE_ASSERT(f_axi_awr_outstanding > 0);
532
                `SLAVE_ASSERT(f_axi_wr_outstanding  > 0);
533
        end
534
 
535
        //
536
        // AXI read data channel signals
537
        //
538
        always @(posedge i_clk)
539
        if (i_axi_rvalid)
540
                `SLAVE_ASSERT(f_axi_rd_outstanding > 0);
541
 
542
        ////////////////////////////////////////////////////////////////////////
543
        //
544
        //
545
        // Optionally disable either read or write channels (or both??)
546
        //
547
        //
548
        ////////////////////////////////////////////////////////////////////////
549
 
550
        initial assert((!F_OPT_NO_READS)||(!F_OPT_NO_WRITES));
551
 
552
        generate if (F_OPT_NO_READS)
553
        begin : NO_READS
554
 
555
                always @(*)
556
                        `SLAVE_ASSUME(i_axi_arvalid == 0);
557
                always @(*)
558
                        `SLAVE_ASSERT(f_axi_rd_outstanding == 0);
559
                always @(*)
560
                        `SLAVE_ASSERT(i_axi_rvalid == 0);
561
 
562
        end endgenerate
563
 
564
        generate if (F_OPT_NO_WRITES)
565
        begin : NO_WRITES
566
 
567
                always @(*)
568
                        `SLAVE_ASSUME(i_axi_awvalid == 0);
569
                always @(*)
570
                        `SLAVE_ASSUME(i_axi_wvalid == 0);
571
                always @(*)
572
                        `SLAVE_ASSERT(f_axi_wr_outstanding == 0);
573
                always @(*)
574
                        `SLAVE_ASSERT(f_axi_awr_outstanding == 0);
575
                always @(*)
576
                        `SLAVE_ASSERT(i_axi_bvalid == 0);
577
 
578
        end endgenerate
579
 
580
        ////////////////////////////////////////////////////////////////////////
581
        //
582
        //
583
        // Cover properties
584
        //
585
        // We'll use this to prove that transactions are even possible, and
586
        // hence that we haven't so constrained the bus that nothing can take
587
        // place.
588
        //
589
        //
590
        ////////////////////////////////////////////////////////////////////////
591
 
592
        //
593
        // AXI write response channel
594
        //
595
        always @(posedge i_clk)
596
        if (!F_OPT_NO_WRITES)
597
                cover((i_axi_bvalid)&&(i_axi_bready));
598
 
599
        //
600
        // AXI read response channel
601
        //
602
        always @(posedge i_clk)
603
        if (!F_OPT_NO_READS)
604
                cover((i_axi_rvalid)&&(i_axi_rready));
605
endmodule

powered by: WebSVN 2.1.0

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