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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [ex/] [fwb_master.v] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 209 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    fwb_master.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     This file describes the rules of a wishbone interaction from the
8
//              perspective of a wishbone master.  These formal rules may be used
9
//      with yosys-smtbmc to *prove* that the master properly handles outgoing
10
//      transactions and incoming responses.
11
//
12
//      This module contains no functional logic.  It is intended for formal
13
//      verification only.  The outputs returned, the number of requests that
14
//      have been made, the number of acknowledgements received, and the number
15
//      of outstanding requests, are designed for further formal verification
16
//      purposes *only*.
17
//
18
//      This file is different from a companion formal_slave.v file in that the
19
//      assertions are made on the outputs of the wishbone master: o_wb_cyc,
20
//      o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, and o_wb_sel, while only
21
//      assumptions are made about the inputs: i_wb_stall, i_wb_ack, i_wb_data,
22
//      i_wb_err.  In the formal_slave.v, assumptions are made about the
23
//      slave inputs (the master outputs), and assertions are made about the
24
//      slave outputs (the master inputs).
25
//
26
//      In order to make it easier to compare the slave against the master,
27
//      assumptions with respect to the slave have been marked with the
28
//      `SLAVE_ASSUME macro.  Similarly, assertions the slave would make have
29
//      been marked with `SLAVE_ASSERT.  This allows the master to redefine
30
//      these two macros to be from his perspective, and therefore the
31
//      diffs between the two files actually show true differences, rather
32
//      than just these differences in perspective.
33
//
34
//
35
// Creator:     Dan Gisselquist, Ph.D.
36
//              Gisselquist Technology, LLC
37
//
38
////////////////////////////////////////////////////////////////////////////////
39
//
40
// Copyright (C) 2017-2019, Gisselquist Technology, LLC
41
//
42
// This program is free software (firmware): you can redistribute it and/or
43
// modify it under the terms of  the GNU General Public License as published
44
// by the Free Software Foundation, either version 3 of the License, or (at
45
// your option) any later version.
46
//
47
// This program is distributed in the hope that it will be useful, but WITHOUT
48
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
49
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
50
// for more details.
51
//
52
// You should have received a copy of the GNU General Public License along
53
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
54
// target there if the PDF file isn't present.)  If not, see
55
// <http://www.gnu.org/licenses/> for a copy.
56
//
57
// License:     GPL, v3, as defined and found on www.gnu.org,
58
//              http://www.gnu.org/licenses/gpl.html
59
//
60
//
61
////////////////////////////////////////////////////////////////////////////////
62
//
63
//
64
`default_nettype none
65
//
66
module  fwb_master(i_clk, i_reset,
67
                // The Wishbone bus
68
                i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel,
69
                        i_wb_ack, i_wb_stall, i_wb_idata, i_wb_err,
70
                // Some convenience output parameters
71
                f_nreqs, f_nacks, f_outstanding);
72
        parameter               AW=32, DW=32;
73
        parameter               F_MAX_STALL = 0,
74
                                F_MAX_ACK_DELAY = 0;
75
        parameter               F_LGDEPTH = 4;
76
        parameter [(F_LGDEPTH-1):0] F_MAX_REQUESTS = 0;
77
        //
78
        // If true, allow the bus to be kept open when there are no outstanding
79
        // requests.  This is useful for any master that might execute a
80
        // read modify write cycle, such as an atomic add.
81
        parameter [0:0]           F_OPT_RMW_BUS_OPTION = 1;
82
        //
83
        // 
84
        parameter [0:0]           F_OPT_SHORT_CIRCUIT_PROOF = 0;
85
        //
86
        // If this is the source of a request, then we can assume STB and CYC
87
        // will initially start out high.  Master interfaces following the
88
        // source on the way to the slave may not have this property
89
        parameter [0:0]           F_OPT_SOURCE = 0;
90
        //
91
        // If true, allow the bus to issue multiple discontinuous requests.
92
        // Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other
93
        // requests are outstanding
94
        parameter       [0:0]     F_OPT_DISCONTINUOUS = 0;
95
        //
96
        //
97
        // If true, insist that there be a minimum of a single clock delay
98
        // between request and response.  This defaults to off since the
99
        // wishbone specification specifically doesn't require this.  However,
100
        // some interfaces do, so we allow it as an option here.
101
        parameter       [0:0]     F_OPT_MINCLOCK_DELAY = 0;
102
        //
103
        //
104
        localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
105
        localparam      MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
106
                                ? F_MAX_STALL : F_MAX_ACK_DELAY;
107
        localparam      DLYBITS= (MAX_DELAY < 4) ? 2
108
                                : ((MAX_DELAY <    16) ? 4
109
                                : ((MAX_DELAY <    64) ? 6
110
                                : ((MAX_DELAY <   256) ? 8
111
                                : ((MAX_DELAY <  1024) ? 10
112
                                : ((MAX_DELAY <  4096) ? 12
113
                                : ((MAX_DELAY < 16384) ? 14
114
                                : ((MAX_DELAY < 65536) ? 16
115
                                : 32)))))));
116
        //
117
        input   wire                    i_clk, i_reset;
118
        // Input/master bus
119
        input   wire                    i_wb_cyc, i_wb_stb, i_wb_we;
120
        input   wire    [(AW-1):0]       i_wb_addr;
121
        input   wire    [(DW-1):0]       i_wb_data;
122
        input   wire    [(DW/8-1):0]     i_wb_sel;
123
        //
124
        input   wire                    i_wb_ack;
125
        input   wire                    i_wb_stall;
126
        input   wire    [(DW-1):0]       i_wb_idata;
127
        input   wire                    i_wb_err;
128
        //
129
        output  reg     [(F_LGDEPTH-1):0]        f_nreqs, f_nacks;
130
        output  wire    [(F_LGDEPTH-1):0]        f_outstanding;
131
 
132
`define SLAVE_ASSUME    assert
133
`define SLAVE_ASSERT    assume
134
        //
135
        // Let's just make sure our parameters are set up right
136
        //
137
        initial assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
138
 
139
        //
140
        // Wrap the request line in a bundle.  The top bit, named STB_BIT,
141
        // is the bit indicating whether the request described by this vector
142
        // is a valid request or not.
143
        //
144
        localparam      STB_BIT = 2+AW+DW+DW/8-1;
145
        wire    [STB_BIT:0]      f_request;
146
        assign  f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel };
147
 
148
        //
149
        // A quick register to be used later to know if the $past() operator
150
        // will yield valid result
151
        reg     f_past_valid;
152
        initial f_past_valid = 1'b0;
153
        always @(posedge i_clk)
154
                f_past_valid <= 1'b1;
155
        always @(*)
156
        if (!f_past_valid)
157
                `SLAVE_ASSUME(i_reset);
158
        //
159
        //
160
        // Assertions regarding the initial (and reset) state
161
        //
162
        //
163
 
164
        //
165
        // Assume we start from a reset condition
166
        initial assert(i_reset);
167
        initial `SLAVE_ASSUME(!i_wb_cyc);
168
        initial `SLAVE_ASSUME(!i_wb_stb);
169
        //
170
        initial `SLAVE_ASSERT(!i_wb_ack);
171
        initial `SLAVE_ASSERT(!i_wb_err);
172
 
173
        always @(posedge i_clk)
174
        if ((!f_past_valid)||($past(i_reset)))
175
        begin
176
                `SLAVE_ASSUME(!i_wb_cyc);
177
                `SLAVE_ASSUME(!i_wb_stb);
178
                //
179
                `SLAVE_ASSERT(!i_wb_ack);
180
                `SLAVE_ASSERT(!i_wb_err);
181
        end
182
 
183
        always @(*)
184
        if (!f_past_valid)
185
                `SLAVE_ASSUME(!i_wb_cyc);
186
 
187
        //
188
        //
189
        // Bus requests
190
        //
191
        //
192
 
193
        // Following any bus error, the CYC line should be dropped to abort
194
        // the transaction
195
        always @(posedge i_clk)
196
        if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
197
                `SLAVE_ASSUME(!i_wb_cyc);
198
 
199
        // STB can only be true if CYC is also true
200
        always @(*)
201
        if (i_wb_stb)
202
                `SLAVE_ASSUME(i_wb_cyc);
203
 
204
        // If a request was both outstanding and stalled on the last clock,
205
        // then nothing should change on this clock regarding it.
206
        always @(posedge i_clk)
207
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
208
                        &&($past(i_wb_stall))&&(i_wb_cyc))
209
        begin
210
                `SLAVE_ASSUME(i_wb_stb);
211
                `SLAVE_ASSUME(i_wb_we   == $past(i_wb_we));
212
                `SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
213
                `SLAVE_ASSUME(i_wb_sel  == $past(i_wb_sel));
214
                if (i_wb_we)
215
                        `SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
216
        end
217
 
218
        // Within any series of STB/requests, the direction of the request
219
        // may not change.
220
        always @(posedge i_clk)
221
        if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
222
                `SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
223
 
224
 
225
        // Within any given bus cycle, the direction may *only* change when
226
        // there are no further outstanding requests.
227
        always @(posedge i_clk)
228
        if ((f_past_valid)&&(f_outstanding > 0))
229
                `SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
230
 
231
        // Write requests must also set one (or more) of i_wb_sel
232
        // always @(*)
233
        // if ((i_wb_stb)&&(i_wb_we))
234
        //      `SLAVE_ASSUME(|i_wb_sel);
235
 
236
 
237
        //
238
        //
239
        // Bus responses
240
        //
241
        //
242
 
243
        // If CYC was low on the last clock, then both ACK and ERR should be
244
        // low on this clock.
245
        always @(posedge i_clk)
246
        if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
247
        begin
248
                `SLAVE_ASSERT(!i_wb_ack);
249
                `SLAVE_ASSERT(!i_wb_err);
250
                // Stall may still be true--such as when we are not
251
                // selected at some arbiter between us and the slave
252
        end
253
 
254
        //
255
        // Any time the CYC line drops, it is possible that there may be a
256
        // remaining (registered) ACK or ERR that hasn't yet been returned.
257
        // Restrict such out of band returns so that they are *only* returned
258
        // if there is an outstanding operation.
259
        always @(posedge i_clk)
260
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
261
        begin
262
                if (($past(f_outstanding == 0))
263
                        &&((!$past(i_wb_stb && !i_wb_stall))
264
                                ||($past(i_wb_ack|i_wb_err))))
265
                begin
266
                        `SLAVE_ASSERT(!i_wb_ack);
267
                        `SLAVE_ASSERT(!i_wb_err);
268
                end
269
        end
270
 
271
        // ACK and ERR may never both be true at the same time
272
        always @(*)
273
                `SLAVE_ASSERT((!i_wb_ack)||(!i_wb_err));
274
 
275
        generate if (F_MAX_STALL > 0)
276
        begin : MXSTALL
277
                //
278
                // Assume the slave cannnot stall for more than F_MAX_STALL
279
                // counts.  We'll count this forward any time STB and STALL
280
                // are both true.
281
                //
282
                reg     [(DLYBITS-1):0]          f_stall_count;
283
 
284
                initial f_stall_count = 0;
285
                always @(posedge i_clk)
286
                if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
287
                        f_stall_count <= f_stall_count + 1'b1;
288
                else
289
                        f_stall_count <= 0;
290
 
291
                always @(*)
292
                if (i_wb_cyc)
293
                        `SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
294
        end endgenerate
295
 
296
        generate if (F_MAX_ACK_DELAY > 0)
297
        begin : MXWAIT
298
                //
299
                // Assume the slave will respond within F_MAX_ACK_DELAY cycles,
300
                // counted either from the end of the last request, or from the
301
                // last ACK received
302
                //
303
                reg     [(DLYBITS-1):0]          f_ackwait_count;
304
 
305
                initial f_ackwait_count = 0;
306
                always @(posedge i_clk)
307
                if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
308
                                &&(!i_wb_ack)&&(!i_wb_err)
309
                                &&(f_outstanding > 0))
310
                        f_ackwait_count <= f_ackwait_count + 1'b1;
311
                else
312
                        f_ackwait_count <= 0;
313
 
314
                always @(*)
315
                if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
316
                                        &&(!i_wb_ack)&&(!i_wb_err)
317
                                        &&(f_outstanding > 0))
318
                        `SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
319
        end endgenerate
320
 
321
        //
322
        // Count the number of requests that have been made
323
        //
324
        initial f_nreqs = 0;
325
        always @(posedge i_clk)
326
        if ((i_reset)||(!i_wb_cyc))
327
                f_nreqs <= 0;
328
        else if ((i_wb_stb)&&(!i_wb_stall))
329
                f_nreqs <= f_nreqs + 1'b1;
330
 
331
 
332
        //
333
        // Count the number of acknowledgements that have been received
334
        //
335
        initial f_nacks = 0;
336
        always @(posedge i_clk)
337
        if (i_reset)
338
                f_nacks <= 0;
339
        else if (!i_wb_cyc)
340
                f_nacks <= 0;
341
        else if ((i_wb_ack)||(i_wb_err))
342
                f_nacks <= f_nacks + 1'b1;
343
 
344
        //
345
        // The number of outstanding requests is the difference between
346
        // the number of requests and the number of acknowledgements
347
        //
348
        assign  f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;
349
 
350
        always @(*)
351
        if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
352
        begin
353
                if (i_wb_stb)
354
                        `SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
355
                else
356
                        `SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
357
                `SLAVE_ASSERT(f_nacks <= f_nreqs);
358
                assert(f_outstanding < (1<<F_LGDEPTH)-1);
359
        end else
360
                assume(f_outstanding < (1<<F_LGDEPTH)-1);
361
 
362
        always @(*)
363
        if ((i_wb_cyc)&&(f_outstanding == 0))
364
        begin
365
                // If nothing is outstanding, then there should be
366
                // no acknowledgements ... however, an acknowledgement
367
                // *can* come back on the same clock as the stb is
368
                // going out.
369
                if (F_OPT_MINCLOCK_DELAY)
370
                begin
371
                        `SLAVE_ASSERT(!i_wb_ack);
372
                        `SLAVE_ASSERT(!i_wb_err);
373
                end else begin
374
                        `SLAVE_ASSERT((!i_wb_ack)||((i_wb_stb)&&(!i_wb_stall)));
375
                        // The same is true of errors.  They may not be
376
                        // created before the request gets through
377
                        `SLAVE_ASSERT((!i_wb_err)||((i_wb_stb)&&(!i_wb_stall)));
378
                end
379
        end
380
 
381
        generate if (F_OPT_SOURCE)
382
        begin : SRC
383
                // Any opening bus request starts with both CYC and STB high
384
                // This is true for the master only, and more specifically
385
                // only for those masters that are the initial source of any
386
                // transaction.  By the time an interaction gets to the slave,
387
                // the CYC line may go high or low without actually affecting
388
                // the STB line of the slave.
389
                always @(posedge i_clk)
390
                if ((f_past_valid)&&(!$past(i_wb_cyc))&&(i_wb_cyc))
391
                        `SLAVE_ASSUME(i_wb_stb);
392
        end endgenerate
393
 
394
 
395
        generate if (!F_OPT_RMW_BUS_OPTION)
396
        begin
397
                // If we aren't waiting for anything, and we aren't issuing
398
                // any requests, then then our transaction is over and we
399
                // should be dropping the CYC line.
400
                always @(*)
401
                if (f_outstanding == 0)
402
                        `SLAVE_ASSUME((i_wb_stb)||(!i_wb_cyc));
403
                // Not all masters will abide by this restriction.  Some
404
                // masters may wish to implement read-modify-write bus
405
                // interactions.  These masters need to keep CYC high between
406
                // transactions, even though nothing is outstanding.  For
407
                // these busses, turn F_OPT_RMW_BUS_OPTION on.
408
        end endgenerate
409
 
410
        generate if (F_OPT_SHORT_CIRCUIT_PROOF)
411
        begin
412
                // In many ways, we don't care what happens on the bus return
413
                // lines if the cycle line is low, so restricting them to a
414
                // known value makes a lot of sense.
415
                //
416
                // On the other hand, if something above *does* depend upon
417
                // these values (when it shouldn't), then we might want to know
418
                // about it.
419
                //
420
                //
421
                always @(posedge i_clk)
422
                begin
423
                        if (!i_wb_cyc)
424
                        begin
425
                                assume(!i_wb_stall);
426
                                assume($stable(i_wb_idata));
427
                        end else if ((!$past(i_wb_ack))&&(!i_wb_ack))
428
                                assume($stable(i_wb_idata));
429
                end
430
        end endgenerate
431
 
432
        generate if ((!F_OPT_DISCONTINUOUS)&&(!F_OPT_RMW_BUS_OPTION))
433
        begin : INSIST_ON_NO_DISCONTINUOUS_STBS
434
                // Within my own code, once a request begins it goes to
435
                // completion and the CYC line is dropped.  The master
436
                // is not allowed to raise STB again after dropping it.
437
                // Doing so would be a *discontinuous* request.
438
                //
439
                // However, in any RMW scheme, discontinuous requests are
440
                // necessary, and the spec doesn't disallow them.  Hence we
441
                // make this check optional.
442
                always @(posedge i_clk)
443
                if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
444
                        `SLAVE_ASSUME(!i_wb_stb);
445
        end endgenerate
446
 
447
endmodule

powered by: WebSVN 2.1.0

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