1 |
36 |
dgisselq |
////////////////////////////////////////////////////////////////////////////////
|
2 |
|
|
//
|
3 |
|
|
// Filename: softmpy.cpp
|
4 |
|
|
//
|
5 |
|
|
// Project: A General Purpose Pipelined FFT Implementation
|
6 |
|
|
//
|
7 |
|
|
// Purpose: If the chip doesn't have any hardware multiplies, you'll need
|
8 |
|
|
// a soft-multiply implementation. This provides that
|
9 |
|
|
// implementation.
|
10 |
|
|
//
|
11 |
|
|
// Creator: Dan Gisselquist, Ph.D.
|
12 |
|
|
// Gisselquist Technology, LLC
|
13 |
|
|
//
|
14 |
|
|
////////////////////////////////////////////////////////////////////////////////
|
15 |
|
|
//
|
16 |
|
|
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
|
17 |
|
|
//
|
18 |
|
|
// This program is free software (firmware): you can redistribute it and/or
|
19 |
|
|
// modify it under the terms of the GNU General Public License as published
|
20 |
|
|
// by the Free Software Foundation, either version 3 of the License, or (at
|
21 |
|
|
// your option) any later version.
|
22 |
|
|
//
|
23 |
|
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
24 |
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
25 |
|
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
26 |
|
|
// for more details.
|
27 |
|
|
//
|
28 |
|
|
// You should have received a copy of the GNU General Public License along
|
29 |
37 |
dgisselq |
// with this program. (It's in the $(ROOT)/doc directory. Run make with no
|
30 |
36 |
dgisselq |
// target there if the PDF file isn't present.) If not, see
|
31 |
|
|
// <http://www.gnu.org/licenses/> for a copy.
|
32 |
|
|
//
|
33 |
|
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
34 |
|
|
// http://www.gnu.org/licenses/gpl.html
|
35 |
|
|
//
|
36 |
|
|
//
|
37 |
|
|
////////////////////////////////////////////////////////////////////////////////
|
38 |
|
|
//
|
39 |
|
|
//
|
40 |
|
|
#define _CRT_SECURE_NO_WARNINGS // ms vs 2012 doesn't like fopen
|
41 |
|
|
#include <stdio.h>
|
42 |
|
|
#include <stdlib.h>
|
43 |
|
|
|
44 |
|
|
#ifdef _MSC_VER // added for ms vs compatibility
|
45 |
|
|
|
46 |
|
|
#include <io.h>
|
47 |
|
|
#include <direct.h>
|
48 |
|
|
#define _USE_MATH_DEFINES
|
49 |
|
|
|
50 |
|
|
#endif
|
51 |
|
|
|
52 |
|
|
#include <string.h>
|
53 |
|
|
#include <string>
|
54 |
|
|
#include <math.h>
|
55 |
|
|
#include <ctype.h>
|
56 |
|
|
#include <assert.h>
|
57 |
|
|
|
58 |
|
|
#include "defaults.h"
|
59 |
|
|
#include "legal.h"
|
60 |
|
|
#include "softmpy.h"
|
61 |
|
|
|
62 |
|
|
void build_multiply(const char *fname) {
|
63 |
|
|
FILE *fp = fopen(fname, "w");
|
64 |
|
|
if (NULL == fp) {
|
65 |
|
|
fprintf(stderr, "Could not open \'%s\' for writing\n", fname);
|
66 |
|
|
perror("O/S Err was:");
|
67 |
|
|
return;
|
68 |
|
|
}
|
69 |
|
|
|
70 |
|
|
fprintf(fp,
|
71 |
|
|
SLASHLINE
|
72 |
|
|
"//\n"
|
73 |
|
|
"// Filename:\tshiftaddmpy.v\n"
|
74 |
|
|
"//\n"
|
75 |
|
|
"// Project:\t%s\n"
|
76 |
|
|
"//\n"
|
77 |
|
|
"// Purpose:\tA portable shift and add multiply.\n"
|
78 |
|
|
"//\n"
|
79 |
|
|
"// While both Xilinx and Altera will offer single clock multiplies, this\n"
|
80 |
|
|
"// simple approach will multiply two numbers on any architecture. The\n"
|
81 |
|
|
"// result maintains the full width of the multiply, there are no extra\n"
|
82 |
|
|
"// stuff bits, no rounding, no shifted bits, etc.\n"
|
83 |
|
|
"//\n"
|
84 |
|
|
"// Further, for those applications that can support it, this multiply\n"
|
85 |
|
|
"// is pipelined and will produce one answer per clock.\n"
|
86 |
|
|
"//\n"
|
87 |
|
|
"// For minimal processing delay, make the first parameter the one with\n"
|
88 |
|
|
"// the least bits, so that AWIDTH <= BWIDTH.\n"
|
89 |
|
|
"//\n"
|
90 |
|
|
"// The processing delay in this multiply is (AWIDTH+1) cycles. That is,\n"
|
91 |
|
|
"// if the data is present on the input at clock t=0, the result will be\n"
|
92 |
|
|
"// present on the output at time t=AWIDTH+1;\n"
|
93 |
|
|
"//\n"
|
94 |
|
|
"//\n%s"
|
95 |
|
|
"//\n", prjname, creator);
|
96 |
|
|
|
97 |
|
|
fprintf(fp, "%s", cpyleft);
|
98 |
|
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
99 |
|
|
fprintf(fp,
|
100 |
|
|
"module shiftaddmpy(i_clk, i_ce, i_a, i_b, o_r);\n"
|
101 |
|
|
"\tparameter\tAWIDTH=%d,BWIDTH=", TST_SHIFTADDMPY_AW);
|
102 |
|
|
#ifdef TST_SHIFTADDMPY_BW
|
103 |
|
|
fprintf(fp, "%d;\n", TST_SHIFTADDMPY_BW);
|
104 |
|
|
#else
|
105 |
|
|
fprintf(fp, "AWIDTH;\n");
|
106 |
|
|
#endif
|
107 |
|
|
fprintf(fp,
|
108 |
37 |
dgisselq |
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
|
109 |
|
|
"\tinput\twire\t[(AWIDTH-1):0]\t\ti_a;\n"
|
110 |
|
|
"\tinput\twire\t[(BWIDTH-1):0]\t\ti_b;\n"
|
111 |
36 |
dgisselq |
"\toutput\treg\t[(AWIDTH+BWIDTH-1):0]\to_r;\n"
|
112 |
|
|
"\n"
|
113 |
|
|
"\treg\t[(AWIDTH-1):0]\tu_a;\n"
|
114 |
|
|
"\treg\t[(BWIDTH-1):0]\tu_b;\n"
|
115 |
|
|
"\treg\t\t\tsgn;\n"
|
116 |
|
|
"\n"
|
117 |
|
|
"\treg\t[(AWIDTH-2):0]\t\tr_a[0:(AWIDTH-1)];\n"
|
118 |
|
|
"\treg\t[(AWIDTH+BWIDTH-2):0]\tr_b[0:(AWIDTH-1)];\n"
|
119 |
|
|
"\treg\t\t\t\tr_s[0:(AWIDTH-1)];\n"
|
120 |
|
|
"\treg\t[(AWIDTH+BWIDTH-1):0]\tacc[0:(AWIDTH-1)];\n"
|
121 |
|
|
"\tgenvar k;\n"
|
122 |
|
|
"\n"
|
123 |
|
|
"\t// If we were forced to stay within two\'s complement arithmetic,\n"
|
124 |
|
|
"\t// taking the absolute value here would require an additional bit.\n"
|
125 |
|
|
"\t// However, because our results are now unsigned, we can stay\n"
|
126 |
|
|
"\t// within the number of bits given (for now).\n"
|
127 |
|
|
"\talways @(posedge i_clk)\n"
|
128 |
|
|
"\t\tif (i_ce)\n"
|
129 |
|
|
"\t\tbegin\n"
|
130 |
|
|
"\t\t\tu_a <= (i_a[AWIDTH-1])?(-i_a):(i_a);\n"
|
131 |
|
|
"\t\t\tu_b <= (i_b[BWIDTH-1])?(-i_b):(i_b);\n"
|
132 |
|
|
"\t\t\tsgn <= i_a[AWIDTH-1] ^ i_b[BWIDTH-1];\n"
|
133 |
|
|
"\t\tend\n"
|
134 |
|
|
"\n"
|
135 |
|
|
"\talways @(posedge i_clk)\n"
|
136 |
|
|
"\t\tif (i_ce)\n"
|
137 |
|
|
"\t\tbegin\n"
|
138 |
|
|
"\t\t\tacc[0] <= (u_a[0]) ? { {(AWIDTH){1\'b0}}, u_b }\n"
|
139 |
|
|
"\t\t\t\t\t: {(AWIDTH+BWIDTH){1\'b0}};\n"
|
140 |
|
|
"\t\t\tr_a[0] <= { u_a[(AWIDTH-1):1] };\n"
|
141 |
|
|
"\t\t\tr_b[0] <= { {(AWIDTH-1){1\'b0}}, u_b };\n"
|
142 |
|
|
"\t\t\tr_s[0] <= sgn; // The final sign, needs to be preserved\n"
|
143 |
|
|
"\t\tend\n"
|
144 |
|
|
"\n"
|
145 |
|
|
"\tgenerate\n"
|
146 |
|
|
"\tfor(k=0; k<AWIDTH-1; k=k+1)\n"
|
147 |
|
|
"\tbegin : genstages\n"
|
148 |
|
|
"\t\talways @(posedge i_clk)\n"
|
149 |
|
|
"\t\tif (i_ce)\n"
|
150 |
|
|
"\t\tbegin\n"
|
151 |
|
|
"\t\t\tacc[k+1] <= acc[k] + ((r_a[k][0]) ? {r_b[k],1\'b0}:0);\n"
|
152 |
|
|
"\t\t\tr_a[k+1] <= { 1\'b0, r_a[k][(AWIDTH-2):1] };\n"
|
153 |
|
|
"\t\t\tr_b[k+1] <= { r_b[k][(AWIDTH+BWIDTH-3):0], 1\'b0};\n"
|
154 |
|
|
"\t\t\tr_s[k+1] <= r_s[k];\n"
|
155 |
|
|
"\t\tend\n"
|
156 |
|
|
"\tend\n"
|
157 |
|
|
"\tendgenerate\n"
|
158 |
|
|
"\n"
|
159 |
|
|
"\talways @(posedge i_clk)\n"
|
160 |
|
|
"\t\tif (i_ce)\n"
|
161 |
|
|
"\t\t\to_r <= (r_s[AWIDTH-1]) ? (-acc[AWIDTH-1]) : acc[AWIDTH-1];\n"
|
162 |
|
|
"\n"
|
163 |
|
|
"endmodule\n");
|
164 |
|
|
|
165 |
|
|
fclose(fp);
|
166 |
|
|
}
|
167 |
|
|
|
168 |
|
|
void build_bimpy(const char *fname) {
|
169 |
|
|
FILE *fp = fopen(fname, "w");
|
170 |
|
|
if (NULL == fp) {
|
171 |
|
|
fprintf(stderr, "Could not open \'%s\' for writing\n", fname);
|
172 |
|
|
perror("O/S Err was:");
|
173 |
|
|
return;
|
174 |
|
|
}
|
175 |
|
|
|
176 |
|
|
fprintf(fp,
|
177 |
|
|
SLASHLINE
|
178 |
|
|
"//\n"
|
179 |
|
|
"// Filename:\t%s\n"
|
180 |
|
|
"//\n"
|
181 |
|
|
"// Project:\t%s\n"
|
182 |
|
|
"//\n"
|
183 |
|
|
"// Purpose:\tA simple 2-bit multiply based upon the fact that LUT's allow\n"
|
184 |
|
|
"// 6-bits of input. In other words, I could build a 3-bit\n"
|
185 |
|
|
"// multiply from 6 LUTs (5 actually, since the first could have two\n"
|
186 |
|
|
"// outputs). This would allow multiplication of three bit digits, save\n"
|
187 |
|
|
"// only for the fact that you would need two bits of carry. The bimpy\n"
|
188 |
|
|
"// approach throttles back a bit and does a 2x2 bit multiply in a LUT,\n"
|
189 |
|
|
"// guaranteeing that it will never carry more than one bit. While this\n"
|
190 |
|
|
"// multiply is hardware independent (and can still run under Verilator\n"
|
191 |
|
|
"// therefore), it is really motivated by trying to optimize for a\n"
|
192 |
|
|
"// specific piece of hardware (Xilinx-7 series ...) that has at least\n"
|
193 |
|
|
"// 4-input LUT's with carry chains.\n"
|
194 |
|
|
"//\n"
|
195 |
|
|
"//\n"
|
196 |
|
|
"//\n%s"
|
197 |
|
|
"//\n", fname, prjname, creator);
|
198 |
|
|
|
199 |
|
|
fprintf(fp, "%s", cpyleft);
|
200 |
|
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
201 |
|
|
fprintf(fp,
|
202 |
|
|
"module bimpy(i_clk, i_ce, i_a, i_b, o_r);\n"
|
203 |
37 |
dgisselq |
"\tparameter\tBW=18; // Number of bits in i_b\n"
|
204 |
|
|
"\tlocalparam\tLUTB=2; // Number of bits in i_a for our LUT multiply\n"
|
205 |
|
|
"\tinput\twire\t\t\ti_clk, i_ce;\n"
|
206 |
|
|
"\tinput\twire\t[(LUTB-1):0]\ti_a;\n"
|
207 |
|
|
"\tinput\twire\t[(BW-1):0]\ti_b;\n"
|
208 |
36 |
dgisselq |
"\toutput\treg\t[(BW+LUTB-1):0] o_r;\n"
|
209 |
|
|
"\n"
|
210 |
|
|
"\twire [(BW+LUTB-2):0] w_r;\n"
|
211 |
|
|
"\twire [(BW+LUTB-3):1] c;\n"
|
212 |
|
|
"\n"
|
213 |
|
|
"\tassign\tw_r = { ((i_a[1])?i_b:{(BW){1\'b0}}), 1\'b0 }\n"
|
214 |
|
|
"\t\t\t\t^ { 1\'b0, ((i_a[0])?i_b:{(BW){1\'b0}}) };\n"
|
215 |
|
|
"\tassign\tc = { ((i_a[1])?i_b[(BW-2):0]:{(BW-1){1\'b0}}) }\n"
|
216 |
|
|
"\t\t\t& ((i_a[0])?i_b[(BW-1):1]:{(BW-1){1\'b0}});\n"
|
217 |
|
|
"\n"
|
218 |
37 |
dgisselq |
"\tinitial o_r = 0;\n"
|
219 |
36 |
dgisselq |
"\talways @(posedge i_clk)\n"
|
220 |
37 |
dgisselq |
"\tif (i_ce)\n"
|
221 |
|
|
"\t\to_r <= w_r + { c, 2'b0 };\n"
|
222 |
|
|
"\n");
|
223 |
|
|
|
224 |
|
|
// Formal properties
|
225 |
|
|
//
|
226 |
|
|
// This module is formally verified as part of longbimpy.v
|
227 |
|
|
// Hence, we'll use an ifdef LONGBIMPY to capture if it is being verified as part of
|
228 |
|
|
// LONGBIMPY, or placed within another module.
|
229 |
|
|
fprintf(fp,
|
230 |
|
|
"`ifdef FORMAL\n");
|
231 |
|
|
|
232 |
|
|
if (formal_property_flag) {
|
233 |
|
|
fprintf(fp,
|
234 |
|
|
"\treg\tf_past_valid;\n"
|
235 |
36 |
dgisselq |
"\n"
|
236 |
37 |
dgisselq |
"\tinitial\tf_past_valid = 1'b0;\n"
|
237 |
|
|
"\talways @(posedge i_clk)\n"
|
238 |
|
|
"\tf_past_valid <= 1'b1;\n"
|
239 |
|
|
"\n"
|
240 |
|
|
"`define\tASSERT\tassert\n"
|
241 |
|
|
"\n");
|
242 |
|
|
|
243 |
|
|
// Now for our module specific assertions
|
244 |
|
|
// These properties will be assumed if this proof is not part of LONGBIMPY's proof
|
245 |
|
|
fprintf(fp,
|
246 |
|
|
"\talways @(posedge i_clk)\n"
|
247 |
|
|
"\tif ((f_past_valid)&&($past(i_ce)))\n"
|
248 |
|
|
"\tbegin\n"
|
249 |
|
|
"\t\tif ($past(i_a)==0)\n"
|
250 |
|
|
"\t\t\t`ASSERT(o_r == 0);\n"
|
251 |
|
|
"\t\telse if ($past(i_a) == 1)\n"
|
252 |
|
|
"\t\t\t`ASSERT(o_r == $past(i_b));\n"
|
253 |
|
|
"\n"
|
254 |
|
|
"\t\tif ($past(i_b)==0)\n"
|
255 |
|
|
"\t\t\t`ASSERT(o_r == 0);\n"
|
256 |
|
|
"\t\telse if ($past(i_b) == 1)\n"
|
257 |
|
|
"\t\t\t`ASSERT(o_r[(LUTB-1):0] == $past(i_a));\n"
|
258 |
|
|
"\tend\n");
|
259 |
|
|
|
260 |
|
|
} else {
|
261 |
|
|
fprintf(fp, "// Enable the formal_property_flag to include formal properties\n");
|
262 |
|
|
}
|
263 |
|
|
|
264 |
|
|
fprintf(fp,
|
265 |
|
|
"`endif\n");
|
266 |
|
|
// And then the end of the module
|
267 |
|
|
fprintf(fp,
|
268 |
36 |
dgisselq |
"endmodule\n");
|
269 |
|
|
|
270 |
|
|
fclose(fp);
|
271 |
|
|
}
|
272 |
|
|
|
273 |
|
|
void build_longbimpy(const char *fname) {
|
274 |
|
|
FILE *fp = fopen(fname, "w");
|
275 |
|
|
if (NULL == fp) {
|
276 |
|
|
fprintf(stderr, "Could not open \'%s\' for writing\n", fname);
|
277 |
|
|
perror("O/S Err was:");
|
278 |
|
|
return;
|
279 |
|
|
}
|
280 |
|
|
|
281 |
|
|
fprintf(fp,
|
282 |
|
|
SLASHLINE
|
283 |
|
|
"//\n"
|
284 |
|
|
"// Filename: %s\n"
|
285 |
|
|
"//\n"
|
286 |
|
|
"// Project: %s\n"
|
287 |
|
|
"//\n"
|
288 |
|
|
"// Purpose: A portable shift and add multiply, built with the knowledge\n"
|
289 |
|
|
"// of the existence of a six bit LUT and carry chain. That knowledge\n"
|
290 |
|
|
"// allows us to multiply two bits from one value at a time against all\n"
|
291 |
|
|
"// of the bits of the other value. This sub multiply is called the\n"
|
292 |
|
|
"// bimpy.\n"
|
293 |
|
|
"//\n"
|
294 |
|
|
"// For minimal processing delay, make the first parameter the one with\n"
|
295 |
|
|
"// the least bits, so that AWIDTH <= BWIDTH.\n"
|
296 |
|
|
"//\n"
|
297 |
|
|
"//\n"
|
298 |
|
|
"//\n%s"
|
299 |
|
|
"//\n", fname, prjname, creator);
|
300 |
|
|
|
301 |
|
|
fprintf(fp, "%s", cpyleft);
|
302 |
|
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
303 |
|
|
fprintf(fp,
|
304 |
37 |
dgisselq |
"module longbimpy(i_clk, i_ce, i_a_unsorted, i_b_unsorted, o_r\n");
|
305 |
|
|
|
306 |
|
|
if (formal_property_flag) fprintf(fp,
|
307 |
|
|
"`ifdef FORMAL\n"
|
308 |
|
|
"\t, f_past_a_unsorted, f_past_b_unsorted\n"
|
309 |
|
|
"`endif\n\t\t");
|
310 |
|
|
|
311 |
|
|
fprintf(fp, ");\n"
|
312 |
36 |
dgisselq |
"\tparameter IAW=%d, // The width of i_a, min width is 5\n"
|
313 |
|
|
"\t\t\tIBW=", TST_LONGBIMPY_AW);
|
314 |
|
|
#ifdef TST_LONGBIMPY_BW
|
315 |
|
|
fprintf(fp, "%d", TST_LONGBIMPY_BW);
|
316 |
|
|
#else
|
317 |
|
|
fprintf(fp, "IAW");
|
318 |
|
|
#endif
|
319 |
|
|
|
320 |
|
|
fprintf(fp, ", // The width of i_b, can be anything\n"
|
321 |
|
|
"\t\t\t// The following three parameters should not be changed\n"
|
322 |
|
|
"\t\t\t// by any implementation, but are based upon hardware\n"
|
323 |
|
|
"\t\t\t// and the above values:\n"
|
324 |
|
|
"\t\t\tOW=IAW+IBW; // The output width\n");
|
325 |
|
|
fprintf(fp,
|
326 |
|
|
"\tlocalparam AW = (IAW<IBW) ? IAW : IBW,\n"
|
327 |
|
|
"\t\t\tBW = (IAW<IBW) ? IBW : IAW,\n"
|
328 |
|
|
"\t\t\tIW=(AW+1)&(-2), // Internal width of A\n"
|
329 |
|
|
"\t\t\tLUTB=2, // How many bits we can multiply by at once\n"
|
330 |
|
|
"\t\t\tTLEN=(AW+(LUTB-1))/LUTB; // Nmbr of rows in our tableau\n"
|
331 |
37 |
dgisselq |
"\tinput\twire\t\t\ti_clk, i_ce;\n"
|
332 |
|
|
"\tinput\twire\t[(IAW-1):0]\ti_a_unsorted;\n"
|
333 |
|
|
"\tinput\twire\t[(IBW-1):0]\ti_b_unsorted;\n"
|
334 |
36 |
dgisselq |
"\toutput\treg\t[(AW+BW-1):0]\to_r;\n"
|
335 |
37 |
dgisselq |
"\n");
|
336 |
|
|
if (formal_property_flag) fprintf(fp,
|
337 |
|
|
"`ifdef FORMAL\n"
|
338 |
|
|
"\toutput\twire\t[(IAW-1):0]\tf_past_a_unsorted;\n"
|
339 |
|
|
"\toutput\twire\t[(IBW-1):0]\tf_past_b_unsorted;\n"
|
340 |
|
|
"`endif\n");
|
341 |
|
|
|
342 |
|
|
fprintf(fp, "\n"
|
343 |
36 |
dgisselq |
"\t//\n"
|
344 |
|
|
"\t// Swap parameter order, so that AW <= BW -- for performance\n"
|
345 |
|
|
"\t// reasons\n"
|
346 |
|
|
"\twire [AW-1:0] i_a;\n"
|
347 |
|
|
"\twire [BW-1:0] i_b;\n"
|
348 |
|
|
"\tgenerate if (IAW <= IBW)\n"
|
349 |
|
|
"\tbegin : NO_PARAM_CHANGE\n"
|
350 |
|
|
"\t\tassign i_a = i_a_unsorted;\n"
|
351 |
|
|
"\t\tassign i_b = i_b_unsorted;\n"
|
352 |
|
|
"\tend else begin : SWAP_PARAMETERS\n"
|
353 |
|
|
"\t\tassign i_a = i_b_unsorted;\n"
|
354 |
|
|
"\t\tassign i_b = i_a_unsorted;\n"
|
355 |
|
|
"\tend endgenerate\n"
|
356 |
|
|
"\n"
|
357 |
|
|
"\treg\t[(IW-1):0]\tu_a;\n"
|
358 |
|
|
"\treg\t[(BW-1):0]\tu_b;\n"
|
359 |
|
|
"\treg\t\t\tsgn;\n"
|
360 |
|
|
"\n"
|
361 |
|
|
"\treg\t[(IW-1-2*(LUTB)):0]\tr_a[0:(TLEN-3)];\n"
|
362 |
|
|
"\treg\t[(BW-1):0]\t\tr_b[0:(TLEN-3)];\n"
|
363 |
|
|
"\treg\t[(TLEN-1):0]\t\tr_s;\n"
|
364 |
|
|
"\treg\t[(IW+BW-1):0]\t\tacc[0:(TLEN-2)];\n"
|
365 |
|
|
"\tgenvar k;\n"
|
366 |
|
|
"\n"
|
367 |
|
|
"\t// First step:\n"
|
368 |
|
|
"\t// Switch to unsigned arithmetic for our multiply, keeping track\n"
|
369 |
|
|
"\t// of the along the way. We'll then add the sign again later at\n"
|
370 |
|
|
"\t// the end.\n"
|
371 |
|
|
"\t//\n"
|
372 |
|
|
"\t// If we were forced to stay within two's complement arithmetic,\n"
|
373 |
|
|
"\t// taking the absolute value here would require an additional bit.\n"
|
374 |
|
|
"\t// However, because our results are now unsigned, we can stay\n"
|
375 |
|
|
"\t// within the number of bits given (for now).\n"
|
376 |
37 |
dgisselq |
"\tinitial u_a = 0;\n"
|
377 |
36 |
dgisselq |
"\tgenerate if (IW > AW)\n"
|
378 |
37 |
dgisselq |
"\tbegin : ABS_AND_ADD_BIT_TO_A\n"
|
379 |
36 |
dgisselq |
"\t\talways @(posedge i_clk)\n"
|
380 |
|
|
"\t\t\tif (i_ce)\n"
|
381 |
|
|
"\t\t\t\tu_a <= { 1\'b0, (i_a[AW-1])?(-i_a):(i_a) };\n"
|
382 |
37 |
dgisselq |
"\tend else begin : ABS_A\n"
|
383 |
36 |
dgisselq |
"\t\talways @(posedge i_clk)\n"
|
384 |
|
|
"\t\t\tif (i_ce)\n"
|
385 |
|
|
"\t\t\t\tu_a <= (i_a[AW-1])?(-i_a):(i_a);\n"
|
386 |
|
|
"\tend endgenerate\n"
|
387 |
|
|
"\n"
|
388 |
37 |
dgisselq |
"\tinitial sgn = 0;\n"
|
389 |
|
|
"\tinitial u_b = 0;\n"
|
390 |
36 |
dgisselq |
"\talways @(posedge i_clk)\n"
|
391 |
37 |
dgisselq |
"\tif (i_ce)\n"
|
392 |
|
|
"\tbegin : ABS_B\n"
|
393 |
|
|
"\t\tu_b <= (i_b[BW-1])?(-i_b):(i_b);\n"
|
394 |
|
|
"\t\tsgn <= i_a[AW-1] ^ i_b[BW-1];\n"
|
395 |
|
|
"\tend\n"
|
396 |
36 |
dgisselq |
"\n"
|
397 |
|
|
"\twire [(BW+LUTB-1):0] pr_a, pr_b;\n"
|
398 |
|
|
"\n"
|
399 |
|
|
"\t//\n"
|
400 |
|
|
"\t// Second step: First two 2xN products.\n"
|
401 |
|
|
"\t//\n"
|
402 |
|
|
"\t// Since we have no tableau of additions (yet), we can do both\n"
|
403 |
|
|
"\t// of the first two rows at the same time and add them together.\n"
|
404 |
|
|
"\t// For the next round, we'll then have a previous sum to accumulate\n"
|
405 |
|
|
"\t// with new and subsequent product, and so only do one product at\n"
|
406 |
|
|
"\t// a time can follow this--but the first clock can do two at a time.\n"
|
407 |
|
|
"\tbimpy\t#(BW) lmpy_0(i_clk,i_ce,u_a[( LUTB-1): 0], u_b, pr_a);\n"
|
408 |
|
|
"\tbimpy\t#(BW) lmpy_1(i_clk,i_ce,u_a[(2*LUTB-1):LUTB], u_b, pr_b);\n"
|
409 |
37 |
dgisselq |
"\n"
|
410 |
|
|
"\tinitial r_s = 0;\n"
|
411 |
|
|
"\tinitial r_a[0] = 0;\n"
|
412 |
|
|
"\tinitial r_b[0] = 0;\n"
|
413 |
36 |
dgisselq |
"\talways @(posedge i_clk)\n"
|
414 |
|
|
"\t\tif (i_ce) r_a[0] <= u_a[(IW-1):(2*LUTB)];\n"
|
415 |
|
|
"\talways @(posedge i_clk)\n"
|
416 |
|
|
"\t\tif (i_ce) r_b[0] <= u_b;\n"
|
417 |
|
|
"\talways @(posedge i_clk)\n"
|
418 |
|
|
"\t\tif (i_ce) r_s <= { r_s[(TLEN-2):0], sgn };\n"
|
419 |
37 |
dgisselq |
"\n"
|
420 |
|
|
"\tinitial acc[0] = 0;\n"
|
421 |
36 |
dgisselq |
"\talways @(posedge i_clk) // One clk after p[0],p[1] become valid\n"
|
422 |
37 |
dgisselq |
"\tif (i_ce) acc[0] <= { {(IW-LUTB){1\'b0}}, pr_a}\n"
|
423 |
|
|
"\t\t +{ {(IW-(2*LUTB)){1\'b0}}, pr_b, {(LUTB){1\'b0}} };\n"
|
424 |
36 |
dgisselq |
"\n"
|
425 |
|
|
"\tgenerate // Keep track of intermediate values, before multiplying them\n"
|
426 |
|
|
"\tif (TLEN > 3) for(k=0; k<TLEN-3; k=k+1)\n"
|
427 |
37 |
dgisselq |
"\tbegin : GENCOPIES\n"
|
428 |
|
|
"\n"
|
429 |
|
|
"\t\tinitial r_a[k+1] = 0;\n"
|
430 |
|
|
"\t\tinitial r_b[k+1] = 0;\n"
|
431 |
36 |
dgisselq |
"\t\talways @(posedge i_clk)\n"
|
432 |
|
|
"\t\tif (i_ce)\n"
|
433 |
|
|
"\t\tbegin\n"
|
434 |
|
|
"\t\t\tr_a[k+1] <= { {(LUTB){1\'b0}},\n"
|
435 |
|
|
"\t\t\t\tr_a[k][(IW-1-(2*LUTB)):LUTB] };\n"
|
436 |
|
|
"\t\t\tr_b[k+1] <= r_b[k];\n"
|
437 |
|
|
"\t\tend\n"
|
438 |
|
|
"\tend endgenerate\n"
|
439 |
|
|
"\n"
|
440 |
|
|
"\tgenerate // The actual multiply and accumulate stage\n"
|
441 |
|
|
"\tif (TLEN > 2) for(k=0; k<TLEN-2; k=k+1)\n"
|
442 |
37 |
dgisselq |
"\tbegin : GENSTAGES\n"
|
443 |
|
|
"\t\twire\t[(BW+LUTB-1):0] genp;\n"
|
444 |
|
|
"\n"
|
445 |
36 |
dgisselq |
"\t\t// First, the multiply: 2-bits times BW bits\n"
|
446 |
|
|
"\t\tbimpy #(BW) genmpy(i_clk,i_ce,r_a[k][(LUTB-1):0],r_b[k], genp);\n"
|
447 |
|
|
"\n"
|
448 |
|
|
"\t\t// Then the accumulate step -- on the next clock\n"
|
449 |
37 |
dgisselq |
"\t\tinitial acc[k+1] = 0;\n"
|
450 |
36 |
dgisselq |
"\t\talways @(posedge i_clk)\n"
|
451 |
37 |
dgisselq |
"\t\tif (i_ce)\n"
|
452 |
|
|
"\t\t\tacc[k+1] <= acc[k] + {{(IW-LUTB*(k+3)){1\'b0}},\n"
|
453 |
|
|
"\t\t\t\tgenp, {(LUTB*(k+2)){1\'b0}} };\n"
|
454 |
36 |
dgisselq |
"\tend endgenerate\n"
|
455 |
|
|
"\n"
|
456 |
|
|
"\twire [(IW+BW-1):0] w_r;\n"
|
457 |
|
|
"\tassign\tw_r = (r_s[TLEN-1]) ? (-acc[TLEN-2]) : acc[TLEN-2];\n"
|
458 |
37 |
dgisselq |
"\n"
|
459 |
|
|
"\tinitial o_r = 0;\n"
|
460 |
36 |
dgisselq |
"\talways @(posedge i_clk)\n"
|
461 |
37 |
dgisselq |
"\tif (i_ce)\n"
|
462 |
|
|
"\t\to_r <= w_r[(AW+BW-1):0];\n"
|
463 |
|
|
"\n");
|
464 |
|
|
|
465 |
|
|
// Make Verilator happy
|
466 |
|
|
fprintf(fp,
|
467 |
36 |
dgisselq |
"\tgenerate if (IW > AW)\n"
|
468 |
|
|
"\tbegin : VUNUSED\n"
|
469 |
|
|
"\t\t// verilator lint_off UNUSED\n"
|
470 |
|
|
"\t\twire\t[(IW-AW)-1:0]\tunused;\n"
|
471 |
|
|
"\t\tassign\tunused = w_r[(IW+BW-1):(AW+BW)];\n"
|
472 |
|
|
"\t\t// verilator lint_on UNUSED\n"
|
473 |
|
|
"\tend endgenerate\n"
|
474 |
37 |
dgisselq |
"\n");
|
475 |
|
|
|
476 |
|
|
// The formal property section
|
477 |
|
|
// Starting with properties specific to this component's proof, and not
|
478 |
|
|
// any parent modules
|
479 |
|
|
fprintf(fp,
|
480 |
|
|
"`ifdef FORMAL\n");
|
481 |
|
|
|
482 |
|
|
if (formal_property_flag) {
|
483 |
|
|
fprintf(fp,
|
484 |
|
|
"\treg f_past_valid;\n"
|
485 |
|
|
"\tinitial\tf_past_valid = 1'b0;\n"
|
486 |
|
|
"\talways @(posedge i_clk)\n"
|
487 |
|
|
"\t\tf_past_valid <= 1'b1;\n"
|
488 |
36 |
dgisselq |
"\n"
|
489 |
37 |
dgisselq |
"`define\tASSERT assert\n"
|
490 |
|
|
"`ifdef LONGBIMPY\n"
|
491 |
|
|
"\n"
|
492 |
|
|
"\talways @(posedge i_clk)\n"
|
493 |
|
|
"\tif (!$past(i_ce))\n"
|
494 |
|
|
"\t\tassume(i_ce);\n"
|
495 |
|
|
"\n"
|
496 |
|
|
"`endif\n"
|
497 |
|
|
"\n");
|
498 |
|
|
|
499 |
|
|
// Now for properties specific to this core
|
500 |
|
|
fprintf(fp,
|
501 |
|
|
"\treg [AW-1:0] f_past_a [0:TLEN];\n"
|
502 |
|
|
"\treg [BW-1:0] f_past_b [0:TLEN];\n"
|
503 |
|
|
"\treg [TLEN+1:0] f_sgn_a, f_sgn_b;\n"
|
504 |
|
|
"\n");
|
505 |
|
|
|
506 |
|
|
fprintf(fp,
|
507 |
|
|
"\tinitial\tf_past_a[0] = 0;\n"
|
508 |
|
|
"\tinitial\tf_past_b[0] = 0;\n"
|
509 |
|
|
"\tinitial\tf_sgn_a = 0;\n"
|
510 |
|
|
"\tinitial\tf_sgn_b = 0;\n"
|
511 |
|
|
"\talways @(posedge i_clk)\n"
|
512 |
|
|
"\tif (i_ce)\n"
|
513 |
|
|
"\tbegin\n"
|
514 |
|
|
"\t\tf_past_a[0] <= u_a;\n"
|
515 |
|
|
"\t\tf_past_b[0] <= u_b;\n"
|
516 |
|
|
"\t\tf_sgn_a[0] <= i_a[AW-1];\n"
|
517 |
|
|
"\t\tf_sgn_b[0] <= i_b[BW-1];\n"
|
518 |
|
|
"\tend\n"
|
519 |
|
|
"\n");
|
520 |
|
|
|
521 |
|
|
fprintf(fp,
|
522 |
|
|
"\tgenerate for(k=0; k<TLEN; k=k+1)\n"
|
523 |
|
|
"\tbegin\n"
|
524 |
|
|
"\t\tinitial\tf_past_a[k+1] = 0;\n"
|
525 |
|
|
"\t\tinitial\tf_past_b[k+1] = 0;\n"
|
526 |
|
|
"\t\tinitial\tf_sgn_a[k+1] = 0;\n"
|
527 |
|
|
"\t\tinitial\tf_sgn_b[k+1] = 0;\n"
|
528 |
|
|
"\t\talways @(posedge i_clk)\n"
|
529 |
|
|
"\t\tif (i_ce)\n"
|
530 |
|
|
"\t\tbegin\n"
|
531 |
|
|
"\t\t\tf_past_a[k+1] <= f_past_a[k];\n"
|
532 |
|
|
"\t\t\tf_past_b[k+1] <= f_past_b[k];\n"
|
533 |
|
|
"\n"
|
534 |
|
|
"\t\t\tf_sgn_a[k+1] <= f_sgn_a[k];\n"
|
535 |
|
|
"\t\t\tf_sgn_b[k+1] <= f_sgn_b[k];\n"
|
536 |
|
|
"\t\tend\n"
|
537 |
|
|
"\tend endgenerate\n"
|
538 |
|
|
"\n");
|
539 |
|
|
|
540 |
|
|
fprintf(fp,
|
541 |
|
|
"\talways @(posedge i_clk)\n"
|
542 |
|
|
"\tif (i_ce)\n"
|
543 |
|
|
"\tbegin\n"
|
544 |
|
|
"\t\tf_sgn_a[TLEN+1] <= f_sgn_a[TLEN];\n"
|
545 |
|
|
"\t\tf_sgn_b[TLEN+1] <= f_sgn_b[TLEN];\n"
|
546 |
|
|
"\tend\n"
|
547 |
|
|
"\n");
|
548 |
|
|
|
549 |
|
|
fprintf(fp,
|
550 |
|
|
"\talways @(posedge i_clk)\n"
|
551 |
|
|
"\tbegin\n"
|
552 |
|
|
"\t\tassert(sgn == (f_sgn_a[0] ^ f_sgn_b[0]));\n"
|
553 |
|
|
"\t\tassert(r_s[TLEN-1:0] == (f_sgn_a[TLEN:1] ^ f_sgn_b[TLEN:1]));\n"
|
554 |
|
|
"\t\tassert(r_s[TLEN-1:0] == (f_sgn_a[TLEN:1] ^ f_sgn_b[TLEN:1]));\n"
|
555 |
|
|
"\tend\n"
|
556 |
|
|
"\n");
|
557 |
|
|
|
558 |
|
|
fprintf(fp,
|
559 |
|
|
"\talways @(posedge i_clk)\n"
|
560 |
|
|
"\tif ((f_past_valid)&&($past(i_ce)))\n"
|
561 |
|
|
"\tbegin\n"
|
562 |
|
|
"\t\tif ($past(i_a)==0)\n"
|
563 |
|
|
"\t\t\t`ASSERT(u_a == 0);\n"
|
564 |
|
|
"\t\telse if ($past(i_a[AW-1]) == 1'b0)\n"
|
565 |
|
|
"\t\t\t`ASSERT(u_a == $past(i_a));\n"
|
566 |
|
|
"\n"
|
567 |
|
|
"\t\tif ($past(i_b)==0)\n"
|
568 |
|
|
"\t\t\t`ASSERT(u_b == 0);\n"
|
569 |
|
|
"\t\telse if ($past(i_b[BW-1]) == 1'b0)\n"
|
570 |
|
|
"\t\t\t`ASSERT(u_b == $past(i_b));\n"
|
571 |
|
|
"\tend\n"
|
572 |
|
|
"\n");
|
573 |
|
|
|
574 |
|
|
fprintf(fp,
|
575 |
|
|
"\tgenerate // Keep track of intermediate values, before multiplying them\n"
|
576 |
|
|
"\tif (TLEN > 3) for(k=0; k<TLEN-3; k=k+1)\n"
|
577 |
|
|
"\tbegin : ASSERT_GENCOPY\n"
|
578 |
|
|
"\t\talways @(posedge i_clk)\n"
|
579 |
|
|
"\t\tif (i_ce)\n"
|
580 |
|
|
"\t\tbegin\n"
|
581 |
|
|
"\t\t\tif (f_past_a[k]==0)\n"
|
582 |
|
|
"\t\t\t\t`ASSERT(r_a[k] == 0);\n"
|
583 |
|
|
"\t\t\telse if (f_past_a[k]==1)\n"
|
584 |
|
|
"\t\t\t\t`ASSERT(r_a[k] == 0);\n"
|
585 |
|
|
"\t\t\t`ASSERT(r_b[k] == f_past_b[k]);\n"
|
586 |
|
|
"\t\tend\n"
|
587 |
|
|
"\tend endgenerate\n"
|
588 |
|
|
"\n");
|
589 |
|
|
|
590 |
|
|
fprintf(fp,
|
591 |
|
|
"\tgenerate // The actual multiply and accumulate stage\n"
|
592 |
|
|
"\tif (TLEN > 2) for(k=0; k<TLEN-2; k=k+1)\n"
|
593 |
|
|
"\tbegin : ASSERT_GENSTAGE\n"
|
594 |
|
|
"\t\talways @(posedge i_clk)\n"
|
595 |
|
|
"\t\tif ((f_past_valid)&&($past(i_ce)))\n"
|
596 |
|
|
"\t\tbegin\n"
|
597 |
|
|
"\t\t\tif (f_past_a[k+1]==0)\n"
|
598 |
|
|
"\t\t\t\t`ASSERT(acc[k] == 0);\n"
|
599 |
|
|
"\t\t\tif (f_past_a[k+1]==1)\n"
|
600 |
|
|
"\t\t\t\t`ASSERT(acc[k] == f_past_b[k+1]);\n"
|
601 |
|
|
"\t\t\tif (f_past_b[k+1]==0)\n"
|
602 |
|
|
"\t\t\t\t`ASSERT(acc[k] == 0);\n"
|
603 |
|
|
"\t\t\tif (f_past_b[k+1]==1)\n"
|
604 |
|
|
"\t\t\tbegin\n"
|
605 |
|
|
"\t\t\t\t`ASSERT(acc[k][(2*k)+3:0]\n"
|
606 |
|
|
"\t\t\t\t == f_past_a[k+1][(2*k)+3:0]);\n"
|
607 |
|
|
"\t\t\t\t`ASSERT(acc[k][(IW+BW-1):(2*k)+4] == 0);\n"
|
608 |
|
|
"\t\t\tend\n"
|
609 |
|
|
"\t\tend\n"
|
610 |
|
|
"\tend endgenerate\n"
|
611 |
|
|
"\n");
|
612 |
|
|
|
613 |
|
|
fprintf(fp,
|
614 |
|
|
"\twire [AW-1:0]\tf_past_a_neg = - f_past_a[TLEN];\n"
|
615 |
|
|
"\twire [BW-1:0]\tf_past_b_neg = - f_past_b[TLEN];\n"
|
616 |
|
|
"\n"
|
617 |
|
|
"\twire [AW-1:0]\tf_past_a_pos = f_past_a[TLEN][AW-1]\n"
|
618 |
|
|
"\t\t\t\t\t? f_past_a_neg : f_past_a[TLEN];\n"
|
619 |
|
|
"\twire [BW-1:0]\tf_past_b_pos = f_past_b[TLEN][BW-1]\n"
|
620 |
|
|
"\t\t\t\t\t? f_past_b_neg : f_past_b[TLEN];\n\n");
|
621 |
|
|
|
622 |
|
|
fprintf(fp,
|
623 |
|
|
"\talways @(posedge i_clk)\n"
|
624 |
|
|
"\tif ((f_past_valid)&&($past(i_ce)))\n"
|
625 |
|
|
"\tbegin\n"
|
626 |
|
|
"\t\tif ((f_past_a[TLEN]==0)||(f_past_b[TLEN]==0))\n"
|
627 |
|
|
"\t\t\t`ASSERT(o_r == 0);\n"
|
628 |
|
|
"\t\telse if (f_past_a[TLEN]==1)\n"
|
629 |
|
|
"\t\tbegin\n"
|
630 |
|
|
"\t\t\tif ((f_sgn_a[TLEN+1]^f_sgn_b[TLEN+1])==0)\n"
|
631 |
|
|
"\t\t\tbegin\n"
|
632 |
|
|
"\t\t\t\t`ASSERT(o_r[BW-1:0] == f_past_b_pos[BW-1:0]);\n"
|
633 |
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:BW] == 0);\n"
|
634 |
|
|
"\t\t\tend else begin // if (f_sgn_b[TLEN+1]) begin\n"
|
635 |
|
|
"\t\t\t\t`ASSERT(o_r[BW-1:0] == f_past_b_neg);\n"
|
636 |
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:BW]\n"
|
637 |
|
|
"\t\t\t\t\t== {(AW){f_past_b_neg[BW-1]}});\n"
|
638 |
|
|
"\t\t\tend\n"
|
639 |
|
|
"\t\tend else if (f_past_b[TLEN]==1)\n"
|
640 |
|
|
"\t\tbegin\n"
|
641 |
|
|
"\t\t\tif ((f_sgn_a[TLEN+1] ^ f_sgn_b[TLEN+1])==0)\n"
|
642 |
|
|
"\t\t\tbegin\n"
|
643 |
|
|
"\t\t\t\t`ASSERT(o_r[AW-1:0] == f_past_a_pos[AW-1:0]);\n"
|
644 |
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:AW] == 0);\n"
|
645 |
|
|
"\t\t\tend else begin\n"
|
646 |
|
|
"\t\t\t\t`ASSERT(o_r[AW-1:0] == f_past_a_neg);\n"
|
647 |
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:AW]\n"
|
648 |
|
|
"\t\t\t\t\t== {(BW){f_past_a_neg[AW-1]}});\n"
|
649 |
|
|
"\t\t\tend\n"
|
650 |
|
|
"\t\tend else begin\n"
|
651 |
|
|
"\t\t\t`ASSERT(o_r != 0);\n"
|
652 |
|
|
"\t\t\tif (!o_r[AW+BW-1:0])\n"
|
653 |
|
|
"\t\t\tbegin\n"
|
654 |
|
|
"\t\t\t\t`ASSERT((o_r[AW-1:0] != f_past_a[TLEN][AW-1:0])\n"
|
655 |
|
|
"\t\t\t\t\t||(o_r[AW+BW-1:AW]!=0));\n"
|
656 |
|
|
"\t\t\t\t`ASSERT((o_r[BW-1:0] != f_past_b[TLEN][BW-1:0])\n"
|
657 |
|
|
"\t\t\t\t\t||(o_r[AW+BW-1:BW]!=0));\n"
|
658 |
|
|
"\t\t\tend else begin\n"
|
659 |
|
|
"\t\t\t\t`ASSERT((o_r[AW-1:0] != f_past_a_neg[AW-1:0])\n"
|
660 |
|
|
"\t\t\t\t\t||(! (&o_r[AW+BW-1:AW])));\n"
|
661 |
|
|
"\t\t\t\t`ASSERT((o_r[BW-1:0] != f_past_b_neg[BW-1:0])\n"
|
662 |
|
|
"\t\t\t\t\t||(! (&o_r[AW+BW-1:BW]!=0)));\n"
|
663 |
|
|
"\t\t\tend\n"
|
664 |
|
|
"\t\tend\n"
|
665 |
|
|
"\tend\n"
|
666 |
|
|
"\n");
|
667 |
|
|
|
668 |
|
|
fprintf(fp,
|
669 |
|
|
"\tgenerate if (IAW <= IBW)\n"
|
670 |
|
|
"\tbegin : NO_PARAM_CHANGE\n"
|
671 |
|
|
"\t\tassign f_past_a_unsorted = (!f_sgn_a[TLEN+1])\n"
|
672 |
|
|
"\t\t\t\t\t? f_past_a[TLEN] : f_past_a_neg;\n"
|
673 |
|
|
"\t\tassign f_past_b_unsorted = (!f_sgn_b[TLEN+1])\n"
|
674 |
|
|
"\t\t\t\t\t? f_past_b[TLEN] : f_past_b_neg;\n"
|
675 |
|
|
"\tend else begin : SWAP_PARAMETERS\n"
|
676 |
|
|
"\t\tassign f_past_a_unsorted = (!f_sgn_b[TLEN+1])\n"
|
677 |
|
|
"\t\t\t\t\t? f_past_b[TLEN] : f_past_b_neg;\n"
|
678 |
|
|
"\t\tassign f_past_b_unsorted = (!f_sgn_a[TLEN+1])\n"
|
679 |
|
|
"\t\t\t\t\t? f_past_a[TLEN] : f_past_a_neg;\n"
|
680 |
|
|
"\tend endgenerate\n");
|
681 |
|
|
|
682 |
|
|
fprintf(fp,
|
683 |
|
|
"`ifdef BUTTERFLY\n"
|
684 |
|
|
"\t// The following properties artificially restrict the inputs\n"
|
685 |
|
|
"\t// to this long binary multiplier to only those values whose\n"
|
686 |
|
|
"\t// absolute value is 0..7. It is used by the formal proof of\n"
|
687 |
|
|
"\t// the BUTTERFLY to artificially limit the scope of the proof.\n"
|
688 |
|
|
"\t// By the time the butterfly sees this code, it will be known\n"
|
689 |
|
|
"\t// that the long binary multiply works. At issue will no longer\n"
|
690 |
|
|
"\t// be whether or not this works, but rather whether it works in\n"
|
691 |
|
|
"\t// context. For that purpose, we'll need to check timing, not\n"
|
692 |
|
|
"\t// results. Checking against inputs of +/- 1 and 0 are perfect\n"
|
693 |
|
|
"\t// for that task. The below assumptions (yes they are assumptions\n"
|
694 |
|
|
"\t// just go a little bit further.\n"
|
695 |
|
|
"\t//\n"
|
696 |
|
|
"\t// THEREFORE, THESE PROPERTIES ARE NOT NECESSARY TO PROVING THAT\n"
|
697 |
|
|
"\t// THIS MODULE WORKS, AND THEY WILL INTERFERE WITH THAT PROOF.\n"
|
698 |
|
|
"\t//\n"
|
699 |
|
|
"\t// This just limits the proof for the butterfly, the parent.\n"
|
700 |
|
|
"\t// module that calls this one\n"
|
701 |
|
|
"\t//\n"
|
702 |
|
|
"\t// Start by assuming that all inputs have an absolute value less\n"
|
703 |
|
|
"\t// than eight.\n"
|
704 |
|
|
"\talways @(*)\n"
|
705 |
|
|
"\t\tassume(u_a[AW-1:3] == 0);\n"
|
706 |
|
|
"\talways @(*)\n"
|
707 |
|
|
"\t\tassume(u_b[BW-1:3] == 0);\n"
|
708 |
|
|
"\n"
|
709 |
|
|
"\t// If the inputs have these properties, then so too do many of\n"
|
710 |
|
|
"\t// our internal values. ASSERT therefore that we never get out\n"
|
711 |
|
|
"\t// of bounds\n"
|
712 |
|
|
"\tgenerate for(k=0; k<TLEN; k=k+1)\n"
|
713 |
|
|
"\tbegin\n"
|
714 |
|
|
"\t\talways @(*)\n"
|
715 |
|
|
"\t\tbegin\n"
|
716 |
|
|
"\t\t\tassert(f_past_a[k][AW-1:3] == 0);\n"
|
717 |
|
|
"\t\t\tassert(f_past_b[k][BW-1:3] == 0);\n"
|
718 |
|
|
"\t\tend\n"
|
719 |
|
|
"\tend endgenerate\n"
|
720 |
|
|
"\n"
|
721 |
|
|
"\tgenerate for(k=0; k<TLEN-1; k=k+1)\n"
|
722 |
|
|
"\tbegin\n"
|
723 |
|
|
"\t\talways @(*)\n"
|
724 |
|
|
"\t\t\tassert(acc[k][IW+BW-1:6] == 0);\n"
|
725 |
|
|
"\tend endgenerate\n"
|
726 |
|
|
"\n"
|
727 |
|
|
"\tgenerate for(k=0; k<TLEN-2; k=k+1)\n"
|
728 |
|
|
"\tbegin\n"
|
729 |
|
|
"\t\talways @(*)\n"
|
730 |
|
|
"\t\t\tassert(r_b[k][BW-1:3] == 0);\n"
|
731 |
|
|
"\tend endgenerate\n"
|
732 |
|
|
"`endif // BUTTERFLY\n");
|
733 |
|
|
|
734 |
|
|
|
735 |
|
|
} else {
|
736 |
|
|
fprintf(fp, "// Formal properties have not been enabled\n");
|
737 |
|
|
}
|
738 |
|
|
|
739 |
|
|
fprintf(fp,
|
740 |
|
|
"`endif\t// FORMAL\n"
|
741 |
36 |
dgisselq |
"endmodule\n");
|
742 |
|
|
|
743 |
|
|
fclose(fp);
|
744 |
|
|
}
|
745 |
|
|
|