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

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [wbxbar.v] - Blame information for rev 17

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

Line No. Rev Author Line
1 16 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    wbxbar.v
4
//
5
// Project:     Pipelined Wishbone to AXI converter
6
//
7
// Purpose:     A Configurable wishbone cross-bar interconnect
8
//
9
// Creator:     Dan Gisselquist, Ph.D.
10
//              Gisselquist Technology, LLC
11
//
12
////////////////////////////////////////////////////////////////////////////////
13
//
14
// Copyright (C) 2019, 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  wbxbar(i_clk, i_reset,
41
        i_mcyc, i_mstb, i_mwe, i_maddr, i_mdata, i_msel,
42
                o_mstall, o_mack, o_mdata, o_merr,
43
        o_scyc, o_sstb, o_swe, o_saddr, o_sdata, o_ssel,
44
                i_sstall, i_sack, i_sdata, i_serr);
45
        parameter       NM = 4, NS=8;
46
        parameter       AW = 20, DW=32;
47
        parameter       [NS*AW-1:0]      SADDR = {
48
                                3'b111, 17'h0,
49
                                3'b110, 17'h0,
50
                                3'b101, 17'h0,
51
                                3'b100, 17'h0,
52
                                3'b011, 17'h0,
53
                                3'b010, 17'h0,
54
                                4'b0010, 16'h0,
55
                                4'b0000, 16'h0 };
56
        parameter       [NS*AW-1:0]      SMASK = (NS <= 1) ? 0
57
                : { {(NS-2){ 3'b111, 17'h0 }}, {(2){ 4'b1111, 16'h0 }} };
58
        // parameter    [AW-1:0]        SADDR = 0;
59
        // parameter    [AW-1:0]        SMASK = 0;
60
        //
61
        // LGMAXBURST is the log_2 of the length of the longest burst that
62
        // might be seen.  It's used to set the size of the internal
63
        // counters that are used to make certain that the cross bar doesn't
64
        // switch while still waiting on a response.
65
        parameter       LGMAXBURST=6;
66
        //
67
        // OPT_TIMEOUT is used to help recover from a misbehaving slave.  If
68
        // set, this value will determine the number of clock cycles to wait
69
        // for a misbehaving slave before returning a bus error.  Alternatively,
70
        // if set to zero, this functionality will be removed.
71
        parameter       OPT_TIMEOUT = 0; // 1023;
72
        //
73
        // If OPT_TIMEOUT is set, then OPT_STARVATION_TIMEOUT may also be set.
74
        // The starvation timeout adds to the bus error timeout generation
75
        // the possibility that a master will wait OPT_TIMEOUT counts without
76
        // receiving the bus.  This may be the case, for example, if one
77
        // bus master is consuming a peripheral to such an extent that there's
78
        // no time/room for another bus master to use it.  In that case, when
79
        // the timeout runs out, the waiting bus master will be given a bus
80
        // error.
81
        parameter [0:0]   OPT_STARVATION_TIMEOUT = 1'b0 && (OPT_TIMEOUT > 0);
82
        //
83
        // TIMEOUT_WIDTH is the number of bits in counter used to check on a
84
        // timeout.
85
        localparam      TIMEOUT_WIDTH = $clog2(OPT_TIMEOUT);
86
        //
87
        // OPT_DBLBUFFER is used to register all of the outputs, and thus
88
        // avoid adding additional combinational latency through the core
89
        // that might require a slower clock speed.
90
        parameter [0:0]   OPT_DBLBUFFER = 1'b1;
91
        //
92
        // OPT_LOWPOWER adds logic to try to force unused values to zero,
93
        // rather than to allow a variety of logic optimizations that could
94
        // be used to reduce the logic count of the device.  Hence, OPT_LOWPOWER
95
        // will use more logic, but it won't drive bus wires unless there's a
96
        // value to drive onto them.
97
        parameter [0:0]   OPT_LOWPOWER = 1'b1;
98
        //
99
        // LGNM is the log (base two) of the number of bus masters connecting
100
        // to this crossbar
101
        localparam      LGNM = (NM>1) ? $clog2(NM) : 1;
102
        //
103
        // LGNM is the log (base two) of the number of slaves plus one come
104
        // out of the system.  The extra "plus one" is used for a pseudo slave
105
        // representing the case where the given address doesn't connect to
106
        // any of the slaves.  This address will generate a bus error.
107
        localparam      LGNS = $clog2(NS+1);
108
        //
109
        //
110
        input   wire                    i_clk, i_reset;
111
        //
112
        // Here are the bus inputs from each of the WB bus masters
113
        input   wire    [NM-1:0] i_mcyc, i_mstb, i_mwe;
114
        input   wire    [NM*AW-1:0]      i_maddr;
115
        input   wire    [NM*DW-1:0]      i_mdata;
116
        input   wire    [NM*DW/8-1:0]    i_msel;
117
        //
118
        // .... and their return data
119
        output  reg     [NM-1:0] o_mstall, o_mack, o_merr;
120
        output  reg     [NM*DW-1:0]      o_mdata;
121
        //
122
        //
123
        // Here are the output ports, used to control each of the various
124
        // slave ports that we are connected to
125
        output  reg     [NS-1:0] o_scyc, o_sstb, o_swe;
126
        output  reg     [NS*AW-1:0]      o_saddr;
127
        output  reg     [NS*DW-1:0]      o_sdata;
128
        output  reg     [NS*DW/8-1:0]    o_ssel;
129
        //
130
        // ... and their return data back to us.
131
        input   wire    [NS-1:0] i_sstall, i_sack, i_serr;
132
        input   wire    [NS*DW-1:0]      i_sdata;
133
        //
134
        //
135
 
136
        // At one time I used o_macc and o_sacc to put into the outgoing
137
        // trace file, just enough logic to tell me if a transaction was
138
        // taking place on the given clock.
139
        //
140
        // assign       o_macc = (i_mstb & ~o_mstall);
141
        // assign       o_sacc = (o_sstb & ~i_sstall);
142
        //
143
        // These definitions work with Verilator, just not with Yosys
144
        // reg  [NM-1:0][NS:0]          request;
145
        // reg  [NM-1:0][NS-1:0]        requested;
146
        // reg  [NM-1:0][NS:0]          grant;
147
        //
148
        // These definitions work with both
149
        reg     [NS:0]                   request         [0:NM-1];
150
        reg     [NS-1:0]         requested       [0:NM-1];
151
        reg     [NS:0]                   grant           [0:NM-1];
152
        reg     [NM-1:0]         mgrant;
153
        reg     [NS-1:0]         sgrant;
154
 
155
        wire    [LGMAXBURST-1:0] w_mpending [0:NM-1];
156
        reg     [NM-1:0]         mfull;
157
        reg     [NM-1:0]         mnearfull;
158
        reg     [NM-1:0]         mempty, timed_out;
159
 
160
        localparam      NMFULL = (NM > 1) ? (1<<LGNM) : 1;
161
        localparam      NSFULL = (1<<LGNS);
162
        reg     [NMFULL-1:0]     r_stb;
163
        reg     [NMFULL-1:0]     r_we;
164
        reg     [AW-1:0] r_addr          [0:NMFULL-1];
165
        reg     [DW-1:0] r_data          [0:NMFULL-1];
166
        reg     [DW/8-1:0]       r_sel           [0:NMFULL-1];
167
        wire    [TIMEOUT_WIDTH-1:0]      w_deadlock_timer [0:NM-1];
168
 
169
 
170
        reg     [LGNS-1:0]       mindex          [0:NMFULL-1];
171
        reg     [LGNM-1:0]       sindex          [0:NSFULL-1];
172
 
173
        reg     [NMFULL-1:0]     m_cyc;
174
        reg     [NMFULL-1:0]     m_stb;
175
        reg     [NMFULL-1:0]     m_we;
176
        reg     [AW-1:0] m_addr          [0:NMFULL-1];
177
        reg     [DW-1:0] m_data          [0:NMFULL-1];
178
        reg     [DW/8-1:0]       m_sel           [0:NMFULL-1];
179
        //
180
        reg     [NSFULL-1:0]     s_stall;
181
        reg     [DW-1:0] s_data          [0:NSFULL-1];
182
        reg     [NSFULL-1:0]     s_ack;
183
        reg     [NSFULL-1:0]     s_err;
184
 
185
        genvar  N, M;
186
        integer iN, iM;
187
        generate for(N=0; N<NM; N=N+1)
188
        begin : DECODE_REQUEST
189
                reg     none_sel;
190
 
191
                always @(*)
192
                begin
193
                        none_sel = !m_stb[N];
194
                        for(iM=0; iM<NS; iM=iM+1)
195
                        begin
196
 
197
                                none_sel = none_sel
198
                                        || (((m_addr[N] ^ SADDR[iM*AW +: AW])
199
                                                &SMASK[iM*AW +: AW])==0);
200
                        end
201
 
202
 
203
                        none_sel = !none_sel;
204
                end
205
 
206
                always @(*)
207
                begin
208
                        for(iM=0; iM<NS; iM=iM+1)
209
                                request[N][iM] = m_stb[N]
210
                                        &&(((m_addr[N] ^ SADDR[iM*AW +: AW])
211
                                                &SMASK[iM*AW +: AW])==0);
212
 
213
                        // Is this address non-existant?
214
                        request[N][NS] = m_stb[N] && none_sel;
215
                end
216
 
217
                always @(*)
218
                        m_cyc[N] = i_mcyc[N];
219
                always @(*)
220
                if (mfull[N])
221
                        m_stb[N] = 1'b0;
222
                else if (mnearfull[N])
223
                        m_stb[N] = i_mstb[N] && !r_stb[N];
224
                else
225
                        m_stb[N] = i_mstb[N] || (i_mcyc[N] && r_stb[N]);
226
                always @(*)
227
                        m_we[N]   = r_stb[N] ? r_we[N] : i_mwe[N];
228
                always @(*)
229
                        m_addr[N] = r_stb[N] ? r_addr[N] : i_maddr[N*AW +: AW];
230
                always @(*)
231
                        m_data[N] = r_stb[N] ? r_data[N] : i_mdata[N*DW +: DW];
232
                always @(*)
233
                        m_sel[N]  = r_stb[N] ? r_sel[N]: i_msel[N*DW/8 +: DW/8];
234
 
235
        end for(N=NM; N<NMFULL; N=N+1)
236
        begin
237
                // in case NM isn't one less than a power of two, complete
238
                // the set
239
                always @(*)
240
                        m_cyc[N] = 0;
241
                always @(*)
242
                        m_stb[N] = 0;
243
                always @(*)
244
                        m_we[N]   = 0;
245
                always @(*)
246
                        m_addr[N] = 0;
247
                always @(*)
248
                        m_data[N] = 0;
249
                always @(*)
250
                        m_sel[N]  = 0;
251
 
252
        end endgenerate
253
 
254
        always @(*)
255
        begin
256
                for(iM=0; iM<NS; iM=iM+1)
257
                begin
258
                        requested[0][iM] = 0;
259
                        for(iN=1; iN<NM; iN=iN+1)
260
                        requested[iN][iM]
261
                                = (request[iN-1][iM] || requested[iN-1][iM]);
262
                end
263
        end
264
 
265
        generate for(M=0; M<NS; M=M+1)
266
        begin
267
 
268
                always @(*)
269
                begin
270
                        sgrant[M] = 0;
271
                        for(iN=0; iN<NM; iN=iN+1)
272
                                if (grant[iN][M])
273
                                        sgrant[M] = 1;
274
                end
275
 
276
                always @(*)
277
                        s_data[M]  = i_sdata[M*DW +: DW];
278
                always @(*)
279
                        s_stall[M] = o_sstb[M] && i_sstall[M];
280
                always @(*)
281
                        s_ack[M]   = o_scyc[M] && i_sack[M];
282
                always @(*)
283
                        s_err[M]   = o_scyc[M] && i_serr[M];
284
        end for(M=NS; M<NSFULL; M=M+1)
285
        begin
286
 
287
                always @(*)
288
                        s_data[M]  = 0;
289
                always @(*)
290
                        s_stall[M] = 1;
291
                always @(*)
292
                        s_ack[M]   = 0;
293
                always @(*)
294
                        s_err[M]   = 1;
295
                // always @(*) sgrant[M]  = 0;
296
 
297
        end endgenerate
298
 
299
        //
300
        // Arbitrate among masters to determine who gets to access a given
301
        // channel
302
        generate for(N=0; N<NM; N=N+1)
303
        begin : ARBITRATE_REQUESTS
304
 
305
                // This is done using a couple of variables.
306
                //
307
                // request[N][M]
308
                //      This is true if master N is requesting to access slave
309
                //      M.  It is combinatorial, so it will be true if the
310
                //      request is being made on the current clock.
311
                //
312
                // requested[N][M]
313
                //      True if some other master, prior to N, has requested
314
                //      channel M.  This creates a basic priority arbiter,
315
                //      such that lower numbered masters have access before
316
                //      a greater numbered master
317
                //
318
                // grant[N][M]
319
                //      True if a grant has been made for master N to access
320
                //      slave channel M
321
                //
322
                // mgrant[N]
323
                //      True if master N has been granted access to some slave
324
                //      channel, any channel.
325
                //
326
                // mindex[N]
327
                //      This is the number of the slave channel that master
328
                //      N has been given access to
329
                //
330
                // sgrant[M]
331
                //      True if there exists some master, N, that has been
332
                //      granted access to this slave, hence grant[N][M] must
333
                //      also be true
334
                //
335
                // sindex[M]
336
                //      This is the index of the master that has access to
337
                //      slave M, assuming sgrant[M].  Hence, if sgrant[M]
338
                //      then grant[sindex[M]][M] must be true
339
                //
340
                reg     stay_on_channel;
341
 
342
                always @(*)
343
                begin
344
                        stay_on_channel = 0;
345
                        for(iM=0; iM<NS; iM=iM+1)
346
                        begin
347
                                if (request[N][iM] && grant[N][iM])
348
                                        stay_on_channel = 1;
349
                        end
350
                end
351
 
352
                reg     requested_channel_is_available;
353
 
354
                always @(*)
355
                begin
356
                        requested_channel_is_available = 0;
357
                        for(iM=0; iM<NS; iM=iM+1)
358
                        begin
359
                                if (request[N][iM] && !sgrant[iM]
360
                                                && !requested[N][iM])
361
                                        requested_channel_is_available = 1;
362
                        end
363
                end
364
 
365
                initial grant[N] = 0;
366
                initial mgrant[N] = 0;
367
                always @(posedge i_clk)
368
                if (i_reset || !i_mcyc[N])
369
                begin
370
                        grant[N] <= 0;
371
                        mgrant[N] <= 0;
372
                end else if (!mgrant[N] || mempty[N])
373
                begin
374
                        if (stay_on_channel)
375
                                mgrant[N] <= 1'b1;
376
                        else if (requested_channel_is_available)
377
                                mgrant[N] <= 1'b1;
378
                        else if (i_mstb[N] || r_stb[N])
379
                                mgrant[N] <= 1'b0;
380
 
381
                        for(iM=0; iM<NS; iM=iM+1)
382
                        begin
383
 
384
                                if (request[N][iM] && grant[N][iM])
385
                                        // Maintain any open channels
386
                                        grant[N][iM] <= 1;
387
                                else if (request[N][iM] && !sgrant[iM]
388
                                                && !requested[N][iM])
389
                                        // Open a new channel if necessary
390
                                        grant[N][iM] <= 1;
391
                                else if (i_mstb[N] || r_stb[N])
392
                                        grant[N][iM] <= 0;
393
 
394
                        end
395
                        if (request[N][NS])
396
                        begin
397
                                grant[N][NS] <= 1'b1;
398
                                mgrant[N] <= 1'b1;
399
                        end else begin
400
                                grant[N][NS] <= 1'b0;
401
                                if (grant[N][NS])
402
                                        mgrant[N] <= 1'b1;
403
                        end
404
                end
405
 
406
                if (NS == 1)
407
                begin
408
 
409
                        always @(*)
410
                                mindex[N] = 0;
411
 
412
                end else begin
413
 
414
                        always @(posedge i_clk)
415
                        if (!mgrant[N] || mempty[N])
416
                        begin
417
 
418
                                for(iM=0; iM<NS; iM=iM+1)
419
                                begin
420
                                        if (request[N][iM] && grant[N][iM])
421
                                        begin
422
                                                // Maintain any open channels
423
                                                mindex[N] <= iM;
424
                                        end else if (request[N][iM]
425
                                                        && !sgrant[iM]
426
                                                        && !requested[N][iM])
427
                                        begin
428
                                                // Open a new channel
429
                                                // if necessary
430
                                                mindex[N] <= iM;
431
                                        end
432
                                end
433
                        end
434
                end
435
 
436
        end for (N=NM; N<NMFULL; N=N+1)
437
        begin
438
 
439
                always @(*)
440
                        mindex[N] = 0;
441
 
442
        end endgenerate
443
 
444
        // Calculate sindex.  sindex[M] (indexed by slave ID)
445
        // references the master controlling this slave.  This makes for
446
        // faster/cheaper logic on the return path, since we can now use
447
        // a fully populated LUT rather than a priority based return scheme
448
        generate for(M=0; M<NS; M=M+1)
449
        begin
450
 
451
                if (NM <= 1)
452
                begin
453
 
454
                        // If there will only ever be one master, then we
455
                        // can assume all slave indexes point to that master
456
                        always @(*)
457
                                sindex[M] = 0;
458
 
459
                end else begin : SINDEX_MORE_THAN_ONE_MASTER
460
 
461
                        always @(posedge i_clk)
462
                        for (iN=0; iN<NM; iN=iN+1)
463
                        begin
464
                                if (!mgrant[iN] || mempty[iN])
465
                                begin
466
                                        if (request[iN][M] && grant[iN][M])
467
                                                sindex[M] <= iN;
468
                                        else if (request[iN][M] && !sgrant[M]
469
                                                        && !requested[iN][M])
470
                                                sindex[M] <= iN;
471
                                end
472
                        end
473
                end
474
 
475
        end for(M=NS; M<NSFULL; M=M+1)
476
        begin
477
                // Assign the unused slave indexes to zero
478
                //
479
                // Remember, to full out a full 2^something set of slaves,
480
                // we may have more slave indexes than we actually have slaves
481
 
482
                always @(*)
483
                        sindex[M] = 0;
484
 
485
        end endgenerate
486
 
487
 
488
        //
489
        // Assign outputs to the slaves, part one
490
        //
491
        // In this part, we assign the difficult outputs: o_scyc and o_sstb
492
        generate for(M=0; M<NS; M=M+1)
493
        begin
494
 
495
                initial o_scyc[M] = 0;
496
                initial o_sstb[M] = 0;
497
                always @(posedge i_clk)
498
                begin
499
                        if (sgrant[M])
500
                        begin
501
 
502
                                if (!i_mcyc[sindex[M]])
503
                                begin
504
                                        o_scyc[M] <= 1'b0;
505
                                        o_sstb[M] <= 1'b0;
506
                                end else begin
507
                                        o_scyc[M] <= 1'b1;
508
 
509
                                        if (!s_stall[M])
510
                                                o_sstb[M] <= m_stb[sindex[M]]
511
                                                  && request[sindex[M]][M]
512
                                                  && !mnearfull[sindex[M]];
513
                                end
514
                        end else begin
515
                                o_scyc[M]  <= 1'b0;
516
                                o_sstb[M]  <= 1'b0;
517
                        end
518
 
519
                        if (i_reset || s_err[M])
520
                        begin
521
                                o_scyc[M] <= 1'b0;
522
                                o_sstb[M] <= 1'b0;
523
                        end
524
                end
525
        end endgenerate
526
 
527
        //
528
        // Assign outputs to the slaves, part two
529
        //
530
        // These are the easy(er) outputs, since there are fewer properties
531
        // riding on them
532
        generate if ((NM == 1) && (!OPT_LOWPOWER))
533
        begin
534
                //
535
                // This is the low logic version of our bus data outputs.
536
                // It only works if we only have one master.
537
                //
538
                // The basic idea here is that we share all of our bus outputs
539
                // between all of the various slaves.  Since we only have one
540
                // bus master, this works.
541
                //
542
                always @(posedge i_clk)
543
                begin
544
                        o_swe[0]        <= o_swe[0];
545
                        o_saddr[0+: AW] <= o_saddr[0+:AW];
546
                        o_sdata[0+: DW] <= o_sdata[0+:DW];
547
                        o_ssel[0+:DW/8] <=o_ssel[0+:DW/8];
548
 
549
                        if (sgrant[mindex[0]] && !s_stall[mindex[0]])
550
                        begin
551
                                o_swe[0]        <= m_we[0];
552
                                o_saddr[0+: AW] <= m_addr[0];
553
                                o_sdata[0+: DW] <= m_data[0];
554
                                o_ssel[0+:DW/8] <= m_sel[0];
555
                        end
556
                end
557
 
558
                for(M=1; M<NS; M=M+1)
559
                always @(*)
560
                begin
561
                        o_swe[M]            = o_swe[0];
562
                        o_saddr[M*AW +: AW] = o_saddr[0 +: AW];
563
                        o_sdata[M*DW +: DW] = o_sdata[0 +: DW];
564
                        o_ssel[M*DW/8+:DW/8]= o_ssel[0 +: DW/8];
565
                end
566
 
567
        end else for(M=0; M<NS; M=M+1)
568
        begin
569
                always @(posedge i_clk)
570
                begin
571
                        if (OPT_LOWPOWER && !sgrant[M])
572
                        begin
573
                                o_swe[M]              <= 1'b0;
574
                                o_saddr[M*AW   +: AW] <= 0;
575
                                o_sdata[M*DW   +: DW] <= 0;
576
                                o_ssel[M*(DW/8)+:DW/8]<= 0;
577
                        end else if (!s_stall[M]) begin
578
                                o_swe[M]              <= m_we[sindex[M]];
579
                                o_saddr[M*AW   +: AW] <= m_addr[sindex[M]];
580
                                if (OPT_LOWPOWER && !m_we[sindex[M]])
581
                                        o_sdata[M*DW   +: DW] <= 0;
582
                                else
583
                                        o_sdata[M*DW   +: DW] <= m_data[sindex[M]];
584
                                o_ssel[M*(DW/8)+:DW/8]<= m_sel[sindex[M]];
585
                        end
586
 
587
                end
588
        end endgenerate
589
 
590
        //
591
        // Assign return values to the masters
592
        generate if (OPT_DBLBUFFER)
593
        begin : DOUBLE_BUFFERRED_STALL
594
 
595
                for(N=0; N<NM; N=N+1)
596
                begin
597
                        initial o_mstall[N] = 0;
598
                        initial o_mack[N]   = 0;
599
                        initial o_merr[N]   = 0;
600
                        always @(posedge i_clk)
601
                        begin
602
                                iM = mindex[N];
603
                                o_mstall[N] <= o_mstall[N]
604
                                                || (i_mstb[N] && !o_mstall[N]);
605
                                o_mack[N]   <= mgrant[N] && s_ack[mindex[N]];
606
                                o_merr[N]   <= mgrant[N] && s_err[mindex[N]];
607
                                if (OPT_LOWPOWER && !mgrant[N])
608
                                        o_mdata[N*DW +: DW] <= 0;
609
                                else
610
                                        o_mdata[N*DW +: DW] <= s_data[mindex[N]];
611
 
612
                                if (mgrant[N])
613
                                begin
614
                                        if ((i_mstb[N]||o_mstall[N])
615
                                                                && mnearfull[N])
616
                                                o_mstall[N] <= 1'b1;
617
                                        else if ((i_mstb[N] || o_mstall[N])
618
                                                        && !request[N][iM])
619
                                                // Requesting another channel
620
                                                o_mstall[N] <= 1'b1;
621
                                        else if (!s_stall[iM])
622
                                                // Downstream channel is clear
623
                                                o_mstall[N] <= 1'b0;
624
                                        else // if (o_sstb[mindex[N]]
625
                                                //   && i_sstall[mindex[N]])
626
                                                // Downstream channel is stalled
627
                                                o_mstall[N] <= i_mstb[N];
628
                                end
629
 
630
                                if (mnearfull[N] && i_mstb[N])
631
                                        o_mstall[N] <= 1'b1;
632
 
633
                                if ((o_mstall[N] && grant[N][NS])
634
                                        ||(timed_out[N] && !o_mack[N]))
635
                                begin
636
                                        o_mstall[N] <= 1'b0;
637
                                        o_mack[N]   <= 1'b0;
638
                                        o_merr[N]   <= 1'b1;
639
                                end
640
 
641
                                if (i_reset || !i_mcyc[N])
642
                                begin
643
                                        o_mstall[N] <= 1'b0;
644
                                        o_mack[N]   <= 1'b0;
645
                                        o_merr[N]   <= 1'b0;
646
                                end
647
                        end
648
 
649
                        always @(*)
650
                                r_stb[N] = o_mstall[N];
651
 
652
                        always @(posedge i_clk)
653
                        if (OPT_LOWPOWER && !i_mcyc[N])
654
                        begin
655
                                r_we[N]   <= 0;
656
                                r_addr[N] <= 0;
657
                                r_data[N] <= 0;
658
                                r_sel[N]  <= 0;
659
                        end else if ((!OPT_LOWPOWER || i_mstb[N]) && !o_mstall[N])
660
                        begin
661
                                r_we[N]   <= i_mwe[N];
662
                                r_addr[N] <= i_maddr[N*AW +: AW];
663
                                r_data[N] <= i_mdata[N*DW +: DW];
664
                                r_sel[N]  <= i_msel[N*(DW/8) +: DW/8];
665
                        end
666
                end
667
 
668
                for(N=NM; N<NMFULL; N=N+1)
669
                begin
670
 
671
                        always @(*)
672
                                r_stb[N] <= 1'b0;
673
 
674
                        always @(*)
675
                        begin
676
                                r_we[N]   = 0;
677
                                r_addr[N] = 0;
678
                                r_data[N] = 0;
679
                                r_sel[N]  = 0;
680
                        end
681
                end
682
 
683
 
684
        end else if (NS == 1) // && !OPT_DBLBUFFER
685
        begin : SINGLE_SLAVE
686
 
687
                for(N=0; N<NM; N=N+1)
688
                begin
689
                        always @(*)
690
                        begin
691
                                o_mstall[N] = !mgrant[N] || s_stall[0]
692
                                        || (i_mstb[N] && !request[N][0]);
693
                                o_mack[N]   =  mgrant[N] && i_sack[0];
694
                                o_merr[N]   =  mgrant[N] && i_serr[0];
695
                                o_mdata[N*DW +: DW]  = (!mgrant[N] && OPT_LOWPOWER)
696
                                        ? 0 : i_sdata;
697
 
698
                                if (mnearfull[N])
699
                                        o_mstall[N] = 1'b1;
700
 
701
                                if (timed_out[N]&&!o_mack[0])
702
                                begin
703
                                        o_mstall[N] = 1'b0;
704
                                        o_mack[N]   = 1'b0;
705
                                        o_merr[N]   = 1'b1;
706
                                end
707
 
708
                                if (grant[N][NS] && m_stb[N])
709
                                begin
710
                                        o_mstall[N] = 1'b0;
711
                                        o_mack[N]   = 1'b0;
712
                                        o_merr[N]   = 1'b1;
713
                                end
714
 
715
                                if (!m_cyc[N])
716
                                begin
717
                                        o_mack[N] = 1'b0;
718
                                        o_merr[N] = 1'b0;
719
                                end
720
                        end
721
                end
722
 
723
                for(N=0; N<NMFULL; N=N+1)
724
                begin
725
 
726
                        always @(*)
727
                                r_stb[N] <= 1'b0;
728
 
729
                        always @(*)
730
                        begin
731
                                r_we[N]   = 0;
732
                                r_addr[N] = 0;
733
                                r_data[N] = 0;
734
                                r_sel[N]  = 0;
735
                        end
736
                end
737
 
738
        end else begin : SINGLE_BUFFER_STALL
739
                for(N=0; N<NM; N=N+1)
740
                begin
741
                        // initial      o_mstall[N] = 0;
742
                        // initial      o_mack[N]   = 0;
743
                        always @(*)
744
                        begin
745
                                o_mstall[N] = 1;
746
                                o_mack[N]   = mgrant[N] && s_ack[mindex[N]];
747
                                o_merr[N]   = mgrant[N] && s_err[mindex[N]];
748
                                if (OPT_LOWPOWER && !mgrant[N])
749
                                        o_mdata[N*DW +: DW] = 0;
750
                                else
751
                                        o_mdata[N*DW +: DW] = s_data[mindex[N]];
752
 
753
                                if (mgrant[N])
754
                                begin
755
                                        iM = mindex[N];
756
                                        o_mstall[N]       = (s_stall[mindex[N]])
757
                                            || (i_mstb[N] && !request[N][iM]);
758
                                end
759
 
760
                                if (mnearfull[N])
761
                                        o_mstall[N] = 1'b1;
762
 
763
                                if (grant[N][NS] ||(timed_out[N]&&!o_mack[0]))
764
                                begin
765
                                        o_mstall[N] = 1'b0;
766
                                        o_mack[N]   = 1'b0;
767
                                        o_merr[N]   = 1'b1;
768
                                end
769
 
770
                                if (!m_cyc[N])
771
                                begin
772
                                        o_mack[N] = 1'b0;
773
                                        o_merr[N] = 1'b0;
774
                                end
775
                        end
776
                end
777
 
778
                for(N=0; N<NMFULL; N=N+1)
779
                begin
780
 
781
                        always @(*)
782
                                r_stb[N] <= 1'b0;
783
 
784
                        always @(*)
785
                        begin
786
                                r_we[N]   = 0;
787
                                r_addr[N] = 0;
788
                                r_data[N] = 0;
789
                                r_sel[N]  = 0;
790
                        end
791
                end
792
 
793
        end endgenerate
794
 
795
        //
796
        // Count the pending transactions per master
797
        generate for(N=0; N<NM; N=N+1)
798
        begin
799
                reg     [LGMAXBURST-1:0] lclpending;
800
                initial lclpending  = 0;
801
                initial mempty[N]    = 1;
802
                initial mnearfull[N] = 0;
803
                initial mfull[N]     = 0;
804
                always @(posedge i_clk)
805
                if (i_reset || !i_mcyc[N] || o_merr[N])
806
                begin
807
                        lclpending <= 0;
808
                        mfull[N]    <= 0;
809
                        mempty[N]   <= 1'b1;
810
                        mnearfull[N]<= 0;
811
                end else case({ (i_mstb[N] && !o_mstall[N]), o_mack[N] })
812
                2'b01: begin
813
                        lclpending <= lclpending - 1'b1;
814
                        mnearfull[N]<= mfull[N];
815
                        mfull[N]    <= 1'b0;
816
                        mempty[N]   <= (lclpending == 1);
817
                        end
818
                2'b10: begin
819
                        lclpending <= lclpending + 1'b1;
820
                        mnearfull[N]<= (&lclpending[LGMAXBURST-1:2])&&(lclpending[1:0] != 0);
821
                        mfull[N]    <= mnearfull[N];
822
                        mempty[N]   <= 1'b0;
823
                        end
824
                default: begin end
825
                endcase
826
 
827
                assign w_mpending[N] = lclpending;
828
 
829
        end endgenerate
830
 
831
 
832
        generate if (OPT_TIMEOUT > 0)
833
        begin : CHECK_TIMEOUT
834
 
835
                for(N=0; N<NM; N=N+1)
836
                begin
837
 
838
                        reg     [TIMEOUT_WIDTH-1:0]      deadlock_timer;
839
 
840
                        initial deadlock_timer = OPT_TIMEOUT;
841
                        initial timed_out[N] = 1'b0;
842
                        always @(posedge i_clk)
843
                        if (i_reset || !i_mcyc[N]
844
                                        ||((w_mpending[N] == 0)
845
                                                &&(!i_mstb[N] && !r_stb[N]))
846
                                        ||((i_mstb[N] || r_stb[N])
847
                                                &&(!o_mstall[N]))
848
                                        ||(o_mack[N] || o_merr[N])
849
                                        ||(!OPT_STARVATION_TIMEOUT&&!mgrant[N]))
850
                        begin
851
                                deadlock_timer <= OPT_TIMEOUT;
852
                                timed_out[N] <= 0;
853
                        end else if (deadlock_timer > 0)
854
                        begin
855
                                deadlock_timer <= deadlock_timer - 1;
856
                                timed_out[N] <= (deadlock_timer <= 1);
857
                        end
858
 
859
                        assign  w_deadlock_timer[N] = deadlock_timer;
860
                end
861
 
862
        end else begin
863
 
864
                always @(*)
865
                        timed_out = 0;
866
 
867
        end endgenerate
868
 
869
`ifdef  FORMAL
870
        localparam      F_MAX_DELAY = 4;
871
        localparam      F_LGDEPTH = LGMAXBURST;
872
        //
873
        reg                     f_past_valid;
874
        //
875
        // Our bus checker keeps track of the number of requests,
876
        // acknowledgments, and the number of outstanding transactions on
877
        // every channel, both the masters driving us
878
        wire    [F_LGDEPTH-1:0]  f_mreqs         [0:NM-1];
879
        wire    [F_LGDEPTH-1:0]  f_macks         [0:NM-1];
880
        wire    [F_LGDEPTH-1:0]  f_moutstanding  [0:NM-1];
881
        //
882
        // as well as the slaves that we drive ourselves
883
        wire    [F_LGDEPTH-1:0]  f_sreqs         [0:NS-1];
884
        wire    [F_LGDEPTH-1:0]  f_sacks         [0:NS-1];
885
        wire    [F_LGDEPTH-1:0]  f_soutstanding  [0:NS-1];
886
 
887
 
888
        initial assert(!OPT_STARVATION_TIMEOUT || OPT_TIMEOUT > 0);
889
 
890
        reg     f_past_valid;
891
        initial f_past_valid = 0;
892
        always @(posedge i_clk)
893
                f_past_valid = 1'b1;
894
 
895
        always @(*)
896
        if (!f_past_valid)
897
                assume(i_reset);
898
 
899
        generate for(N=0; N<NM; N=N+1)
900
        begin
901
                always @(*)
902
                if (f_past_valid)
903
                for(iN=N+1; iN<NM; iN=iN+1)
904
                        // Can't grant the same channel to two separate
905
                        // masters.  This applies to all but the error or
906
                        // no-slave-selected channel
907
                        assert((grant[N][NS-1:0] & grant[iN][NS-1:0])==0);
908
 
909
                for(M=1; M<=NS; M=M+1)
910
                begin
911
                        // Can't grant two channels to the same master
912
                        always @(*)
913
                        if (f_past_valid && grant[N][M])
914
                                assert(grant[N][M-1:0] == 0);
915
                end
916
 
917
 
918
                always @(*)
919
                if (&w_mpending[N])
920
                        assert(o_merr[N] || o_mstall[N]);
921
 
922
                reg     checkgrant;
923
                always @(*)
924
                if (f_past_valid)
925
                begin
926
                        checkgrant = 0;
927
                        for(iM=0; iM<NS; iM=iM+1)
928
                                if (grant[N][iM])
929
                                        checkgrant = 1;
930
                        if (grant[N][NS])
931
                                checkgrant = 1;
932
 
933
                        assert(checkgrant == mgrant[N]);
934
                end
935
 
936
        end endgenerate
937
 
938
        // Double check the grant mechanism and its dependent variables
939
        generate for(N=0; N<NM; N=N+1)
940
        begin
941
 
942
                for(M=0; M<NS; M=M+1)
943
                begin
944
                        always @(*)
945
                        if ((f_past_valid)&&grant[N][M])
946
                        begin
947
                                assert(mgrant[N]);
948
                                assert(mindex[N] == M);
949
                                assert(sindex[M] == N);
950
                        end
951
                end
952
        end endgenerate
953
 
954
        // Double check the timeout flags for consistency
955
        generate for(N=0; N<NM; N=N+1)
956
        begin
957
                always @(*)
958
                if (f_past_valid)
959
                begin
960
                        assert(mempty[N] == (w_mpending[N] == 0));
961
                        assert(mnearfull[N]==(&w_mpending[N][LGMAXBURST-1:1]));
962
                        assert(mfull[N] == (&w_mpending[N]));
963
                end
964
        end endgenerate
965
 
966
`ifdef  VERIFIC
967
        //
968
        // The Verific parser is currently broken, and doesn't allow
969
        // initial assumes or asserts.  The following lines get us around that
970
        //
971
        always @(*)
972
        if (!f_past_valid)
973
                assume(sgrant == 0);
974
 
975
        generate for(M=0; M<NS; M=M+1)
976
        begin
977
                always @(*)
978
                if (!f_past_valid)
979
                begin
980
                        assume(o_scyc[M] == 0);
981
                        assume(o_sstb[M] == 0);
982
                end
983
        end endgenerate
984
 
985
        generate for(N=0; N<NM; N=N+1)
986
        begin
987
                always @(*)
988
                if (!f_past_valid)
989
                begin
990
                        assume(grant[N] == 0);
991
                        assume(mgrant[N] == 0);
992
                end
993
        end
994
`endif
995
 
996
        ////////////////////////////////////////////////////////////////////////
997
        //
998
        //      BUS CHECK
999
        //
1000
        // Verify that every channel, whether master or slave, follows the rules
1001
        // of the WB road.
1002
        //
1003
        ////////////////////////////////////////////////////////////////////////
1004
        generate for(N=0; N<NM; N=N+1)
1005
        begin : WB_SLAVE_CHECK
1006
 
1007
                fwb_slave #(
1008
                        .AW(AW), .DW(DW),
1009
                        .F_LGDEPTH(LGMAXBURST),
1010
                        .F_MAX_ACK_DELAY(0),
1011
                        .F_MAX_STALL(0)
1012
                        ) slvi(i_clk, i_reset,
1013
                                i_mcyc[N], i_mstb[N], i_mwe[N],
1014
                                i_maddr[N*AW +: AW], i_mdata[N*DW +: DW],                                       i_msel[N*(DW/8) +: (DW/8)],
1015
                        o_mack[N], o_mstall[N], o_mdata[N*DW +: DW], o_merr[N],
1016
                        f_mreqs[N], f_macks[N], f_moutstanding[N]);
1017
 
1018
                always @(*)
1019
                if ((f_past_valid)&&(grant[N][NS]))
1020
                        assert(f_moutstanding[N] <= 1);
1021
 
1022
                always @(*)
1023
                if ((f_past_valid)&&(grant[N][NS] && i_mcyc[N]))
1024
                        assert(o_mstall[N] || o_merr[N]);
1025
 
1026
        end endgenerate
1027
 
1028
        generate for(M=0; M<NS; M=M+1)
1029
        begin : WB_MASTER_CHECK
1030
                fwb_master #(
1031
                        .AW(AW), .DW(DW),
1032
                        .F_LGDEPTH(LGMAXBURST),
1033
                        .F_MAX_ACK_DELAY(F_MAX_DELAY),
1034
                        .F_MAX_STALL(2)
1035
                        ) mstri(i_clk, i_reset,
1036
                                o_scyc[M], o_sstb[M], o_swe[M],
1037
                                o_saddr[M*AW +: AW], o_sdata[M*DW +: DW],
1038
                                o_ssel[M*(DW/8) +: (DW/8)],
1039
                        i_sack[M], i_sstall[M], s_data[M], i_serr[M],
1040
                        f_sreqs[M], f_sacks[M], f_soutstanding[M]);
1041
        end endgenerate
1042
 
1043
        ////////////////////////////////////////////////////////////////////////
1044
        //
1045
        ////////////////////////////////////////////////////////////////////////
1046
        generate for(N=0; N<NM; N=N+1)
1047
        begin : CHECK_OUTSTANDING
1048
 
1049
                always @(posedge i_clk)
1050
                if (i_mcyc[N])
1051
                        assert(f_moutstanding[N] == w_mpending[N]);
1052
 
1053
                reg     [LGMAXBURST:0]   n_outstanding;
1054
                always @(*)
1055
                if (i_mcyc[N])
1056
                        assert(f_moutstanding[N] >=
1057
                                (o_mstall[N] && OPT_DBLBUFFER) ? 1:0
1058
                                + (o_mack[N] && OPT_DBLBUFFER) ? 1:0);
1059
 
1060
                always @(*)
1061
                        n_outstanding = f_moutstanding[N]
1062
                                - ((o_mstall[N] && OPT_DBLBUFFER) ? 1:0)
1063
                                - ((o_mack[N] && OPT_DBLBUFFER) ? 1:0);
1064
                always @(posedge i_clk)
1065
                if (i_mcyc[N] && !mgrant[N] && !o_merr[N])
1066
                        assert(f_moutstanding[N]
1067
                                        == (o_mstall[N]&&OPT_DBLBUFFER ? 1:0));
1068
                else if (i_mcyc[N] && mgrant[N])
1069
                for(iM=0; iM<NS; iM=iM+1)
1070
                if (grant[N][iM] && o_scyc[iM] && !i_serr[iM] && !o_merr[N])
1071
                        assert(n_outstanding
1072
                                == {1'b0,f_soutstanding[iM]}+(o_sstb[iM] ? 1:0));
1073
 
1074
                always @(*)
1075
                if (i_mcyc[N] && r_stb[N] && OPT_DBLBUFFER)
1076
                        assume(i_mwe[N] == r_we[N]);
1077
 
1078
                always @(*)
1079
                if (!OPT_DBLBUFFER && !mnearfull[N])
1080
                        assert(i_mstb[N] == m_stb[N]);
1081
 
1082
                always @(*)
1083
                if (!OPT_DBLBUFFER)
1084
                        assert(i_mwe[N] == m_we[N]);
1085
 
1086
                always @(*)
1087
                for(iM=0; iM<NS; iM=iM+1)
1088
                if (grant[N][iM] && i_mcyc[N])
1089
                begin
1090
                        if (f_soutstanding[iM] > 0)
1091
                                assert(i_mwe[N] == o_swe[iM]);
1092
                        if (o_sstb[iM])
1093
                                assert(i_mwe[N] == o_swe[iM]);
1094
                        if (o_mack[N])
1095
                                assert(i_mwe[N] == o_swe[iM]);
1096
                        if (o_scyc[iM] && i_sack[iM])
1097
                                assert(i_mwe[N] == o_swe[iM]);
1098
                        if (o_merr[N] && !timed_out[N])
1099
                                assert(i_mwe[N] == o_swe[iM]);
1100
                        if (o_scyc[iM] && i_serr[iM])
1101
                                assert(i_mwe[N] == o_swe[iM]);
1102
                end
1103
 
1104
        end endgenerate
1105
 
1106
        generate for(M=0; M<NS; M=M+1)
1107
        begin
1108
                always @(posedge i_clk)
1109
                if (!$past(sgrant[M]))
1110
                        assert(!o_scyc[M]);
1111
        end endgenerate
1112
 
1113
        ////////////////////////////////////////////////////////////////////////
1114
        //
1115
        //      CONTRACT SECTION
1116
        //
1117
        // Here's the contract, in two parts:
1118
        //
1119
        //      1. Should ever a master (any master) wish to read from a slave
1120
        //              (any slave), he should be able to read a known value
1121
        //              from that slave (any value) from any arbitrary address
1122
        //              he might wish to read from (any address)
1123
        //
1124
        //      2. Should ever a master (any master) wish to write to a slave
1125
        //              (any slave), he should be able to write the exact
1126
        //              value he wants (any value) to the exact address he wants
1127
        //              (any address)
1128
        //
1129
        //      special_master  is an arbitrary constant chosen by the solver,
1130
        //              which can reference *any* possible master
1131
        //      special_address is an arbitrary constant chosen by the solver,
1132
        //              which can reference *any* possible address the master
1133
        //              might wish to access
1134
        //      special_value   is an arbitrary value (at least during
1135
        //              induction) representing the current value within the
1136
        //              slave at the given address
1137
        //
1138
        //
1139
        ////////////////////////////////////////////////////////////////////////
1140
        //
1141
        // Now let's pay attention to a special bus master and a special
1142
        // address referencing a special bus slave.  We'd like to assert
1143
        // that we can access the values of every slave from every master.
1144
        (* anyconst *) reg      [(NM<=1)?0:(LGNM-1):0]    special_master;
1145
                        reg     [(NS<=1)?0:(LGNS-1):0]    special_slave;
1146
        (* anyconst *) reg      [AW-1:0] special_address;
1147
                        reg     [DW-1:0] special_value;
1148
 
1149
        always @(*)
1150
        if (NM <= 1)
1151
                assume(special_master == 0);
1152
        always @(*)
1153
        if (NS <= 1)
1154
                assume(special_slave == 0);
1155
 
1156
        //
1157
        // Decode the special address to discover the slave associated with it
1158
        always @(*)
1159
        begin
1160
                special_slave = NS;
1161
                for(iM=0; iM<NS; iM = iM+1)
1162
                begin
1163
                        if (((special_address ^ SADDR[iM*AW +: AW])
1164
                                        &SMASK[iM*AW +: AW]) == 0)
1165
                                special_slave = iM;
1166
                end
1167
        end
1168
 
1169
        generate if (NS > 1)
1170
        begin : DOUBLE_ADDRESS_CHECK
1171
                //
1172
                // Check that no slave address has been assigned twice.
1173
                // This check only needs to be done once at the beginning
1174
                // of the run, during the BMC section.
1175
                reg     address_found;
1176
 
1177
                always @(*)
1178
                if (!f_past_valid)
1179
                begin
1180
                        address_found = 0;
1181
                        for(iM=0; iM<NS; iM = iM+1)
1182
                        begin
1183
                                if (((special_address ^ SADDR[iM*AW +: AW])
1184
                                                &SMASK[iM*AW +: AW]) == 0)
1185
                                begin
1186
                                        assert(address_found == 0);
1187
                                        address_found = 1;
1188
                                end
1189
                        end
1190
                end
1191
 
1192
        end endgenerate
1193
        //
1194
        // Let's assume this slave will acknowledge any request on the next
1195
        // bus cycle after the stall goes low.  Further, lets assume that
1196
        // it never creates an error, and that it always responds to our special
1197
        // address with the special data value given above.  To do this, we'll
1198
        // also need to make certain that the special value will change
1199
        // following any write.
1200
        //
1201
        // These are the "assumptions" associated with our fictitious slave.
1202
        initial assume(special_value == 0);
1203
        always @(posedge i_clk)
1204
        if (special_slave < NS)
1205
        begin
1206
                if ($past(o_sstb[special_slave] && !i_sstall[special_slave]))
1207
                begin
1208
                        assume(i_sack[special_slave]);
1209
 
1210
                        if ($past(!o_swe[special_slave])
1211
                                        &&($past(o_saddr[special_slave*AW +: AW]) == special_address))
1212
                                assume(i_sdata[special_slave*DW+: DW]
1213
                                                == special_value);
1214
                end else
1215
                        assume(!i_sack[special_slave]);
1216
                assume(!i_serr[special_slave]);
1217
 
1218
                if (o_scyc[special_slave])
1219
                        assert(f_soutstanding[special_slave]
1220
                                == i_sack[special_slave]);
1221
 
1222
                if (o_sstb[special_slave] && !i_sstall[special_slave]
1223
                        && o_swe[special_slave])
1224
                begin
1225
                        for(iM=0; iM < DW/8; iM=iM+1)
1226
                        if (o_ssel[special_slave * DW/8 + iM])
1227
                                special_value[iM*8 +: 8] <= o_sdata[special_slave * DW + iM*8 +: 8];
1228
                end
1229
        end
1230
 
1231
        //
1232
        // Now its time to make some assertions.  Specifically, we want to
1233
        // assert that any time we read from this special slave, the special
1234
        // value is returned.
1235
        reg     [2:0]    read_seq;
1236
        initial read_seq = 0;
1237
        always @(posedge i_clk)
1238
        if ((special_master < NM)&&(special_slave < NS)
1239
                        &&(i_mcyc[special_master])
1240
                        &&(!timed_out[special_master]))
1241
        begin
1242
                read_seq <= 0;
1243
                if ((grant[special_master][special_slave])
1244
                        &&(m_stb[special_master])
1245
                        &&(m_addr[special_master] == special_address)
1246
                        &&(!m_we[special_master])
1247
                        )
1248
                begin
1249
                        read_seq[0] <= 1;
1250
                end
1251
 
1252
                if (|read_seq)
1253
                begin
1254
                        assert(grant[special_master][special_slave]);
1255
                        assert(mgrant[special_master]);
1256
                        assert(sgrant[special_slave]);
1257
                        assert(mindex[special_master] == special_slave);
1258
                        assert(sindex[special_slave] == special_master);
1259
                        assert(!o_merr[special_master]);
1260
                end
1261
 
1262
                if (read_seq[0] && !$past(s_stall[special_slave]))
1263
                begin
1264
                        assert(o_scyc[special_slave]);
1265
                        assert(o_sstb[special_slave]);
1266
                        assert(!o_swe[special_slave]);
1267
                        assert(o_saddr[special_slave*AW +: AW] == special_address);
1268
 
1269
                        read_seq[1] <= 1;
1270
 
1271
                end else if (read_seq[0] && $past(s_stall[special_slave]))
1272
                begin
1273
                        assert($stable(m_stb[special_master]));
1274
                        assert(!m_we[special_master]);
1275
                        assert(m_addr[special_master] == special_address);
1276
 
1277
                        read_seq[0] <= 1;
1278
                end
1279
 
1280
                if (read_seq[1] && $past(s_stall[special_slave]))
1281
                begin
1282
                        assert(o_scyc[special_slave]);
1283
                        assert(o_sstb[special_slave]);
1284
                        assert(!o_swe[special_slave]);
1285
                        assert(o_saddr[special_slave*AW +: AW] == special_address);
1286
                        read_seq[1] <= 1;
1287
                end else if (read_seq[1] && !$past(s_stall[special_slave]))
1288
                begin
1289
                        assert(i_sack[special_slave]);
1290
                        assert(i_sdata[special_slave*DW +: DW] == $past(special_value));
1291
                        if (OPT_DBLBUFFER)
1292
                                read_seq[2] <= 1;
1293
                end
1294
 
1295
                if (read_seq[2] || ((!OPT_DBLBUFFER)&&read_seq[1]
1296
                                        && !$past(s_stall[special_slave])))
1297
                begin
1298
                        assert(o_mack[special_master]);
1299
                        assert(o_mdata[special_master * DW +: DW]
1300
                                == $past(special_value,2));
1301
                end
1302
        end else
1303
                read_seq <= 0;
1304
 
1305
        //
1306
        // Let's try a write assertion now.  Specifically, on any request to
1307
        // write to our special address, we want to assert that the special
1308
        // value at that address can be written.
1309
        reg     [2:0]    write_seq;
1310
        initial write_seq = 0;
1311
        always @(posedge i_clk)
1312
        if ((special_master < NM)&&(special_slave < NS)
1313
                        &&(i_mcyc[special_master])
1314
                        &&(!timed_out[special_master]))
1315
        begin
1316
                write_seq <= 0;
1317
                if ((grant[special_master][special_slave])
1318
                        &&(m_stb[special_master])
1319
                        &&(m_addr[special_master] == special_address)
1320
                        &&(m_we[special_master]))
1321
                begin
1322
                        // Our write sequence begins when our special master
1323
                        // has access to the bus, *and* he is trying to write
1324
                        // to our special address.
1325
                        write_seq[0] <= 1;
1326
                end
1327
 
1328
                if (|write_seq)
1329
                begin
1330
                        assert(grant[special_master][special_slave]);
1331
                        assert(mgrant[special_master]);
1332
                        assert(sgrant[special_slave]);
1333
                        assert(mindex[special_master] == special_slave);
1334
                        assert(sindex[special_slave] == special_master);
1335
                        assert(!o_merr[special_master]);
1336
                end
1337
 
1338
                if (write_seq[0] && !$past(s_stall[special_slave]))
1339
                begin
1340
                        assert(o_scyc[special_slave]);
1341
                        assert(o_sstb[special_slave]);
1342
                        assert(o_swe[special_slave]);
1343
                        assert(o_saddr[special_slave*AW +: AW] == special_address);
1344
                        assert(o_sdata[special_slave*DW +: DW]
1345
                                == $past(m_data[special_master]));
1346
                        assert(o_ssel[special_slave*DW/8 +: DW/8]
1347
                                == $past(m_sel[special_master]));
1348
 
1349
                        write_seq[1] <= 1;
1350
 
1351
                end else if (write_seq[0] && $past(s_stall[special_slave]))
1352
                begin
1353
                        assert($stable(m_stb[special_master]));
1354
                        assert(m_we[special_master]);
1355
                        assert(m_addr[special_master] == special_address);
1356
                        assert($stable(m_data[special_master]));
1357
                        assert($stable(m_sel[special_master]));
1358
 
1359
                        write_seq[0] <= 1;
1360
                end
1361
 
1362
                if (write_seq[1] && $past(s_stall[special_slave]))
1363
                begin
1364
                        assert(o_scyc[special_slave]);
1365
                        assert(o_sstb[special_slave]);
1366
                        assert(o_swe[special_slave]);
1367
                        assert(o_saddr[special_slave*AW +: AW] == special_address);
1368
                        assert($stable(o_sdata[special_slave*DW +: DW]));
1369
                        assert($stable(o_ssel[special_slave*DW/8 +: DW/8]));
1370
                        write_seq[1] <= 1;
1371
                end else if (write_seq[1] && !$past(s_stall[special_slave]))
1372
                begin
1373
                        for(iM=0; iM<DW/8; iM=iM+1)
1374
                        begin
1375
                                if ($past(o_ssel[special_slave * DW/8 + iM]))
1376
                                        assert(special_value[iM*8 +: 8]
1377
                                                == $past(o_sdata[special_slave*DW+iM*8 +: 8]));
1378
                        end
1379
 
1380
                        assert(i_sack[special_slave]);
1381
                        if (OPT_DBLBUFFER)
1382
                                write_seq[2] <= 1;
1383
                end
1384
 
1385
                if (write_seq[2] || ((!OPT_DBLBUFFER)&&write_seq[1]
1386
                                        && !$past(s_stall[special_slave])))
1387
                        assert(o_mack[special_master]);
1388
        end else
1389
                write_seq <= 0;
1390
 
1391
`endif
1392
endmodule

powered by: WebSVN 2.1.0

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