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

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [bench/] [formal/] [faxi_slave.v] - Blame information for rev 15

Go to most recent revision | Details | Compare with Previous | View Log

Line No. Rev Author Line
1 10 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    faxi_slave.v (Formal properties of an AXI 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) 2017, Gisselquist Technology, LLC
15
//
16
// This program is free software (firmware): you can redistribute it and/or
17
// modify it under the terms of  the GNU General Public License as published
18
// by the Free Software Foundation, either version 3 of the License, or (at
19
// your option) any later version.
20
//
21
// This program is distributed in the hope that it will be useful, but WITHOUT
22
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
23
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
24
// for more details.
25
//
26
// You should have received a copy of the GNU General Public License along
27
// with this program.  (It's in the $(ROOT)/doc directory, run make with no
28
// target there if the PDF file isn't present.)  If not, see
29
// <http://www.gnu.org/licenses/> for a copy.
30
//
31
// License:     GPL, v3, as defined and found on www.gnu.org,
32
//              http://www.gnu.org/licenses/gpl.html
33
//
34
//
35
////////////////////////////////////////////////////////////////////////////////
36
//
37
//
38
`default_nettype        none
39
//
40
module faxi_slave #(
41
        parameter C_AXI_ID_WIDTH        = 3, // The AXI id width used for R&W
42
                                             // This is an int between 1-16
43
        parameter C_AXI_DATA_WIDTH      = 128,// Width of the AXI R&W data
44
        parameter C_AXI_ADDR_WIDTH      = 28,   // AXI Address width (log wordsize)
45
        localparam DW                   = C_AXI_DATA_WIDTH,
46
        localparam AW                   = C_AXI_ADDR_WIDTH,
47
        parameter       [(C_AXI_ID_WIDTH-1):0]   F_AXI_MAXSTALL = 3,
48
        parameter       [(C_AXI_ID_WIDTH-1):0]   F_AXI_MAXDELAY = 3,
49
        parameter [0:0] F_STRICT_ORDER    = 0,     // Reorder, or not? 0 -> Reorder
50
        parameter [0:0] F_CONSECUTIVE_IDS= 0,      // 0=ID's must be consecutive
51
        parameter [0:0] F_OPT_BURSTS    = 1'b1,   // Check burst lengths
52
        parameter [0:0] F_CHECK_IDS       = 1'b1  // Check ID's upon issue&return
53
        ) (
54
        input                           i_clk,  // System clock
55
        input                           i_axi_reset_n,
56
 
57
// AXI write address channel signals
58
        input                           i_axi_awready, // Slave is ready to accept
59
        input   wire    [C_AXI_ID_WIDTH-1:0]     i_axi_awid,     // Write ID
60
        input   wire    [AW-1:0] i_axi_awaddr,   // Write address
61
        input   wire    [7:0]            i_axi_awlen,    // Write Burst Length
62
        input   wire    [2:0]            i_axi_awsize,   // Write Burst size
63
        input   wire    [1:0]            i_axi_awburst,  // Write Burst type
64
        input   wire    [0:0]             i_axi_awlock,   // Write lock type
65
        input   wire    [3:0]            i_axi_awcache,  // Write Cache type
66
        input   wire    [2:0]            i_axi_awprot,   // Write Protection type
67
        input   wire    [3:0]            i_axi_awqos,    // Write Quality of Svc
68
        input   wire                    i_axi_awvalid,  // Write address valid
69
 
70
// AXI write data channel signals
71
        input   wire                    i_axi_wready,  // Write data ready
72
        input   wire    [DW-1:0] i_axi_wdata,    // Write data
73
        input   wire    [DW/8-1:0]       i_axi_wstrb,    // Write strobes
74
        input   wire                    i_axi_wlast,    // Last write transaction
75
        input   wire                    i_axi_wvalid,   // Write valid
76
 
77
// AXI write response channel signals
78
        input   wire [C_AXI_ID_WIDTH-1:0] i_axi_bid,     // Response ID
79
        input   wire [1:0]               i_axi_bresp,    // Write response
80
        input   wire                    i_axi_bvalid,  // Write reponse valid
81
        input   wire                    i_axi_bready,  // Response ready
82
 
83
// AXI read address channel signals
84
        input   wire                    i_axi_arready,  // Read address ready
85
        input   wire    [C_AXI_ID_WIDTH-1:0]     i_axi_arid,     // Read ID
86
        input   wire    [AW-1:0] i_axi_araddr,   // Read address
87
        input   wire    [7:0]            i_axi_arlen,    // Read Burst Length
88
        input   wire    [2:0]            i_axi_arsize,   // Read Burst size
89
        input   wire    [1:0]            i_axi_arburst,  // Read Burst type
90
        input   wire    [0:0]             i_axi_arlock,   // Read lock type
91
        input   wire    [3:0]            i_axi_arcache,  // Read Cache type
92
        input   wire    [2:0]            i_axi_arprot,   // Read Protection type
93
        input   wire    [3:0]            i_axi_arqos,    // Read Protection type
94
        input   wire                    i_axi_arvalid,  // Read address valid
95
 
96
// AXI read data channel signals
97
        input   wire [C_AXI_ID_WIDTH-1:0] i_axi_rid,     // Response ID
98
        input   wire [1:0]               i_axi_rresp,   // Read response
99
        input   wire                    i_axi_rvalid,  // Read reponse valid
100
        input   wire [DW-1:0]            i_axi_rdata,    // Read data
101
        input   wire                    i_axi_rlast,    // Read last
102
        input   wire                    i_axi_rready,  // Read Response ready
103
        //
104
        output  reg     [(C_AXI_ID_WIDTH-1):0]   f_axi_rd_outstanding,
105
        output  reg     [(C_AXI_ID_WIDTH-1):0]   f_axi_wr_outstanding,
106
        output  reg     [(C_AXI_ID_WIDTH-1):0]   f_axi_awr_outstanding,
107
        output  reg [((1<<C_AXI_ID_WIDTH)-1):0]  f_axi_rd_id_outstanding,
108
        output  reg [((1<<C_AXI_ID_WIDTH)-1):0]  f_axi_awr_id_outstanding,
109
        output  reg [((1<<C_AXI_ID_WIDTH)-1):0]  f_axi_wr_id_outstanding
110
 
111
);
112
        reg [((1<<C_AXI_ID_WIDTH)-1):0]  f_axi_wr_id_complete;
113
 
114
//*****************************************************************************
115
// Parameter declarations
116
//*****************************************************************************
117
 
118
        localparam      LG_AXI_DW       = ( C_AXI_DATA_WIDTH ==   8) ? 3
119
                                        : ((C_AXI_DATA_WIDTH ==  16) ? 4
120
                                        : ((C_AXI_DATA_WIDTH ==  32) ? 5
121
                                        : ((C_AXI_DATA_WIDTH ==  64) ? 6
122
                                        : ((C_AXI_DATA_WIDTH == 128) ? 7
123
                                        : 8))));
124
 
125
        localparam      LG_WB_DW        = ( DW ==   8) ? 3
126
                                        : ((DW ==  16) ? 4
127
                                        : ((DW ==  32) ? 5
128
                                        : ((DW ==  64) ? 6
129
                                        : ((DW == 128) ? 7
130
                                        : 8))));
131
        localparam      LGFIFOLN = C_AXI_ID_WIDTH;
132
        localparam      FIFOLN = (1<<LGFIFOLN);
133
 
134
 
135
//*****************************************************************************
136
// Internal register and wire declarations
137
//*****************************************************************************
138
 
139
// Things we're not changing ...
140
        always @(*)
141
        begin
142
        assume(i_axi_awlen   == 8'h0);  // Burst length is one
143
        assume(i_axi_awsize  == 3'b101);        // maximum bytes per burst is 32
144
        assume(i_axi_awburst == 2'b01); // Incrementing address (ignored)
145
        assume(i_axi_arburst == 2'b01); // Incrementing address (ignored)
146
        assume(i_axi_awlock  == 1'b0);  // Normal signaling
147
        assume(i_axi_arlock  == 1'b0);  // Normal signaling
148
        assume(i_axi_awcache == 4'h2);  // Normal: no cache, no buffer
149
        assume(i_axi_arcache == 4'h2);  // Normal: no cache, no buffer
150
        assume(i_axi_awprot  == 3'b010);// Unpriviledged, unsecure, data access
151
        assume(i_axi_arprot  == 3'b010);// Unpriviledged, unsecure, data access
152
        assume(i_axi_awqos   == 4'h0);  // Lowest quality of service (unused)
153
        assume(i_axi_arqos   == 4'h0);  // Lowest quality of service (unused)
154
        end
155
 
156
        // wire w_fifo_full;
157
        wire    axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
158
                axi_rd_err, axi_wr_err;
159
        //
160
        assign  axi_ard_req = (i_axi_arvalid)&&(i_axi_arready);
161
        assign  axi_awr_req = (i_axi_awvalid)&&(i_axi_awready);
162
        assign  axi_wr_req  = (i_axi_wvalid )&&(i_axi_wready);
163
        //
164
        assign  axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready);
165
        assign  axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready);
166
        assign  axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
167
        assign  axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
168
 
169
        //
170
        // Setup
171
        //
172
        reg     f_past_valid;
173
        integer k;
174
 
175
        initial f_past_valid = 1'b0;
176
        always @(posedge i_clk)
177
                f_past_valid <= 1'b1;
178
        always @(*)
179
                if (!f_past_valid)
180
                        assume(!i_axi_reset_n);
181
 
182
        //
183
        // All signals must be synchronous with the clock
184
        //
185
        always @($global_clock)
186
        if (f_past_valid) begin
187
                // Assume our inputs will only change on the positive edge
188
                // of the clock
189
                if (!$rose(i_clk))
190
                begin
191
                        // AXI inputs
192
                        assert($stable(i_axi_awready));
193
                        assert($stable(i_axi_wready));
194
                        //
195
                        assert($stable(i_axi_bid));
196
                        assert($stable(i_axi_bresp));
197
                        assert($stable(i_axi_bvalid));
198
                        assert($stable(i_axi_arready));
199
                        //
200
                        assert($stable(i_axi_rid));
201
                        assert($stable(i_axi_rresp));
202
                        assert($stable(i_axi_rvalid));
203
                        assert($stable(i_axi_rdata));
204
                        assert($stable(i_axi_rlast));
205
                        //
206
                        // AXI outputs
207
                        //
208
                        assume($stable(i_axi_awvalid));
209
                        assume($stable(i_axi_awid));
210
                        assume($stable(i_axi_awlen));
211
                        assume($stable(i_axi_awsize));
212
                        assume($stable(i_axi_awlock));
213
                        assume($stable(i_axi_awcache));
214
                        assume($stable(i_axi_awprot));
215
                        assume($stable(i_axi_awqos));
216
                        //
217
                        assume($stable(i_axi_wvalid));
218
                        assume($stable(i_axi_wdata));
219
                        assume($stable(i_axi_wstrb));
220
                        assume($stable(i_axi_wlast));
221
                        //
222
                        assume($stable(i_axi_arvalid));
223
                        assume($stable(i_axi_arid));
224
                        assume($stable(i_axi_arlen));
225
                        assume($stable(i_axi_arsize));
226
                        assume($stable(i_axi_arburst));
227
                        assume($stable(i_axi_arlock));
228
                        assume($stable(i_axi_arprot));
229
                        assume($stable(i_axi_arqos));
230
                        //
231
                        assume($stable(i_axi_bready));
232
                        //
233
                        assume($stable(i_axi_rready));
234
                        //
235
                        // Formal outputs
236
                        //
237
                        assume($stable(f_axi_rd_outstanding));
238
                        assume($stable(f_axi_wr_outstanding));
239
                        assume($stable(f_axi_awr_outstanding));
240
                end
241
        end
242
 
243
        ////////////////////////////////////////////////////
244
        //
245
        //
246
        // Reset properties
247
        //
248
        //
249
        ////////////////////////////////////////////////////
250
 
251
        always @(posedge i_clk)
252
        if ((f_past_valid)&&(!$past(i_axi_reset_n)))
253
        begin
254
                assume(!i_axi_arvalid);
255
                assume(!i_axi_awvalid);
256
                assume(!i_axi_wvalid);
257
                assert(!i_axi_bvalid);
258
                assert(!i_axi_rvalid);
259
        end
260
 
261
        ////////////////////////////////////////////////////
262
        //
263
        //
264
        // Stability assumptions, AXI inputs/responses
265
        //
266
        //
267
        ////////////////////////////////////////////////////
268
 
269
        // Assume any response from the bus will not change prior to that
270
        // response being accepted
271
        always @(posedge i_clk)
272
        if (f_past_valid)
273
        begin
274
                if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
275
                begin
276
                        assert(i_axi_rid    == $past(i_axi_rid));
277
                        assert(i_axi_rresp  == $past(i_axi_rresp));
278
                        assert(i_axi_rdata  == $past(i_axi_rdata));
279
                        assert(i_axi_rlast  == $past(i_axi_rlast));
280
                end
281
 
282
                if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
283
                begin
284
                        assert(i_axi_bid    == $past(i_axi_bid));
285
                        assert(i_axi_bresp  == $past(i_axi_bresp));
286
                end
287
        end
288
 
289
        // Nothing should be returning a result on the first clock
290
        initial assert(!i_axi_bvalid);
291
        initial assert(!i_axi_rvalid);
292
        //
293
        initial assume(!i_axi_arvalid);
294
        initial assume(!i_axi_awvalid);
295
        initial assume(!i_axi_wvalid);
296
 
297
        //////////////////////////////////////////////
298
        //
299
        //
300
        // Stability assumptions, AXI outputs/requests
301
        //
302
        //
303
        //////////////////////////////////////////////
304
 
305
        // Read address chanel
306
        always @(posedge i_clk)
307
        if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
308
        begin
309
                assume(i_axi_arvalid);
310
                assume($stable(i_axi_arid));
311
                assume($stable(i_axi_araddr));
312
                assume($stable(i_axi_arlen));
313
                assume($stable(i_axi_arsize));
314
                assume($stable(i_axi_arburst));
315
                assume($stable(i_axi_arlock));
316
                assume($stable(i_axi_arcache));
317
                assume($stable(i_axi_arprot));
318
                assume($stable(i_axi_arqos));
319
                assume($stable(i_axi_arvalid));
320
        end
321
 
322
        // If valid, but not ready, on any channel is true, nothing changes
323
        // until valid && ready
324
        always @(posedge i_clk)
325
        if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
326
        begin
327
                assume($stable(i_axi_awid));
328
                assume($stable(i_axi_awaddr));
329
                assume($stable(i_axi_awlen));
330
                assume($stable(i_axi_awsize));
331
                assume($stable(i_axi_awburst));
332
                assume($stable(i_axi_awlock));
333
                assume($stable(i_axi_awcache));
334
                assume($stable(i_axi_awprot));
335
                assume($stable(i_axi_awqos));
336
                assume($stable(i_axi_awvalid));
337
        end
338
 
339
        always @(posedge i_clk)
340
        if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
341
        begin
342
                // AXI write data channel signals
343
                assume($stable(i_axi_wdata));
344
                assume($stable(i_axi_wstrb));
345
                assume($stable(i_axi_wlast));
346
                assume($stable(i_axi_wvalid));
347
        end
348
 
349
        //
350
        //
351
 
352
        ///////////////////////////////////////////////////////////////////
353
        //
354
        //
355
        // Insist upon a maximum delay before a request is accepted
356
        //
357
        //
358
        ///////////////////////////////////////////////////////////////////
359
 
360
        //
361
        // AXI write address channel
362
        //
363
        //
364
        reg     [(C_AXI_ID_WIDTH):0]     f_axi_awstall;
365
        initial f_axi_awstall = 0;
366
        always @(posedge i_clk)
367
                if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready))
368
                        f_axi_awstall <= 0;
369
                else
370
                        f_axi_awstall <= f_axi_awstall + 1'b1;
371
        always @(*)
372
                assert((F_AXI_MAXSTALL==0)||(f_axi_awstall < F_AXI_MAXSTALL));
373
 
374
        //
375
        // AXI write data channel
376
        //
377
        //
378
        // AXI explicitly allows write bursts with zero strobes.  This is part
379
        // of how a transaction is aborted (if at all).
380
        //always @(*) if (i_axi_wvalid) assume(|i_axi_wstrb);
381
 
382
        reg     [(C_AXI_ID_WIDTH):0]     f_axi_wstall;
383
        initial f_axi_wstall = 0;
384
        always @(posedge i_clk)
385
                if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready))
386
                        f_axi_wstall <= 0;
387
                else
388
                        f_axi_wstall <= f_axi_wstall + 1'b1;
389
        always @(*)
390
                assert((F_AXI_MAXSTALL==0)||(f_axi_wstall < F_AXI_MAXSTALL));
391
 
392
 
393
        //
394
        // AXI read address channel
395
        //
396
        //
397
        reg     [(C_AXI_ID_WIDTH):0]     f_axi_arstall;
398
        initial f_axi_arstall = 0;
399
        always @(posedge i_clk)
400
                if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready))
401
                        f_axi_arstall <= 0;
402
                else
403
                        f_axi_arstall <= f_axi_arstall + 1'b1;
404
        always @(*)
405
                assert((F_AXI_MAXSTALL==0)||(f_axi_arstall < F_AXI_MAXSTALL));
406
 
407
 
408
        ////////////////////////////////////////////////////////////////////////
409
        //
410
        //
411
        // Count outstanding transactions.  With these measures, we count
412
        // once per any burst.
413
        //
414
        //
415
        ////////////////////////////////////////////////////////////////////////
416
        initial f_axi_awr_outstanding = 0;
417
        always @(posedge i_clk)
418
                if (!i_axi_reset_n)
419
                        f_axi_awr_outstanding <= 0;
420
                else case({ (axi_awr_req), (axi_wr_ack) })
421
                        2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1;
422
                        2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
423
                        default: begin end
424
                endcase
425
 
426
        initial f_axi_wr_outstanding = 0;
427
        always @(posedge i_clk)
428
                if (!i_axi_reset_n)
429
                        f_axi_wr_outstanding <= 0;
430
                else case({ (axi_wr_req)&&(i_axi_wlast), (axi_wr_ack) })
431
                2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1;
432
                2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 1'b1;
433
                endcase
434
 
435
        initial f_axi_rd_outstanding = 0;
436
        always @(posedge i_clk)
437
                if (!i_axi_reset_n)
438
                        f_axi_rd_outstanding <= 0;
439
                else case({ (axi_ard_req), (axi_rd_ack)&&(i_axi_rlast) })
440
                2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
441
                2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1;
442
                endcase
443
 
444
        // Do not let the number of outstanding requests overflow
445
        always @(posedge i_clk)
446
                assume(f_axi_wr_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
447
        always @(posedge i_clk)
448
                assume(f_axi_awr_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
449
        always @(posedge i_clk)
450
                assume(f_axi_rd_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
451
 
452
        ////////////////////////////////////////////////////////////////////////
453
        //
454
        //
455
        // Insist that all responses are returned in less than a maximum delay
456
        // In this case, we count responses within a burst, rather than entire
457
        // bursts.
458
        //
459
        //
460
        ////////////////////////////////////////////////////////////////////////
461
 
462
        reg     [(C_AXI_ID_WIDTH):0]     f_axi_wr_ack_delay,
463
                                        f_axi_awr_ack_delay,
464
                                        f_axi_rd_ack_delay;
465
 
466
        initial f_axi_rd_ack_delay = 0;
467
        always @(posedge i_clk)
468
                if ((!i_axi_reset_n)||(axi_rd_ack))
469
                        f_axi_rd_ack_delay <= 0;
470
                else if (f_axi_rd_outstanding > 0)
471
                        f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
472
 
473
        initial f_axi_wr_ack_delay = 0;
474
        always @(posedge i_clk)
475
                if ((!i_axi_reset_n)||(axi_wr_ack))
476
                        f_axi_wr_ack_delay <= 0;
477
                else if (f_axi_wr_outstanding > 0)
478
                        f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
479
 
480
        initial f_axi_awr_ack_delay = 0;
481
        always @(posedge i_clk)
482
                if ((!i_axi_reset_n)||(axi_wr_ack))
483
                        f_axi_awr_ack_delay <= 0;
484
                else if (f_axi_awr_outstanding > 0)
485
                        f_axi_awr_ack_delay <= f_axi_awr_ack_delay + 1'b1;
486
 
487
        always @(posedge i_clk)
488
                assert((F_AXI_MAXDELAY==0)||(f_axi_rd_ack_delay < F_AXI_MAXDELAY));
489
 
490
        always @(posedge i_clk)
491
                assert((F_AXI_MAXDELAY==0)||(f_axi_wr_ack_delay < F_AXI_MAXDELAY));
492
 
493
        always @(posedge i_clk)
494
                assert((F_AXI_MAXDELAY==0)||(f_axi_awr_ack_delay < F_AXI_MAXDELAY));
495
 
496
        ////////////////////////////////////////////////////////////////////////
497
        //
498
        //
499
        // Assume all acknowledgements must follow requests
500
        //
501
        // The outstanding count is a count of bursts, but the acknowledgements
502
        // we are looking for are individual.  Hence, there should be no
503
        // individual acknowledgements coming back if there's no outstanding
504
        // burst.
505
        //
506
        //
507
        ////////////////////////////////////////////////////////////////////////
508
 
509
        //
510
        // AXI write response channel
511
        //
512
        always @(posedge i_clk)
513
                if ((!axi_awr_req)&&(axi_wr_ack))
514
                        assert(f_axi_awr_outstanding > 0);
515
        always @(posedge i_clk)
516
                if ((!axi_wr_req)&&(axi_wr_ack))
517
                        assert(f_axi_wr_outstanding > 0);
518
 
519
        //
520
        // AXI read data channel signals
521
        //
522
        initial f_axi_rd_outstanding = 0;
523
        always @(posedge i_clk)
524
                if ((!axi_ard_req)&&(axi_rd_ack))
525
                        assert(f_axi_rd_outstanding > 0);
526
 
527
        ///////////////////////////////////////////////////////////////////
528
        //
529
        //
530
        // Manage the ID buffer.  Basic rules apply such as you can't
531
        // make a request of an already requested ID # before that ID
532
        // is returned, etc.
533
        //
534
        // Elements in this buffer reference transactions--possibly burst
535
        // transactions and not necessarily the individual values.
536
        //
537
        //
538
        /////////////////////////////////////////////////////////////////// 
539
        // Now, let's look into that FIFO.  Without it, we know nothing about
540
        // the ID's
541
 
542
        initial f_axi_rd_id_outstanding = 0;
543
        initial f_axi_wr_id_outstanding = 0;
544
        initial f_axi_awr_id_outstanding = 0;
545
        initial f_axi_wr_id_complete = 0;
546
        always @(posedge i_clk)
547
                if (!i_axi_reset_n)
548
                begin
549
                        f_axi_rd_id_outstanding <= 0;
550
                        f_axi_wr_id_outstanding <= 0;
551
                        f_axi_wr_id_complete <= 0;
552
                        f_axi_awr_id_outstanding <= 0;
553
                end else begin
554
                // When issuing a write
555
                if (axi_awr_req)
556
                begin
557
                        if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS))
558
                                assume(f_axi_awr_id_outstanding[i_axi_awid+1'b1] == 1'b0);
559
                        assume((!F_CHECK_IDS)
560
                                ||(f_axi_awr_id_outstanding[i_axi_awid] == 1'b0));
561
                        assume((!F_CHECK_IDS)
562
                                ||(f_axi_wr_id_complete[i_axi_awid] == 1'b0));
563
                        f_axi_awr_id_outstanding[i_axi_awid] <= 1'b1;
564
                        f_axi_wr_id_complete[i_axi_awid] <= 1'b0;
565
                end
566
 
567
                if (axi_wr_req)
568
                begin
569
                        if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS))
570
                                assume(f_axi_wr_id_outstanding[i_axi_awid+1'b1] == 1'b0);
571
                        assume((!F_CHECK_IDS)
572
                                ||(f_axi_wr_id_outstanding[i_axi_awid] == 1'b0));
573
                        f_axi_wr_id_outstanding[i_axi_awid] <= 1'b1;
574
                        if (i_axi_wlast)
575
                        begin
576
                                assert(f_axi_wr_id_complete[i_axi_awid] == 1'b0);
577
                                f_axi_wr_id_complete[i_axi_awid] <= 1'b1;
578
                        end
579
                end
580
 
581
                // When issuing a read
582
                if (axi_ard_req)
583
                begin
584
                        if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS))
585
                                assume(f_axi_rd_id_outstanding[i_axi_arid+1'b1] == 1'b0);
586
                        assume((!F_CHECK_IDS)
587
                                ||(f_axi_rd_id_outstanding[i_axi_arid] == 1'b0));
588
                        f_axi_rd_id_outstanding[i_axi_arid] <= 1'b1;
589
                end
590
 
591
                // When a write is acknowledged
592
                if (axi_wr_ack)
593
                begin
594
                        if (F_CHECK_IDS)
595
                        begin
596
                                assert(f_axi_awr_id_outstanding[i_axi_bid]);
597
                                assert(f_axi_wr_id_outstanding[i_axi_bid]);
598
                                assert((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS)
599
                                        ||(!f_axi_wr_id_outstanding[i_axi_bid-1'b1]));
600
                                assert((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS)
601
                                        ||(!f_axi_awr_id_outstanding[i_axi_bid-1'b1]));
602
                                assert(f_axi_wr_id_complete[i_axi_bid]);
603
                        end
604
                        f_axi_awr_id_outstanding[i_axi_bid] <= 1'b0;
605
                        f_axi_wr_id_outstanding[i_axi_bid]  <= 1'b0;
606
                        f_axi_wr_id_complete[i_axi_bid]     <= 1'b0;
607
                end
608
 
609
                // When a read is acknowledged
610
                if (axi_rd_ack)
611
                begin
612
                        if (F_CHECK_IDS)
613
                        begin
614
                                assert(f_axi_rd_id_outstanding[i_axi_rid]);
615
                                assert((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS)
616
                                        ||(!f_axi_rd_id_outstanding[i_axi_rid-1'b1]));
617
                        end
618
 
619
                        if (i_axi_rlast)
620
                                f_axi_rd_id_outstanding[i_axi_rid] <= 1'b0;
621
                end
622
        end
623
 
624
 
625
        reg     [LGFIFOLN:0]     f_axi_rd_id_outstanding_count,
626
                                f_axi_awr_id_outstanding_count,
627
                                f_axi_wr_id_outstanding_count;
628
 
629
        initial f_axi_rd_id_outstanding_count = 0;
630
        initial f_axi_awr_id_outstanding_count = 0;
631
        initial f_axi_wr_id_outstanding_count = 0;
632
        always @(*)
633
        begin
634
                //
635
                f_axi_rd_id_outstanding_count = 0;
636
                for(k=0; k< FIFOLN; k=k+1)
637
                        if (f_axi_rd_id_outstanding[k])
638
                                f_axi_rd_id_outstanding_count
639
                                        = f_axi_rd_id_outstanding_count +1;
640
                //
641
                f_axi_wr_id_outstanding_count = 0;
642
                for(k=0; k< FIFOLN; k=k+1)
643
                        if (f_axi_wr_id_outstanding[k])
644
                                f_axi_wr_id_outstanding_count = f_axi_wr_id_outstanding_count +1;
645
                f_axi_awr_id_outstanding_count = 0;
646
                for(k=0; k< FIFOLN; k=k+1)
647
                        if (f_axi_awr_id_outstanding[k])
648
                                f_axi_awr_id_outstanding_count = f_axi_awr_id_outstanding_count +1;
649
        end
650
 
651
        always @(*)
652
                assume((!F_CHECK_IDS)||(f_axi_awr_outstanding== f_axi_awr_id_outstanding_count));
653
 
654
        always @(*)
655
                assume((!F_CHECK_IDS)||(f_axi_wr_outstanding == f_axi_wr_id_outstanding_count));
656
 
657
        always @(*)
658
                assume((!F_CHECK_IDS)||(f_axi_rd_outstanding == f_axi_rd_id_outstanding_count));
659
 
660
        always @(*)
661
                assume( ((f_axi_wr_id_complete)&(~f_axi_awr_id_outstanding)) == 0);
662
 
663
        generate if (F_OPT_BURSTS)
664
        begin
665
                reg     [(8-1):0]        f_rd_pending    [0:(FIFOLN-1)];
666
                reg     [(8-1):0]        f_wr_pending,
667
                                        f_rd_count, f_wr_count;
668
 
669
                reg     r_last_rd_id_valid,
670
                        r_last_wr_id_valid;
671
 
672
                reg     [(C_AXI_ID_WIDTH-1):0]   r_last_wr_id, r_last_rd_id;
673
 
674
                initial r_last_wr_id_valid = 1'b0;
675
                initial r_last_rd_id_valid = 1'b0;
676
                always @(posedge i_clk)
677
                if (!i_axi_reset_n)
678
                begin
679
                        r_last_wr_id_valid <= 1'b0;
680
                        r_last_rd_id_valid <= 1'b0;
681
                        f_wr_count <= 0;
682
                        f_rd_count <= 0;
683
                end else begin
684
                        if (axi_awr_req)
685
                        begin
686
                                f_wr_pending <= i_axi_awlen+9'h1;
687
                                assume(f_wr_pending == 0);
688
                                r_last_wr_id_valid <= 1'b1;
689
                        end
690
 
691
                        if (axi_ard_req)
692
                                f_rd_pending[i_axi_arid] <= i_axi_arlen+9'h1;
693
 
694
 
695
                        if ((axi_wr_req)&&(i_axi_wlast))
696
                        begin
697
                                f_wr_count <= 0;
698
                                r_last_wr_id_valid <= 1'b0;
699
                                assume(
700
                                        // Either this is the last
701
                                        // of a series of requests we've
702
                                        // been waiting for,
703
                                        (f_wr_pending == f_wr_count - 9'h1)
704
                                        // *or* the only value
705
                                        // associated with an as yet
706
                                        // to be counted request
707
                                        ||((axi_awr_req)&&(i_axi_awlen == 0)));
708
                        end else if (axi_wr_req)
709
                                f_wr_count <= f_wr_count + 1'b1;
710
 
711
                        if (axi_rd_ack)
712
                        begin
713
                                if (i_axi_rlast)
714
                                        r_last_rd_id_valid <= 1'b0;
715
                                else
716
                                        r_last_rd_id_valid <= 1'b1;
717
 
718
                                r_last_rd_id <= i_axi_rid;
719
                                if ((axi_rd_ack)&&(r_last_rd_id_valid))
720
                                        assert(i_axi_rid == r_last_rd_id);
721
                        end
722
 
723
                        if ((axi_rd_ack)&&(i_axi_rlast))
724
                                assume(f_rd_count == f_rd_pending[i_axi_rid]-9'h1);
725
                        if ((axi_rd_ack)&&(i_axi_rlast))
726
                                f_rd_count <= 0;
727
                        else if (axi_rd_ack)
728
                                f_rd_count <= f_rd_count + 1'b1;
729
                end
730
        end else begin
731
                always @(*) begin
732
                        // Since we aren't allowing bursts, *every*
733
                        // write data and read data must always be the last
734
                        // value
735
                        assume((i_axi_wlast)||(!i_axi_wvalid));
736
                        assert((i_axi_rlast)||(!i_axi_rvalid));
737
 
738
                        assume((!i_axi_arvalid)||(i_axi_arlen==0));
739
                        assume((!i_axi_awvalid)||(i_axi_awlen==0));
740
                end
741
 
742
                always @(posedge i_clk)
743
                        if (i_axi_awvalid)
744
                                assume(i_axi_awlen == 0);
745
                always @(posedge i_clk)
746
                        if (i_axi_arvalid)
747
                                assume(i_axi_arlen == 0);
748
                always @(posedge i_clk)
749
                        if (i_axi_wvalid)
750
                                assume(i_axi_wlast);
751
                always @(posedge i_clk)
752
                        if (i_axi_rvalid)
753
                                assert(i_axi_rlast);
754
        end endgenerate
755
 
756
`endif
757
endmodule

powered by: WebSVN 2.1.0

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