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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [core/] [div.v] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
2 69 dgisselq
//
3
// Filename:    div.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7 201 dgisselq
// Purpose:     Provide an Integer divide capability to the Zip CPU.  Provides
8
//              for both signed and unsigned divide.
9 69 dgisselq
//
10 201 dgisselq
// Steps:
11 209 dgisselq
//      i_reset The DIVide unit starts in idle.  It can also be placed into an
12 201 dgisselq
//      idle by asserting the reset input.
13 69 dgisselq
//
14 209 dgisselq
//      i_wr    When i_reset is asserted, a divide begins.  On the next clock:
15 201 dgisselq
//
16
//        o_busy is set high so everyone else knows we are at work and they can
17
//              wait for us to complete.
18
//
19
//        pre_sign is set to true if we need to do a signed divide.  In this
20
//              case, we take a clock cycle to turn the divide into an unsigned
21
//              divide.
22
//
23
//        o_quotient, a place to store our result, is initialized to all zeros.
24
//
25
//        r_dividend is set to the numerator
26
//
27
//        r_divisor is set to 2^31 * the denominator (shift left by 31, or add
28
//              31 zeros to the right of the number.
29
//
30
//      pre_sign When true (clock cycle after i_wr), a clock cycle is used
31
//              to take the absolute value of the various arguments (r_dividend
32
//              and r_divisor), and to calculate what sign the output result
33
//              should be.
34
//
35
//
36
//      At this point, the divide is has started.  The divide works by walking
37 205 dgisselq
//      through every shift of the
38 201 dgisselq
//
39
//                  DIVIDEND    over the
40
//              DIVISOR
41
//
42
//      If the DIVISOR is bigger than the dividend, the divisor is shifted
43
//      right, and nothing is done to the output quotient.
44
//
45
//                  DIVIDEND
46
//               DIVISOR
47
//
48
//      This repeats, until DIVISOR is less than or equal to the divident, as in
49
//
50
//              DIVIDEND
51
//              DIVISOR
52
//
53 205 dgisselq
//      At this point, if the DIVISOR is less than the dividend, the
54 201 dgisselq
//      divisor is subtracted from the dividend, and the DIVISOR is again
55
//      shifted to the right.  Further, a '1' bit gets set in the output
56
//      quotient.
57
//
58
//      Once we've done this for 32 clocks, we've accumulated our answer into
59
//      the output quotient, and we can proceed to the next step.  If the
60
//      result will be signed, the next step negates the quotient, otherwise
61
//      it returns the result.
62
//
63
//      On the clock when we are done, o_busy is set to false, and o_valid set
64
//      to true.  (It is a violation of the ZipCPU internal protocol for both
65 205 dgisselq
//      busy and valid to ever be true on the same clock.  It is also a
66 201 dgisselq
//      violation for busy to be false with valid true thereafter.)
67
//
68
//
69 69 dgisselq
// Creator:     Dan Gisselquist, Ph.D.
70
//              Gisselquist Technology, LLC
71
//
72 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
73 69 dgisselq
//
74 209 dgisselq
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
75 69 dgisselq
//
76
// This program is free software (firmware): you can redistribute it and/or
77
// modify it under the terms of  the GNU General Public License as published
78
// by the Free Software Foundation, either version 3 of the License, or (at
79
// your option) any later version.
80
//
81
// This program is distributed in the hope that it will be useful, but WITHOUT
82
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
83
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
84
// for more details.
85
//
86 201 dgisselq
// You should have received a copy of the GNU General Public License along
87
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
88
// target there if the PDF file isn't present.)  If not, see
89
// <http://www.gnu.org/licenses/> for a copy.
90
//
91 69 dgisselq
// License:     GPL, v3, as defined and found on www.gnu.org,
92
//              http://www.gnu.org/licenses/gpl.html
93
//
94
//
95 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
96 69 dgisselq
//
97 201 dgisselq
//
98 209 dgisselq
`default_nettype        none
99
//
100 69 dgisselq
// `include "cpudefs.v"
101
//
102 209 dgisselq
module  div(i_clk, i_reset, i_wr, i_signed, i_numerator, i_denominator,
103 69 dgisselq
                o_busy, o_valid, o_err, o_quotient, o_flags);
104 196 dgisselq
        parameter               BW=32, LGBW = 5;
105 209 dgisselq
        input   wire            i_clk, i_reset;
106 69 dgisselq
        // Input parameters
107 209 dgisselq
        input   wire            i_wr, i_signed;
108
        input   wire [(BW-1):0]  i_numerator, i_denominator;
109 69 dgisselq
        // Output parameters
110
        output  reg             o_busy, o_valid, o_err;
111
        output  reg [(BW-1):0]   o_quotient;
112
        output  wire    [3:0]    o_flags;
113
 
114 160 dgisselq
        // r_busy is an internal busy register.  It will clear one clock
115
        // before we are valid, so it can't be o_busy ...
116
        //
117
        reg                     r_busy;
118 209 dgisselq
        reg     [BW-1:0] r_divisor;
119
        reg     [(2*BW-2):0]     r_dividend;
120 69 dgisselq
        wire    [(BW):0] diff; // , xdiff[(BW-1):0];
121 209 dgisselq
        assign  diff = r_dividend[2*BW-2:BW-1] - r_divisor;
122 69 dgisselq
 
123 160 dgisselq
        reg             r_sign, pre_sign, r_z, r_c, last_bit;
124
        reg     [(LGBW-1):0]     r_bit;
125 174 dgisselq
        reg     zero_divisor;
126
 
127 205 dgisselq
        // The Divide logic begins with r_busy.  We use r_busy to determine
128
        // whether or not the divide is in progress, vs being complete.
129
        // Here, we clear r_busy on any reset and set it on i_wr (the request
130
        // do to a divide).  The divide ends when we are on the last bit,
131
        // or equivalently when we discover we are dividing by zero.
132 160 dgisselq
        initial r_busy = 1'b0;
133 69 dgisselq
        always @(posedge i_clk)
134 209 dgisselq
        if (i_reset)
135
                r_busy <= 1'b0;
136
        else if (i_wr)
137
                r_busy <= 1'b1;
138
        else if ((last_bit)||(zero_divisor))
139
                r_busy <= 1'b0;
140 160 dgisselq
 
141 205 dgisselq
        // o_busy is very similar to r_busy, save for some key differences.
142
        // Primary among them is that o_busy needs to (possibly) be true
143
        // for an extra clock after r_busy clears.  This would be that extra
144
        // clock where we negate the result (assuming a signed divide, and that
145
        // the result is supposed to be negative.)  Otherwise, the two are
146
        // identical.
147 160 dgisselq
        initial o_busy = 1'b0;
148
        always @(posedge i_clk)
149 209 dgisselq
        if (i_reset)
150
                o_busy <= 1'b0;
151
        else if (i_wr)
152
                o_busy <= 1'b1;
153
        else if (((last_bit)&&(!r_sign))||(zero_divisor))
154
                o_busy <= 1'b0;
155
        else if (!r_busy)
156
                o_busy <= 1'b0;
157 88 dgisselq
 
158
        always @(posedge i_clk)
159 209 dgisselq
        if (i_wr)
160
                zero_divisor <= (i_denominator == 0);
161 205 dgisselq
 
162
        // o_valid is part of the ZipCPU protocol.  It will be set to true
163
        // anytime our answer is valid and may be used by the calling module.
164
        // Indeed, the ZipCPU will halt (and ignore us) once the i_wr has been
165
        // set until o_valid gets set.
166
        //
167
        // Here, we clear o_valid on a reset, and any time we are on the last
168
        // bit while busy (provided the sign is zero, or we are dividing by
169
        // zero).  Since o_valid is self-clearing, we don't need to clear
170
        // it on an i_wr signal.
171
        initial o_valid = 1'b0;
172
        always @(posedge i_clk)
173 209 dgisselq
        if ((i_reset)||(o_valid))
174
                o_valid <= 1'b0;
175
        else if ((r_busy)&&(zero_divisor))
176
                o_valid <= 1'b1;
177
        else if (r_busy)
178
        begin
179
                if (last_bit)
180
                        o_valid <= (!r_sign);
181
        end else if (r_sign)
182
        begin
183
                o_valid <= 1'b1;
184
        end else
185
                o_valid <= 1'b0;
186 69 dgisselq
 
187 205 dgisselq
        // Division by zero error reporting.  Anytime we detect a zero divisor,
188
        // we set our output error, and then hold it until we are valid and
189
        // everything clears.
190 174 dgisselq
        initial o_err = 1'b0;
191 69 dgisselq
        always @(posedge i_clk)
192 209 dgisselq
        if (i_reset)
193
                o_err <= 1'b0;
194
        else if ((r_busy)&&(zero_divisor))
195
                o_err <= 1'b1;
196
        else
197
                o_err <= 1'b0;
198 69 dgisselq
 
199 205 dgisselq
        // r_bit
200
        //
201
        // Keep track of which "bit" of our divide we are on.  This number
202
        // ranges from 31 down to zero.  On any write, we set ourselves to
203
        // 5'h1f.  Otherwise, while we are busy (but not within the pre-sign
204
        // adjustment stage), we subtract one from our value on every clock.
205 209 dgisselq
        initial r_bit = 0;
206 205 dgisselq
        always @(posedge i_clk)
207 209 dgisselq
        if (i_reset)
208
                r_bit <= 0;
209
        else if ((r_busy)&&(!pre_sign))
210
                r_bit <= r_bit + 1'b1;
211
        else
212
                r_bit <= 0;
213 205 dgisselq
 
214
        // last_bit
215
        //
216
        // This logic replaces a lot of logic that was inside our giant state
217
        // machine with ... something simpler.  In particular, we'll use this
218 209 dgisselq
        // logic to determine if we are processing our last bit.  The only trick
219
        // is, this bit needs to be set whenever (r_busy) and (r_bit == -1),
220
        // hence we need to set on (r_busy) and (r_bit == -2) so as to be set
221 205 dgisselq
        // when (r_bit == 0).
222 160 dgisselq
        initial last_bit = 1'b0;
223 69 dgisselq
        always @(posedge i_clk)
224 209 dgisselq
        if (i_reset)
225
                last_bit <= 1'b0;
226
        else if (r_busy)
227
                last_bit <= (r_bit == {(LGBW){1'b1}}-1'b1);
228
        else
229
                last_bit <= 1'b0;
230 160 dgisselq
 
231 205 dgisselq
        // pre_sign
232
        //
233
        // This is part of the state machine.  pre_sign indicates that we need
234
        // a extra clock to take the absolute value of our inputs.  It need only
235
        // be true for the one clock, and then it must clear itself.
236
        initial pre_sign = 1'b0;
237 160 dgisselq
        always @(posedge i_clk)
238 209 dgisselq
        if (i_reset)
239
                pre_sign <= 1'b0;
240
        else
241
                pre_sign <= (i_wr)&&(i_signed)&&((i_numerator[BW-1])||(i_denominator[BW-1]));
242 205 dgisselq
 
243
        // As a result of our operation, we need to set the flags.  The most
244
        // difficult of these is the "Z" flag indicating that the result is
245
        // zero.  Here, we'll use the same logic that sets the low-order
246
        // bit to clear our zero flag, and leave the zero flag set in all
247 209 dgisselq
        // other cases.
248 205 dgisselq
        always @(posedge i_clk)
249 209 dgisselq
        if (i_wr)
250
                r_z <= 1'b1;
251
        else if ((r_busy)&&(!pre_sign)&&(!diff[BW]))
252
                r_z <= 1'b0;
253 205 dgisselq
 
254
        // r_dividend
255
        // This is initially the numerator.  On a signed divide, it then becomes
256
        // the absolute value of the numerator.  We'll subtract from this value
257 209 dgisselq
        // the divisor for every output bit we are looking for--just as with
258
        // traditional long division.
259 205 dgisselq
        always @(posedge i_clk)
260 209 dgisselq
        if (pre_sign)
261
        begin
262
                // If we are doing a signed divide, then take the
263
                // absolute value of the dividend
264
                if (r_dividend[BW-1])
265 69 dgisselq
                begin
266 209 dgisselq
                        r_dividend[2*BW-2:0] <= {(2*BW-1){1'b1}};
267
                        r_dividend[BW-1:0] <= -r_dividend[BW-1:0];
268
                end
269
        end else if (r_busy)
270
        begin
271
                r_dividend <= { r_dividend[2*BW-3:0], 1'b0 };
272
                if (!diff[BW])
273
                        r_dividend[2*BW-2:BW] <= diff[(BW-2):0];
274
        end else if (!r_busy)
275
                // Once we are done, and r_busy is no longer high, we'll
276
                // always accept new values into our dividend.  This
277
                // guarantees that, when i_wr is set, the new value
278
                // is already set as desired.
279
                r_dividend <=  { 31'h0, i_numerator };
280 205 dgisselq
 
281
        initial r_divisor = 0;
282
        always @(posedge i_clk)
283 209 dgisselq
        if (i_reset)
284
                r_divisor <= 0;
285
        else if ((pre_sign)&&(r_busy))
286
        begin
287
                if (r_divisor[BW-1])
288
                        r_divisor <= -r_divisor;
289
        end else if (!r_busy)
290
                r_divisor <= i_denominator;
291 205 dgisselq
 
292
        // r_sign
293
        // is a flag for our state machine control(s).  r_sign will be set to
294
        // true any time we are doing a signed divide and the result must be
295
        // negative.  In that case, we take a final logic stage at the end of
296
        // the divide to negate the output.  This flag is what tells us we need
297
        // to do that.  r_busy will be true during the divide, then when r_busy
298
        // goes low, r_sign will be checked, then the idle/reset stage will have
299
        // been reached.  For this reason, we cannot set r_sign unless we are
300
        // up to something.
301
        initial r_sign = 1'b0;
302
        always @(posedge i_clk)
303 209 dgisselq
        if (i_reset)
304
                r_sign <= 1'b0;
305
        else if (pre_sign)
306
                r_sign <= ((r_divisor[(BW-1)])^(r_dividend[(BW-1)]));
307
        else if (r_busy)
308
                r_sign <= (r_sign)&&(!zero_divisor);
309
        else
310
                r_sign <= 1'b0;
311 205 dgisselq
 
312 209 dgisselq
        initial o_quotient = 0;
313 205 dgisselq
        always @(posedge i_clk)
314 209 dgisselq
        if (i_reset)
315
                o_quotient <= 0;
316
        else if (r_busy)
317
        begin
318
                o_quotient <= { o_quotient[(BW-2):0], 1'b0 };
319
                if (!diff[BW])
320
                        o_quotient[0] <= 1'b1;
321
        end else if (r_sign)
322
                o_quotient <= -o_quotient;
323
        else
324
                o_quotient <= 0;
325 69 dgisselq
 
326
        // Set Carry on an exact divide
327 205 dgisselq
        // Perhaps nothing uses this, but ... well, I suppose we could remove
328
        // this logic eventually, just ... not yet.
329 209 dgisselq
        initial r_c = 1'b0;
330 69 dgisselq
        always @(posedge i_clk)
331 209 dgisselq
        if (i_reset)
332
                r_c <= 1'b0;
333
        else
334
                r_c <= (r_busy)&&(diff == 0);
335 205 dgisselq
 
336
        // The last flag: Negative.  This flag is set assuming that the result
337
        // of the divide was negative (i.e., the high order bit is set).  This
338
        // will also be true of an unsigned divide--if the high order bit is
339
        // ever set upon completion.  Indeed, you might argue that there's no
340
        // logic involved.
341
        wire    w_n;
342 69 dgisselq
        assign w_n = o_quotient[(BW-1)];
343
 
344
        assign o_flags = { 1'b0, w_n, r_c, r_z };
345 209 dgisselq
 
346
`ifdef  FORMAL
347
        reg     f_past_valid;
348
        initial f_past_valid = 0;
349
        always @(posedge i_clk)
350
                f_past_valid <= 1'b1;
351
 
352
`ifdef  DIV
353
`define ASSUME  assume
354
`else
355
`define ASSUME  assert
356
`endif
357
 
358
        initial `ASSUME(i_reset);
359
        always @(*)
360
        if (!f_past_valid)
361
                `ASSUME(i_reset);
362
 
363
        always @(posedge i_clk)
364
        if ((!f_past_valid)||($past(i_reset)))
365
        begin
366
                assert(!o_busy);
367
                assert(!o_valid);
368
                assert(!o_err);
369
                //
370
                assert(!r_busy);
371
                // assert(!zero_divisor);
372
                assert(r_bit==0);
373
                assert(!last_bit);
374
                assert(!pre_sign);
375
                // assert(!r_z);
376
                // assert(r_dividend==0);
377
                assert(o_quotient==0);
378
                assert(!r_c);
379
                assert(r_divisor==0);
380
 
381
                `ASSUME(!i_wr);
382
        end
383
 
384
        always @(*)
385
        if (o_busy)
386
                `ASSUME(!i_wr);
387
 
388
        always @(posedge i_clk)
389
        if ((f_past_valid)&&(!$past(i_reset))&&($past(o_busy))&&(!o_busy))
390
        begin
391
                assert(o_valid);
392
        end
393
 
394
        // A formal methods section
395
        //
396
        // This section isn't yet complete.  For now, it is just
397
        // a description of things I think should be in here ... not
398
        // yet a description of what it would take to prove
399
        // this divide (yet).
400
        always @(*)
401
        if (o_err)
402
                assert(o_valid);
403
 
404
        always @(posedge i_clk)
405
        if ((f_past_valid)&&(!$past(i_wr)))
406
                assert(!pre_sign);
407
        always @(posedge i_clk)
408
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr))&&($past(i_signed))
409
                        &&(|$past({i_numerator[BW-1],i_denominator[BW-1]})))
410
                assert(pre_sign);
411
 
412
        // always @(posedge i_clk)
413
        // if ((f_past_valid)&&(!$past(pre_sign)))
414
                // assert(!r_sign);
415
        reg     [BW:0]   f_bits_set;
416
 
417
        always @(posedge i_clk)
418
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr)))
419
                assert(o_busy);
420
 
421
        always @(posedge i_clk)
422
        if ((f_past_valid)&&($past(o_valid)))
423
                assert(!o_valid);
424
 
425
        always @(*)
426
        if ((o_valid)&&(!o_err))
427
                assert(r_z == ((o_quotient == 0)? 1'b1:1'b0));
428
        else if (o_busy)
429
                assert(r_z == (((o_quotient&f_bits_set[BW-1:0]) == 0)? 1'b1: 1'b0));
430
 
431
        always @(*)
432
        if ((o_valid)&&(!o_err))
433
                assert(w_n == o_quotient[BW-1]);
434
 
435
        always @(posedge i_clk)
436
        if ((f_past_valid)&&(!$past(r_busy))&&(!$past(i_wr)))
437
                assert(!o_busy);
438
        always @(posedge i_clk)
439
                assert((!o_busy)||(!o_valid));
440
 
441
        always @(*)
442
        if(r_busy)
443
                assert(o_busy);
444
 
445
        always @(posedge i_clk)
446
        if (i_reset)
447
                f_bits_set <= 0;
448
        else if (i_wr)
449
                f_bits_set <= 0;
450
        else if ((r_busy)&&(!pre_sign))
451
                f_bits_set <= { f_bits_set[BW-1:0], 1'b1 };
452
 
453
        always @(posedge i_clk)
454
        if (r_busy)
455
                assert(((1<<r_bit)-1) == f_bits_set);
456
 
457
        always @(*)
458
        if ((o_valid)&&(!o_err))
459
                assert((!f_bits_set[BW])&&(&f_bits_set[BW-1:0]));
460
 
461
 
462
        /*
463
        always @(posedge i_clk)
464
        if ((f_past_valid)&&(!$past(i_reset))&&($past(r_busy))
465
                &&($past(r_divisor[2*BW-2:BW])==0))
466
        begin
467
                if ($past(r_divisor) == 0)
468
                        assert(o_err);
469
                else if ($past(pre_sign))
470
                begin
471
                        if ($past(r_dividend[BW-1]))
472
                                assert(r_dividend == -$past(r_dividend));
473
                        if ($past(r_divisor[(2*BW-2)]))
474
                        begin
475
                                assert(r_divisor[(2*BW-2):(BW-1)]
476
                                        == -$past(r_divisor[(2*BW-2):(BW-1)]));
477
                                assert(r_divisor[BW-2:0] == 0);
478
                        end
479
                end else begin
480
                        if (o_quotient[0])
481
                                assert(r_dividend == $past(diff));
482
                        else
483
                                assert(r_dividend == $past(r_dividend));
484
 
485
                        // r_divisor should shift down on every step
486
                        assert(r_divisor[2*BW-2]==0);
487
                        assert(r_divisor[2*BW-3:0]==$past(r_divisor[2*BW-2:1]));
488
                end
489
                if ($past(r_dividend) >= $past(r_divisor[BW-1:0]))
490
                        assert(o_quotient[0]);
491
                else
492
                        assert(!o_quotient[0]);
493
        end
494
        */
495
 
496
        always @(*)
497
        if (r_busy)
498
                assert((f_bits_set & r_dividend[BW-1:0])==0);
499
 
500
        always @(*)
501
        if (r_busy)
502
                assert((r_divisor == 0) == zero_divisor);
503
 
504
`ifdef  VERIFIC
505
        // Verify unsigned division
506
        assert property (@(posedge i_clk)
507
                disable iff (i_reset)
508
                (i_wr)&&(i_denominator != 0)&&(!i_signed)
509
                |=> ((!o_err)&&(!o_valid)&&(o_busy)&&(!r_sign)&&(!pre_sign)
510
                                throughout (r_bit == 0)
511
                        ##1 ((r_bit == $past(r_bit)+1)&&({1'b0,r_bit}< BW-1))
512
                                        [*0:$]
513
                        ##1 ({ 1'b0, r_bit } == BW-1))
514
                        ##1 (!o_err)&&(o_valid));
515
 
516
        // Verify division by zero
517
        assert property (@(posedge i_clk)
518
                disable iff (i_reset)
519
                (i_wr)&&(i_denominator == 0)
520
                |=> (zero_divisor throughout
521
                        (!o_err)&&(!o_valid)&&(pre_sign) [*0:1]
522
                        ##1 ((r_busy)&&(!o_err)&&(!o_valid))
523
                        ##1 ((o_err)&&(o_valid))));
524
 
525
 
526
`endif  // VERIFIC
527
`endif
528 69 dgisselq
endmodule
529 209 dgisselq
//
530
// How much logic will this divide use, now that it's been updated to
531
// a different (long division) algorithm?
532
//
533
// iCE40 stats                  (Updated)       (Original)
534
//   Number of cells:                700        820
535
//     SB_CARRY                      125        125
536
//     SB_DFF                          1          
537
//     SB_DFFE                        33          1
538
//     SB_DFFESR                      37
539
//     SB_DFFESS                      31
540
//     SB_DFFSR                       40         40
541
//     SB_LUT4                       433        553
542
// 
543
// Xilinx stats                 (Updated)       (Original)
544
//   Number of cells:                758        831
545
//     FDRE                          142        142
546
//     LUT1                           97         97
547
//     LUT2                           69        174
548
//     LUT3                            6          5
549
//     LUT4                            1          6
550
//     LUT5                           68         35
551
//     LUT6                           94         98
552
//     MUXCY                         129        129
553
//     MUXF7                          12          8
554
//     MUXF8                           6          3
555
//     XORCY                         134        134
556
 

powered by: WebSVN 2.1.0

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