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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [bench/] [formal/] [abs_div.v] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 209 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    abs_div.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     The original divide module provides an Integer divide
8
//              capability to the Zip CPU.  This module is an abstract
9
//      divide module.  It *might* produce a valid integer divide, either signed
10
//      or unsigned, result.  It might instead do somethin else.  It is designed
11
//      to be easier for the formal tools to work with.
12
//
13
// Steps:
14
//      i_reset The DIVide unit starts in idle.  It can also be placed into an
15
//      idle by asserting the reset input.
16
//
17
//      i_wr    When i_reset is asserted, a divide begins.  On the next clock:
18
//
19
//        o_busy is set high so everyone else knows we are at work and they can
20
//              wait for us to complete.
21
//
22
//        pre_sign is set to true if we need to do a signed divide.  In this
23
//              case, we take a clock cycle to turn the divide into an unsigned
24
//              divide.
25
//
26
//        o_quotient, a place to store our result, is initialized to all zeros.
27
//
28
//        r_dividend is set to the numerator
29
//
30
//        r_divisor is set to 2^31 * the denominator (shift left by 31, or add
31
//              31 zeros to the right of the number.
32
//
33
//      pre_sign When true (clock cycle after i_wr), a clock cycle is used
34
//              to take the absolute value of the various arguments (r_dividend
35
//              and r_divisor), and to calculate what sign the output result
36
//              should be.
37
//
38
//
39
//      At this point, the divide is has started.  The divide works by walking
40
//      through every shift of the
41
//
42
//                  DIVIDEND    over the
43
//              DIVISOR
44
//
45
//      If the DIVISOR is bigger than the dividend, the divisor is shifted
46
//      right, and nothing is done to the output quotient.
47
//
48
//                  DIVIDEND
49
//               DIVISOR
50
//
51
//      This repeats, until DIVISOR is less than or equal to the divident, as in
52
//
53
//              DIVIDEND
54
//              DIVISOR
55
//
56
//      At this point, if the DIVISOR is less than the dividend, the
57
//      divisor is subtracted from the dividend, and the DIVISOR is again
58
//      shifted to the right.  Further, a '1' bit gets set in the output
59
//      quotient.
60
//
61
//      Once we've done this for 32 clocks, we've accumulated our answer into
62
//      the output quotient, and we can proceed to the next step.  If the
63
//      result will be signed, the next step negates the quotient, otherwise
64
//      it returns the result.
65
//
66
//      On the clock when we are done, o_busy is set to false, and o_valid set
67
//      to true.  (It is a violation of the ZipCPU internal protocol for both
68
//      busy and valid to ever be true on the same clock.  It is also a
69
//      violation for busy to be false with valid true thereafter.)
70
//
71
//
72
// Creator:     Dan Gisselquist, Ph.D.
73
//              Gisselquist Technology, LLC
74
//
75
////////////////////////////////////////////////////////////////////////////////
76
//
77
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
78
//
79
// This program is free software (firmware): you can redistribute it and/or
80
// modify it under the terms of  the GNU General Public License as published
81
// by the Free Software Foundation, either version 3 of the License, or (at
82
// your option) any later version.
83
//
84
// This program is distributed in the hope that it will be useful, but WITHOUT
85
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
86
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
87
// for more details.
88
//
89
// You should have received a copy of the GNU General Public License along
90
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
91
// target there if the PDF file isn't present.)  If not, see
92
// <http://www.gnu.org/licenses/> for a copy.
93
//
94
// License:     GPL, v3, as defined and found on www.gnu.org,
95
//              http://www.gnu.org/licenses/gpl.html
96
//
97
//
98
////////////////////////////////////////////////////////////////////////////////
99
//
100
//
101
`default_nettype        none
102
//
103
module  abs_div(i_clk, i_reset, i_wr, i_signed, i_numerator, i_denominator,
104
                o_busy, o_valid, o_err, o_quotient, o_flags);
105
        parameter               BW=32, LGBW = 5;
106
        parameter       [4:0]    MAXDELAY = 3;
107
        input   wire            i_clk, i_reset;
108
        // Input parameters
109
        input   wire            i_wr, i_signed;
110
        input   wire [(BW-1):0]  i_numerator, i_denominator;
111
        // Output parameters
112
        output  wire            o_busy;
113
        output  reg             o_valid, o_err;
114
        output  reg [(BW-1):0]   o_quotient;
115
        output  wire    [3:0]    o_flags;
116
 
117
        (* anyseq *)    reg                     any_err;
118
        (* anyseq *)    reg     [(BW-1):0]       any_quotient;
119
        (* anyseq *)    reg     [5:0]            wait_time;
120
 
121
        always @(*)
122
                o_err      = any_err;
123
        always @(*)
124
                o_quotient = any_quotient;
125
 
126
        reg     [5:0]    r_busy_counter;
127
 
128
        always @(*)
129
                assume(wait_time > 5'h1);
130
 
131
        always @(*)
132
                assume((MAXDELAY == 0)||(wait_time < MAXDELAY));
133
 
134
        initial r_busy_counter = 0;
135
        always @(posedge i_clk)
136
        if (i_reset)
137
                r_busy_counter <= 0;
138
        else if ((i_wr)&&(!o_busy))
139
                r_busy_counter <= wait_time;
140
        else if (r_busy_counter > 0)
141
                r_busy_counter <= r_busy_counter - 1'b1;
142
 
143
        always @(*)
144
        assert((MAXDELAY == 0)||(r_busy_counter < MAXDELAY));
145
 
146
        assign  o_busy = (r_busy_counter != 0);
147
 
148
        initial o_valid = 1'b0;
149
        always @(posedge i_clk)
150
        if (i_reset)
151
                o_valid <= 1'b0;
152
        else
153
                o_valid <= (r_busy_counter == 1);
154
 
155
        (* anyseq *)    reg     [3:0]    any_flags;
156
 
157
        assign o_flags    = (o_valid) ?
158
                        { 1'b0, o_quotient[31], any_flags[1],
159
                                        (o_quotient == 0) } : any_flags;
160
 
161
`ifdef  FORMAL
162
        reg     f_past_valid;
163
        initial f_past_valid = 0;
164
        always @(posedge i_clk)
165
                f_past_valid <= 1'b1;
166
        always @(posedge i_clk)
167
        if (!f_past_valid)
168
                assert((!o_busy)&&(!o_valid));
169
 
170
`define ASSUME  assert
171
 
172
        initial `ASSUME(i_reset);
173
        always @(*)
174
        if (!f_past_valid)
175
                `ASSUME(i_reset);
176
 
177
        always @(posedge i_clk)
178
        if ((!f_past_valid)||($past(i_reset)))
179
                `ASSUME(!i_wr);
180
 
181
        always @(*)
182
        if (o_busy)
183
                `ASSUME(!i_wr);
184
 
185
        always @(posedge i_clk)
186
        if ((f_past_valid)&&(!$past(i_reset))&&($past(o_busy))&&(!o_busy))
187
                assume(o_valid);
188
 
189
        always @(*)
190
        if (o_err)
191
                assume(o_valid);
192
 
193
        always @(posedge i_clk)
194
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr)))
195
                assert(o_busy);
196
 
197
        always @(posedge i_clk)
198
        if ((f_past_valid)&&($past(o_valid)))
199
                assume(!o_valid);
200
 
201
        always @(*)
202
        if ((o_valid)&&(!o_err))
203
                assume(o_flags[3] == ((o_quotient == 0)? 1'b1:1'b0));
204
 
205
        always @(*)
206
        if ((o_valid)&&(!o_err))
207
                assume(o_flags[1] == o_quotient[BW-1]);
208
 
209
        always @(posedge i_clk)
210
        if ((f_past_valid)&&(!$past(o_busy))&&(!$past(i_wr)))
211
                assume(!o_busy);
212
 
213
        always @(posedge i_clk)
214
                assume((!o_busy)||(!o_valid));
215
 
216
`endif
217
endmodule

powered by: WebSVN 2.1.0

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