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

Subversion Repositories zipcpu

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

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 209 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    fwb_slave.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 slave.  These formal rules may be used
9
//      with yosys-smtbmc to *prove* that the slave properly handles outgoing
10
//      responses to (assumed correct) incoming requests.
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_master.v file in that
19
//      assumptions are made about the inputs to the slave: i_wb_cyc,
20
//      i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, and i_wb_sel, while full
21
//      assertions are made about the outputs: o_wb_stall, o_wb_ack, o_wb_data,
22
//      o_wb_err.  In the formal_master.v, assertions are made about the
23
//      master outputs (slave inputs)), and assumptions are made about the
24
//      master inputs (the slave outputs).
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_slave(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
        // If true, allow the bus to issue multiple discontinuous requests.
85
        // Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other
86
        // requests are outstanding
87
        parameter       [0:0]     F_OPT_DISCONTINUOUS = 0;
88
        //
89
        //
90
        // If true, insist that there be a minimum of a single clock delay
91
        // between request and response.  This defaults to off since the
92
        // wishbone specification specifically doesn't require this.  However,
93
        // some interfaces do, so we allow it as an option here.
94
        parameter       [0:0]     F_OPT_MINCLOCK_DELAY = 0;
95
        //
96
        //
97
        localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
98
        localparam      MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
99
                                ? F_MAX_STALL : F_MAX_ACK_DELAY;
100
        localparam      DLYBITS= (MAX_DELAY < 4) ? 2
101
                                : ((MAX_DELAY <    16) ? 4
102
                                : ((MAX_DELAY <    64) ? 6
103
                                : ((MAX_DELAY <   256) ? 8
104
                                : ((MAX_DELAY <  1024) ? 10
105
                                : ((MAX_DELAY <  4096) ? 12
106
                                : ((MAX_DELAY < 16384) ? 14
107
                                : ((MAX_DELAY < 65536) ? 16
108
                                : 32)))))));
109
        //
110
        input   wire                    i_clk, i_reset;
111
        // Input/master bus
112
        input   wire                    i_wb_cyc, i_wb_stb, i_wb_we;
113
        input   wire    [(AW-1):0]       i_wb_addr;
114
        input   wire    [(DW-1):0]       i_wb_data;
115
        input   wire    [(DW/8-1):0]     i_wb_sel;
116
        //
117
        input   wire                    i_wb_ack;
118
        input   wire                    i_wb_stall;
119
        input   wire    [(DW-1):0]       i_wb_idata;
120
        input   wire                    i_wb_err;
121
        //
122
        output  reg     [(F_LGDEPTH-1):0]        f_nreqs, f_nacks;
123
        output  wire    [(F_LGDEPTH-1):0]        f_outstanding;
124
 
125
`define SLAVE_ASSUME    assume
126
`define SLAVE_ASSERT    assert
127
        //
128
        // Let's just make sure our parameters are set up right
129
        //
130
        initial assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
131
 
132
        //
133
        // Wrap the request line in a bundle.  The top bit, named STB_BIT,
134
        // is the bit indicating whether the request described by this vector
135
        // is a valid request or not.
136
        //
137
        localparam      STB_BIT = 2+AW+DW+DW/8-1;
138
        wire    [STB_BIT:0]      f_request;
139
        assign  f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel };
140
 
141
        //
142
        // A quick register to be used later to know if the $past() operator
143
        // will yield valid result
144
        reg     f_past_valid;
145
        initial f_past_valid = 1'b0;
146
        always @(posedge i_clk)
147
                f_past_valid <= 1'b1;
148
        always @(*)
149
        if (!f_past_valid)
150
                `SLAVE_ASSUME(i_reset);
151
        //
152
        //
153
        // Assertions regarding the initial (and reset) state
154
        //
155
        //
156
 
157
        //
158
        // Assume we start from a reset condition
159
        initial assert(i_reset);
160
        initial `SLAVE_ASSUME(!i_wb_cyc);
161
        initial `SLAVE_ASSUME(!i_wb_stb);
162
        //
163
        initial `SLAVE_ASSERT(!i_wb_ack);
164
        initial `SLAVE_ASSERT(!i_wb_err);
165
 
166
        always @(posedge i_clk)
167
        if ((!f_past_valid)||($past(i_reset)))
168
        begin
169
                `SLAVE_ASSUME(!i_wb_cyc);
170
                `SLAVE_ASSUME(!i_wb_stb);
171
                //
172
                `SLAVE_ASSERT(!i_wb_ack);
173
                `SLAVE_ASSERT(!i_wb_err);
174
        end
175
 
176
        always @(*)
177
        if (!f_past_valid)
178
                `SLAVE_ASSUME(!i_wb_cyc);
179
 
180
        //
181
        //
182
        // Bus requests
183
        //
184
        //
185
 
186
        // Following any bus error, the CYC line should be dropped to abort
187
        // the transaction
188
        always @(posedge i_clk)
189
        if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
190
                `SLAVE_ASSUME(!i_wb_cyc);
191
 
192
        // STB can only be true if CYC is also true
193
        always @(*)
194
        if (i_wb_stb)
195
                `SLAVE_ASSUME(i_wb_cyc);
196
 
197
        // If a request was both outstanding and stalled on the last clock,
198
        // then nothing should change on this clock regarding it.
199
        always @(posedge i_clk)
200
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
201
                        &&($past(i_wb_stall))&&(i_wb_cyc))
202
        begin
203
                `SLAVE_ASSUME(i_wb_stb);
204
                `SLAVE_ASSUME(i_wb_we   == $past(i_wb_we));
205
                `SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
206
                `SLAVE_ASSUME(i_wb_sel  == $past(i_wb_sel));
207
                if (i_wb_we)
208
                        `SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
209
        end
210
 
211
        // Within any series of STB/requests, the direction of the request
212
        // may not change.
213
        always @(posedge i_clk)
214
        if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
215
                `SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
216
 
217
 
218
        // Within any given bus cycle, the direction may *only* change when
219
        // there are no further outstanding requests.
220
        always @(posedge i_clk)
221
        if ((f_past_valid)&&(f_outstanding > 0))
222
                `SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
223
 
224
        // Write requests must also set one (or more) of i_wb_sel
225
        // always @(*)
226
        // if ((i_wb_stb)&&(i_wb_we))
227
        //      `SLAVE_ASSUME(|i_wb_sel);
228
 
229
 
230
        //
231
        //
232
        // Bus responses
233
        //
234
        //
235
 
236
        // If CYC was low on the last clock, then both ACK and ERR should be
237
        // low on this clock.
238
        always @(posedge i_clk)
239
        if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
240
        begin
241
                `SLAVE_ASSERT(!i_wb_ack);
242
                `SLAVE_ASSERT(!i_wb_err);
243
                // Stall may still be true--such as when we are not
244
                // selected at some arbiter between us and the slave
245
        end
246
 
247
        //
248
        // Any time the CYC line drops, it is possible that there may be a
249
        // remaining (registered) ACK or ERR that hasn't yet been returned.
250
        // Restrict such out of band returns so that they are *only* returned
251
        // if there is an outstanding operation.
252
        always @(posedge i_clk)
253
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
254
        begin
255
                if (($past(f_outstanding == 0))
256
                        &&((!$past(i_wb_stb && !i_wb_stall))
257
                                ||($past(i_wb_ack|i_wb_err))))
258
                begin
259
                        `SLAVE_ASSERT(!i_wb_ack);
260
                        `SLAVE_ASSERT(!i_wb_err);
261
                end
262
        end
263
 
264
        // ACK and ERR may never both be true at the same time
265
        always @(*)
266
                `SLAVE_ASSERT((!i_wb_ack)||(!i_wb_err));
267
 
268
        generate if (F_MAX_STALL > 0)
269
        begin : MXSTALL
270
                //
271
                // Assume the slave cannnot stall for more than F_MAX_STALL
272
                // counts.  We'll count this forward any time STB and STALL
273
                // are both true.
274
                //
275
                reg     [(DLYBITS-1):0]          f_stall_count;
276
 
277
                initial f_stall_count = 0;
278
                always @(posedge i_clk)
279
                if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
280
                        f_stall_count <= f_stall_count + 1'b1;
281
                else
282
                        f_stall_count <= 0;
283
 
284
                always @(*)
285
                if (i_wb_cyc)
286
                        `SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
287
        end endgenerate
288
 
289
        generate if (F_MAX_ACK_DELAY > 0)
290
        begin : MXWAIT
291
                //
292
                // Assume the slave will respond within F_MAX_ACK_DELAY cycles,
293
                // counted either from the end of the last request, or from the
294
                // last ACK received
295
                //
296
                reg     [(DLYBITS-1):0]          f_ackwait_count;
297
 
298
                initial f_ackwait_count = 0;
299
                always @(posedge i_clk)
300
                if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
301
                                &&(!i_wb_ack)&&(!i_wb_err)
302
                                &&(f_outstanding > 0))
303
                        f_ackwait_count <= f_ackwait_count + 1'b1;
304
                else
305
                        f_ackwait_count <= 0;
306
 
307
                always @(*)
308
                if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
309
                                        &&(!i_wb_ack)&&(!i_wb_err)
310
                                        &&(f_outstanding > 0))
311
                        `SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
312
        end endgenerate
313
 
314
        //
315
        // Count the number of requests that have been received
316
        //
317
        initial f_nreqs = 0;
318
        always @(posedge i_clk)
319
        if ((i_reset)||(!i_wb_cyc))
320
                f_nreqs <= 0;
321
        else if ((i_wb_stb)&&(!i_wb_stall))
322
                f_nreqs <= f_nreqs + 1'b1;
323
 
324
 
325
        //
326
        // Count the number of acknowledgements that have been returned
327
        //
328
        initial f_nacks = 0;
329
        always @(posedge i_clk)
330
        if (i_reset)
331
                f_nacks <= 0;
332
        else if (!i_wb_cyc)
333
                f_nacks <= 0;
334
        else if ((i_wb_ack)||(i_wb_err))
335
                f_nacks <= f_nacks + 1'b1;
336
 
337
        //
338
        // The number of outstanding requests is the difference between
339
        // the number of requests and the number of acknowledgements
340
        //
341
        assign  f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;
342
 
343
        always @(*)
344
        if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
345
        begin
346
                if (i_wb_stb)
347
                        `SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
348
                else
349
                        `SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
350
                `SLAVE_ASSERT(f_nacks <= f_nreqs);
351
                assert(f_outstanding < (1<<F_LGDEPTH)-1);
352
        end else
353
                assume(f_outstanding < (1<<F_LGDEPTH)-1);
354
 
355
        always @(*)
356
        if ((i_wb_cyc)&&(f_outstanding == 0))
357
        begin
358
                // If nothing is outstanding, then there should be
359
                // no acknowledgements ... however, an acknowledgement
360
                // *can* come back on the same clock as the stb is
361
                // going out.
362
                if (F_OPT_MINCLOCK_DELAY)
363
                begin
364
                        `SLAVE_ASSERT(!i_wb_ack);
365
                        `SLAVE_ASSERT(!i_wb_err);
366
                end else begin
367
                        `SLAVE_ASSERT((!i_wb_ack)||((i_wb_stb)&&(!i_wb_stall)));
368
                        // The same is true of errors.  They may not be
369
                        // created before the request gets through
370
                        `SLAVE_ASSERT((!i_wb_err)||((i_wb_stb)&&(!i_wb_stall)));
371
                end
372
        end
373
 
374
        generate if (!F_OPT_RMW_BUS_OPTION)
375
        begin
376
                // If we aren't waiting for anything, and we aren't issuing
377
                // any requests, then then our transaction is over and we
378
                // should be dropping the CYC line.
379
                always @(*)
380
                if (f_outstanding == 0)
381
                        `SLAVE_ASSUME((i_wb_stb)||(!i_wb_cyc));
382
                // Not all masters will abide by this restriction.  Some
383
                // masters may wish to implement read-modify-write bus
384
                // interactions.  These masters need to keep CYC high between
385
                // transactions, even though nothing is outstanding.  For
386
                // these busses, turn F_OPT_RMW_BUS_OPTION on.
387
        end endgenerate
388
 
389
        generate if ((!F_OPT_DISCONTINUOUS)&&(!F_OPT_RMW_BUS_OPTION))
390
        begin : INSIST_ON_NO_DISCONTINUOUS_STBS
391
                // Within my own code, once a request begins it goes to
392
                // completion and the CYC line is dropped.  The master
393
                // is not allowed to raise STB again after dropping it.
394
                // Doing so would be a *discontinuous* request.
395
                //
396
                // However, in any RMW scheme, discontinuous requests are
397
                // necessary, and the spec doesn't disallow them.  Hence we
398
                // make this check optional.
399
                always @(posedge i_clk)
400
                if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
401
                        `SLAVE_ASSUME(!i_wb_stb);
402
        end endgenerate
403
 
404
endmodule

powered by: WebSVN 2.1.0

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