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

Subversion Repositories wb2axip

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

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

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

powered by: WebSVN 2.1.0

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