| Line 24... |
Line 24... |
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// for more details.
|
// for more details.
|
//
|
//
|
// You should have received a copy of the GNU General Public License along
|
// You should have received a copy of the GNU General Public License along
|
// with this program. (It's in the $(ROOT)/doc directory, run make with no
|
// with this program. (It's in the $(ROOT)/doc directory. Run make with no
|
// target there if the PDF file isn't present.) If not, see
|
// target there if the PDF file isn't present.) If not, see
|
// <http://www.gnu.org/licenses/> for a copy.
|
// <http://www.gnu.org/licenses/> for a copy.
|
//
|
//
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// http://www.gnu.org/licenses/gpl.html
|
// http://www.gnu.org/licenses/gpl.html
|
| Line 103... |
Line 103... |
fprintf(fp, "%d;\n", TST_SHIFTADDMPY_BW);
|
fprintf(fp, "%d;\n", TST_SHIFTADDMPY_BW);
|
#else
|
#else
|
fprintf(fp, "AWIDTH;\n");
|
fprintf(fp, "AWIDTH;\n");
|
#endif
|
#endif
|
fprintf(fp,
|
fprintf(fp,
|
"\tinput\t\t\t\t\ti_clk, i_ce;\n"
|
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
|
"\tinput\t\t[(AWIDTH-1):0]\t\ti_a;\n"
|
"\tinput\twire\t[(AWIDTH-1):0]\t\ti_a;\n"
|
"\tinput\t\t[(BWIDTH-1):0]\t\ti_b;\n"
|
"\tinput\twire\t[(BWIDTH-1):0]\t\ti_b;\n"
|
"\toutput\treg\t[(AWIDTH+BWIDTH-1):0]\to_r;\n"
|
"\toutput\treg\t[(AWIDTH+BWIDTH-1):0]\to_r;\n"
|
"\n"
|
"\n"
|
"\treg\t[(AWIDTH-1):0]\tu_a;\n"
|
"\treg\t[(AWIDTH-1):0]\tu_a;\n"
|
"\treg\t[(BWIDTH-1):0]\tu_b;\n"
|
"\treg\t[(BWIDTH-1):0]\tu_b;\n"
|
"\treg\t\t\tsgn;\n"
|
"\treg\t\t\tsgn;\n"
|
| Line 198... |
Line 198... |
|
|
fprintf(fp, "%s", cpyleft);
|
fprintf(fp, "%s", cpyleft);
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
fprintf(fp,
|
fprintf(fp,
|
"module bimpy(i_clk, i_ce, i_a, i_b, o_r);\n"
|
"module bimpy(i_clk, i_ce, i_a, i_b, o_r);\n"
|
"\tparameter\tBW=18, // Number of bits in i_b\n"
|
"\tparameter\tBW=18; // Number of bits in i_b\n"
|
"\t\t\tLUTB=2; // Number of bits in i_a for our LUT multiply\n"
|
"\tlocalparam\tLUTB=2; // Number of bits in i_a for our LUT multiply\n"
|
"\tinput\t\t\t\ti_clk, i_ce;\n"
|
"\tinput\twire\t\t\ti_clk, i_ce;\n"
|
"\tinput\t\t[(LUTB-1):0]\ti_a;\n"
|
"\tinput\twire\t[(LUTB-1):0]\ti_a;\n"
|
"\tinput\t\t[(BW-1):0]\ti_b;\n"
|
"\tinput\twire\t[(BW-1):0]\ti_b;\n"
|
"\toutput\treg\t[(BW+LUTB-1):0] o_r;\n"
|
"\toutput\treg\t[(BW+LUTB-1):0] o_r;\n"
|
"\n"
|
"\n"
|
"\twire [(BW+LUTB-2):0] w_r;\n"
|
"\twire [(BW+LUTB-2):0] w_r;\n"
|
"\twire [(BW+LUTB-3):1] c;\n"
|
"\twire [(BW+LUTB-3):1] c;\n"
|
"\n"
|
"\n"
|
"\tassign\tw_r = { ((i_a[1])?i_b:{(BW){1\'b0}}), 1\'b0 }\n"
|
"\tassign\tw_r = { ((i_a[1])?i_b:{(BW){1\'b0}}), 1\'b0 }\n"
|
"\t\t\t\t^ { 1\'b0, ((i_a[0])?i_b:{(BW){1\'b0}}) };\n"
|
"\t\t\t\t^ { 1\'b0, ((i_a[0])?i_b:{(BW){1\'b0}}) };\n"
|
"\tassign\tc = { ((i_a[1])?i_b[(BW-2):0]:{(BW-1){1\'b0}}) }\n"
|
"\tassign\tc = { ((i_a[1])?i_b[(BW-2):0]:{(BW-1){1\'b0}}) }\n"
|
"\t\t\t& ((i_a[0])?i_b[(BW-1):1]:{(BW-1){1\'b0}});\n"
|
"\t\t\t& ((i_a[0])?i_b[(BW-1):1]:{(BW-1){1\'b0}});\n"
|
"\n"
|
"\n"
|
|
"\tinitial o_r = 0;\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|
"\t\tif (i_ce)\n"
|
"\tif (i_ce)\n"
|
"\t\t\to_r <= w_r + { c, 2'b0 };\n"
|
"\t\to_r <= w_r + { c, 2'b0 };\n"
|
|
"\n");
|
|
|
|
// Formal properties
|
|
//
|
|
// This module is formally verified as part of longbimpy.v
|
|
// Hence, we'll use an ifdef LONGBIMPY to capture if it is being verified as part of
|
|
// LONGBIMPY, or placed within another module.
|
|
fprintf(fp,
|
|
"`ifdef FORMAL\n");
|
|
|
|
if (formal_property_flag) {
|
|
fprintf(fp,
|
|
"\treg\tf_past_valid;\n"
|
|
"\n"
|
|
"\tinitial\tf_past_valid = 1'b0;\n"
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tf_past_valid <= 1'b1;\n"
|
"\n"
|
"\n"
|
|
"`define\tASSERT\tassert\n"
|
|
"\n");
|
|
|
|
// Now for our module specific assertions
|
|
// These properties will be assumed if this proof is not part of LONGBIMPY's proof
|
|
fprintf(fp,
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif ((f_past_valid)&&($past(i_ce)))\n"
|
|
"\tbegin\n"
|
|
"\t\tif ($past(i_a)==0)\n"
|
|
"\t\t\t`ASSERT(o_r == 0);\n"
|
|
"\t\telse if ($past(i_a) == 1)\n"
|
|
"\t\t\t`ASSERT(o_r == $past(i_b));\n"
|
|
"\n"
|
|
"\t\tif ($past(i_b)==0)\n"
|
|
"\t\t\t`ASSERT(o_r == 0);\n"
|
|
"\t\telse if ($past(i_b) == 1)\n"
|
|
"\t\t\t`ASSERT(o_r[(LUTB-1):0] == $past(i_a));\n"
|
|
"\tend\n");
|
|
|
|
} else {
|
|
fprintf(fp, "// Enable the formal_property_flag to include formal properties\n");
|
|
}
|
|
|
|
fprintf(fp,
|
|
"`endif\n");
|
|
// And then the end of the module
|
|
fprintf(fp,
|
"endmodule\n");
|
"endmodule\n");
|
|
|
fclose(fp);
|
fclose(fp);
|
}
|
}
|
|
|
| Line 253... |
Line 299... |
"//\n", fname, prjname, creator);
|
"//\n", fname, prjname, creator);
|
|
|
fprintf(fp, "%s", cpyleft);
|
fprintf(fp, "%s", cpyleft);
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
fprintf(fp,
|
fprintf(fp,
|
"module longbimpy(i_clk, i_ce, i_a_unsorted, i_b_unsorted, o_r);\n"
|
"module longbimpy(i_clk, i_ce, i_a_unsorted, i_b_unsorted, o_r\n");
|
|
|
|
if (formal_property_flag) fprintf(fp,
|
|
"`ifdef FORMAL\n"
|
|
"\t, f_past_a_unsorted, f_past_b_unsorted\n"
|
|
"`endif\n\t\t");
|
|
|
|
fprintf(fp, ");\n"
|
"\tparameter IAW=%d, // The width of i_a, min width is 5\n"
|
"\tparameter IAW=%d, // The width of i_a, min width is 5\n"
|
"\t\t\tIBW=", TST_LONGBIMPY_AW);
|
"\t\t\tIBW=", TST_LONGBIMPY_AW);
|
#ifdef TST_LONGBIMPY_BW
|
#ifdef TST_LONGBIMPY_BW
|
fprintf(fp, "%d", TST_LONGBIMPY_BW);
|
fprintf(fp, "%d", TST_LONGBIMPY_BW);
|
#else
|
#else
|
| Line 273... |
Line 326... |
"\tlocalparam AW = (IAW<IBW) ? IAW : IBW,\n"
|
"\tlocalparam AW = (IAW<IBW) ? IAW : IBW,\n"
|
"\t\t\tBW = (IAW<IBW) ? IBW : IAW,\n"
|
"\t\t\tBW = (IAW<IBW) ? IBW : IAW,\n"
|
"\t\t\tIW=(AW+1)&(-2), // Internal width of A\n"
|
"\t\t\tIW=(AW+1)&(-2), // Internal width of A\n"
|
"\t\t\tLUTB=2, // How many bits we can multiply by at once\n"
|
"\t\t\tLUTB=2, // How many bits we can multiply by at once\n"
|
"\t\t\tTLEN=(AW+(LUTB-1))/LUTB; // Nmbr of rows in our tableau\n"
|
"\t\t\tTLEN=(AW+(LUTB-1))/LUTB; // Nmbr of rows in our tableau\n"
|
"\tinput\t\t\t\ti_clk, i_ce;\n"
|
"\tinput\twire\t\t\ti_clk, i_ce;\n"
|
"\tinput\t\t[(IAW-1):0]\ti_a_unsorted;\n"
|
"\tinput\twire\t[(IAW-1):0]\ti_a_unsorted;\n"
|
"\tinput\t\t[(IBW-1):0]\ti_b_unsorted;\n"
|
"\tinput\twire\t[(IBW-1):0]\ti_b_unsorted;\n"
|
"\toutput\treg\t[(AW+BW-1):0]\to_r;\n"
|
"\toutput\treg\t[(AW+BW-1):0]\to_r;\n"
|
"\n"
|
"\n");
|
|
if (formal_property_flag) fprintf(fp,
|
|
"`ifdef FORMAL\n"
|
|
"\toutput\twire\t[(IAW-1):0]\tf_past_a_unsorted;\n"
|
|
"\toutput\twire\t[(IBW-1):0]\tf_past_b_unsorted;\n"
|
|
"`endif\n");
|
|
|
|
fprintf(fp, "\n"
|
"\t//\n"
|
"\t//\n"
|
"\t// Swap parameter order, so that AW <= BW -- for performance\n"
|
"\t// Swap parameter order, so that AW <= BW -- for performance\n"
|
"\t// reasons\n"
|
"\t// reasons\n"
|
"\twire [AW-1:0] i_a;\n"
|
"\twire [AW-1:0] i_a;\n"
|
"\twire [BW-1:0] i_b;\n"
|
"\twire [BW-1:0] i_b;\n"
|
| Line 311... |
Line 371... |
"\t//\n"
|
"\t//\n"
|
"\t// If we were forced to stay within two's complement arithmetic,\n"
|
"\t// If we were forced to stay within two's complement arithmetic,\n"
|
"\t// taking the absolute value here would require an additional bit.\n"
|
"\t// taking the absolute value here would require an additional bit.\n"
|
"\t// However, because our results are now unsigned, we can stay\n"
|
"\t// However, because our results are now unsigned, we can stay\n"
|
"\t// within the number of bits given (for now).\n"
|
"\t// within the number of bits given (for now).\n"
|
|
"\tinitial u_a = 0;\n"
|
"\tgenerate if (IW > AW)\n"
|
"\tgenerate if (IW > AW)\n"
|
"\tbegin\n"
|
"\tbegin : ABS_AND_ADD_BIT_TO_A\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\t\tif (i_ce)\n"
|
"\t\t\tif (i_ce)\n"
|
"\t\t\t\tu_a <= { 1\'b0, (i_a[AW-1])?(-i_a):(i_a) };\n"
|
"\t\t\t\tu_a <= { 1\'b0, (i_a[AW-1])?(-i_a):(i_a) };\n"
|
"\tend else begin\n"
|
"\tend else begin : ABS_A\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\t\tif (i_ce)\n"
|
"\t\t\tif (i_ce)\n"
|
"\t\t\t\tu_a <= (i_a[AW-1])?(-i_a):(i_a);\n"
|
"\t\t\t\tu_a <= (i_a[AW-1])?(-i_a):(i_a);\n"
|
"\tend endgenerate\n"
|
"\tend endgenerate\n"
|
"\n"
|
"\n"
|
|
"\tinitial sgn = 0;\n"
|
|
"\tinitial u_b = 0;\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|
"\t\tif (i_ce)\n"
|
"\tif (i_ce)\n"
|
"\t\tbegin\n"
|
"\tbegin : ABS_B\n"
|
"\t\t\tu_b <= (i_b[BW-1])?(-i_b):(i_b);\n"
|
"\t\tu_b <= (i_b[BW-1])?(-i_b):(i_b);\n"
|
"\t\t\tsgn <= i_a[AW-1] ^ i_b[BW-1];\n"
|
"\t\tsgn <= i_a[AW-1] ^ i_b[BW-1];\n"
|
"\t\tend\n"
|
"\tend\n"
|
"\n"
|
"\n"
|
"\twire [(BW+LUTB-1):0] pr_a, pr_b;\n"
|
"\twire [(BW+LUTB-1):0] pr_a, pr_b;\n"
|
"\n"
|
"\n"
|
"\t//\n"
|
"\t//\n"
|
"\t// Second step: First two 2xN products.\n"
|
"\t// Second step: First two 2xN products.\n"
|
| Line 341... |
Line 404... |
"\t// For the next round, we'll then have a previous sum to accumulate\n"
|
"\t// For the next round, we'll then have a previous sum to accumulate\n"
|
"\t// with new and subsequent product, and so only do one product at\n"
|
"\t// with new and subsequent product, and so only do one product at\n"
|
"\t// a time can follow this--but the first clock can do two at a time.\n"
|
"\t// a time can follow this--but the first clock can do two at a time.\n"
|
"\tbimpy\t#(BW) lmpy_0(i_clk,i_ce,u_a[( LUTB-1): 0], u_b, pr_a);\n"
|
"\tbimpy\t#(BW) lmpy_0(i_clk,i_ce,u_a[( LUTB-1): 0], u_b, pr_a);\n"
|
"\tbimpy\t#(BW) lmpy_1(i_clk,i_ce,u_a[(2*LUTB-1):LUTB], u_b, pr_b);\n"
|
"\tbimpy\t#(BW) lmpy_1(i_clk,i_ce,u_a[(2*LUTB-1):LUTB], u_b, pr_b);\n"
|
|
"\n"
|
|
"\tinitial r_s = 0;\n"
|
|
"\tinitial r_a[0] = 0;\n"
|
|
"\tinitial r_b[0] = 0;\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|
"\t\tif (i_ce) r_a[0] <= u_a[(IW-1):(2*LUTB)];\n"
|
"\t\tif (i_ce) r_a[0] <= u_a[(IW-1):(2*LUTB)];\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|
"\t\tif (i_ce) r_b[0] <= u_b;\n"
|
"\t\tif (i_ce) r_b[0] <= u_b;\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|
"\t\tif (i_ce) r_s <= { r_s[(TLEN-2):0], sgn };\n"
|
"\t\tif (i_ce) r_s <= { r_s[(TLEN-2):0], sgn };\n"
|
|
"\n"
|
|
"\tinitial acc[0] = 0;\n"
|
"\talways @(posedge i_clk) // One clk after p[0],p[1] become valid\n"
|
"\talways @(posedge i_clk) // One clk after p[0],p[1] become valid\n"
|
"\t\tif (i_ce) acc[0] <= { {(IW-LUTB){1\'b0}}, pr_a}\n"
|
"\tif (i_ce) acc[0] <= { {(IW-LUTB){1\'b0}}, pr_a}\n"
|
"\t\t\t +{ {(IW-(2*LUTB)){1\'b0}}, pr_b, {(LUTB){1\'b0}} };\n"
|
"\t\t +{ {(IW-(2*LUTB)){1\'b0}}, pr_b, {(LUTB){1\'b0}} };\n"
|
"\n"
|
"\n"
|
"\tgenerate // Keep track of intermediate values, before multiplying them\n"
|
"\tgenerate // Keep track of intermediate values, before multiplying them\n"
|
"\tif (TLEN > 3) for(k=0; k<TLEN-3; k=k+1)\n"
|
"\tif (TLEN > 3) for(k=0; k<TLEN-3; k=k+1)\n"
|
"\tbegin : gencopies\n"
|
"\tbegin : GENCOPIES\n"
|
|
"\n"
|
|
"\t\tinitial r_a[k+1] = 0;\n"
|
|
"\t\tinitial r_b[k+1] = 0;\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\tif (i_ce)\n"
|
"\t\tif (i_ce)\n"
|
"\t\tbegin\n"
|
"\t\tbegin\n"
|
"\t\t\tr_a[k+1] <= { {(LUTB){1\'b0}},\n"
|
"\t\t\tr_a[k+1] <= { {(LUTB){1\'b0}},\n"
|
"\t\t\t\tr_a[k][(IW-1-(2*LUTB)):LUTB] };\n"
|
"\t\t\t\tr_a[k][(IW-1-(2*LUTB)):LUTB] };\n"
|
| Line 365... |
Line 437... |
"\t\tend\n"
|
"\t\tend\n"
|
"\tend endgenerate\n"
|
"\tend endgenerate\n"
|
"\n"
|
"\n"
|
"\tgenerate // The actual multiply and accumulate stage\n"
|
"\tgenerate // The actual multiply and accumulate stage\n"
|
"\tif (TLEN > 2) for(k=0; k<TLEN-2; k=k+1)\n"
|
"\tif (TLEN > 2) for(k=0; k<TLEN-2; k=k+1)\n"
|
"\tbegin : genstages\n"
|
"\tbegin : GENSTAGES\n"
|
"\t\t// First, the multiply: 2-bits times BW bits\n"
|
|
"\t\twire\t[(BW+LUTB-1):0] genp;\n"
|
"\t\twire\t[(BW+LUTB-1):0] genp;\n"
|
|
"\n"
|
|
"\t\t// First, the multiply: 2-bits times BW bits\n"
|
"\t\tbimpy #(BW) genmpy(i_clk,i_ce,r_a[k][(LUTB-1):0],r_b[k], genp);\n"
|
"\t\tbimpy #(BW) genmpy(i_clk,i_ce,r_a[k][(LUTB-1):0],r_b[k], genp);\n"
|
"\n"
|
"\n"
|
"\t\t// Then the accumulate step -- on the next clock\n"
|
"\t\t// Then the accumulate step -- on the next clock\n"
|
|
"\t\tinitial acc[k+1] = 0;\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\talways @(posedge i_clk)\n"
|
"\t\t\tif (i_ce)\n"
|
"\t\tif (i_ce)\n"
|
"\t\t\t\tacc[k+1] <= acc[k] + {{(IW-LUTB*(k+3)){1\'b0}},\n"
|
"\t\t\tacc[k+1] <= acc[k] + {{(IW-LUTB*(k+3)){1\'b0}},\n"
|
"\t\t\t\t\tgenp, {(LUTB*(k+2)){1\'b0}} };\n"
|
"\t\t\t\tgenp, {(LUTB*(k+2)){1\'b0}} };\n"
|
"\tend endgenerate\n"
|
"\tend endgenerate\n"
|
"\n"
|
"\n"
|
"\twire [(IW+BW-1):0] w_r;\n"
|
"\twire [(IW+BW-1):0] w_r;\n"
|
"\tassign\tw_r = (r_s[TLEN-1]) ? (-acc[TLEN-2]) : acc[TLEN-2];\n"
|
"\tassign\tw_r = (r_s[TLEN-1]) ? (-acc[TLEN-2]) : acc[TLEN-2];\n"
|
"\talways @(posedge i_clk)\n"
|
|
"\t\tif (i_ce)\n"
|
|
"\t\t\to_r <= w_r[(AW+BW-1):0];\n"
|
|
"\n"
|
"\n"
|
|
"\tinitial o_r = 0;\n"
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif (i_ce)\n"
|
|
"\t\to_r <= w_r[(AW+BW-1):0];\n"
|
|
"\n");
|
|
|
|
// Make Verilator happy
|
|
fprintf(fp,
|
"\tgenerate if (IW > AW)\n"
|
"\tgenerate if (IW > AW)\n"
|
"\tbegin : VUNUSED\n"
|
"\tbegin : VUNUSED\n"
|
"\t\t// verilator lint_off UNUSED\n"
|
"\t\t// verilator lint_off UNUSED\n"
|
"\t\twire\t[(IW-AW)-1:0]\tunused;\n"
|
"\t\twire\t[(IW-AW)-1:0]\tunused;\n"
|
"\t\tassign\tunused = w_r[(IW+BW-1):(AW+BW)];\n"
|
"\t\tassign\tunused = w_r[(IW+BW-1):(AW+BW)];\n"
|
"\t\t// verilator lint_on UNUSED\n"
|
"\t\t// verilator lint_on UNUSED\n"
|
"\tend endgenerate\n"
|
"\tend endgenerate\n"
|
|
"\n");
|
|
|
|
// The formal property section
|
|
// Starting with properties specific to this component's proof, and not
|
|
// any parent modules
|
|
fprintf(fp,
|
|
"`ifdef FORMAL\n");
|
|
|
|
if (formal_property_flag) {
|
|
fprintf(fp,
|
|
"\treg f_past_valid;\n"
|
|
"\tinitial\tf_past_valid = 1'b0;\n"
|
|
"\talways @(posedge i_clk)\n"
|
|
"\t\tf_past_valid <= 1'b1;\n"
|
|
"\n"
|
|
"`define\tASSERT assert\n"
|
|
"`ifdef LONGBIMPY\n"
|
|
"\n"
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif (!$past(i_ce))\n"
|
|
"\t\tassume(i_ce);\n"
|
|
"\n"
|
|
"`endif\n"
|
|
"\n");
|
|
|
|
// Now for properties specific to this core
|
|
fprintf(fp,
|
|
"\treg [AW-1:0] f_past_a [0:TLEN];\n"
|
|
"\treg [BW-1:0] f_past_b [0:TLEN];\n"
|
|
"\treg [TLEN+1:0] f_sgn_a, f_sgn_b;\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\tinitial\tf_past_a[0] = 0;\n"
|
|
"\tinitial\tf_past_b[0] = 0;\n"
|
|
"\tinitial\tf_sgn_a = 0;\n"
|
|
"\tinitial\tf_sgn_b = 0;\n"
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif (i_ce)\n"
|
|
"\tbegin\n"
|
|
"\t\tf_past_a[0] <= u_a;\n"
|
|
"\t\tf_past_b[0] <= u_b;\n"
|
|
"\t\tf_sgn_a[0] <= i_a[AW-1];\n"
|
|
"\t\tf_sgn_b[0] <= i_b[BW-1];\n"
|
|
"\tend\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\tgenerate for(k=0; k<TLEN; k=k+1)\n"
|
|
"\tbegin\n"
|
|
"\t\tinitial\tf_past_a[k+1] = 0;\n"
|
|
"\t\tinitial\tf_past_b[k+1] = 0;\n"
|
|
"\t\tinitial\tf_sgn_a[k+1] = 0;\n"
|
|
"\t\tinitial\tf_sgn_b[k+1] = 0;\n"
|
|
"\t\talways @(posedge i_clk)\n"
|
|
"\t\tif (i_ce)\n"
|
|
"\t\tbegin\n"
|
|
"\t\t\tf_past_a[k+1] <= f_past_a[k];\n"
|
|
"\t\t\tf_past_b[k+1] <= f_past_b[k];\n"
|
|
"\n"
|
|
"\t\t\tf_sgn_a[k+1] <= f_sgn_a[k];\n"
|
|
"\t\t\tf_sgn_b[k+1] <= f_sgn_b[k];\n"
|
|
"\t\tend\n"
|
|
"\tend endgenerate\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif (i_ce)\n"
|
|
"\tbegin\n"
|
|
"\t\tf_sgn_a[TLEN+1] <= f_sgn_a[TLEN];\n"
|
|
"\t\tf_sgn_b[TLEN+1] <= f_sgn_b[TLEN];\n"
|
|
"\tend\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tbegin\n"
|
|
"\t\tassert(sgn == (f_sgn_a[0] ^ f_sgn_b[0]));\n"
|
|
"\t\tassert(r_s[TLEN-1:0] == (f_sgn_a[TLEN:1] ^ f_sgn_b[TLEN:1]));\n"
|
|
"\t\tassert(r_s[TLEN-1:0] == (f_sgn_a[TLEN:1] ^ f_sgn_b[TLEN:1]));\n"
|
|
"\tend\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif ((f_past_valid)&&($past(i_ce)))\n"
|
|
"\tbegin\n"
|
|
"\t\tif ($past(i_a)==0)\n"
|
|
"\t\t\t`ASSERT(u_a == 0);\n"
|
|
"\t\telse if ($past(i_a[AW-1]) == 1'b0)\n"
|
|
"\t\t\t`ASSERT(u_a == $past(i_a));\n"
|
|
"\n"
|
|
"\t\tif ($past(i_b)==0)\n"
|
|
"\t\t\t`ASSERT(u_b == 0);\n"
|
|
"\t\telse if ($past(i_b[BW-1]) == 1'b0)\n"
|
|
"\t\t\t`ASSERT(u_b == $past(i_b));\n"
|
|
"\tend\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\tgenerate // Keep track of intermediate values, before multiplying them\n"
|
|
"\tif (TLEN > 3) for(k=0; k<TLEN-3; k=k+1)\n"
|
|
"\tbegin : ASSERT_GENCOPY\n"
|
|
"\t\talways @(posedge i_clk)\n"
|
|
"\t\tif (i_ce)\n"
|
|
"\t\tbegin\n"
|
|
"\t\t\tif (f_past_a[k]==0)\n"
|
|
"\t\t\t\t`ASSERT(r_a[k] == 0);\n"
|
|
"\t\t\telse if (f_past_a[k]==1)\n"
|
|
"\t\t\t\t`ASSERT(r_a[k] == 0);\n"
|
|
"\t\t\t`ASSERT(r_b[k] == f_past_b[k]);\n"
|
|
"\t\tend\n"
|
|
"\tend endgenerate\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\tgenerate // The actual multiply and accumulate stage\n"
|
|
"\tif (TLEN > 2) for(k=0; k<TLEN-2; k=k+1)\n"
|
|
"\tbegin : ASSERT_GENSTAGE\n"
|
|
"\t\talways @(posedge i_clk)\n"
|
|
"\t\tif ((f_past_valid)&&($past(i_ce)))\n"
|
|
"\t\tbegin\n"
|
|
"\t\t\tif (f_past_a[k+1]==0)\n"
|
|
"\t\t\t\t`ASSERT(acc[k] == 0);\n"
|
|
"\t\t\tif (f_past_a[k+1]==1)\n"
|
|
"\t\t\t\t`ASSERT(acc[k] == f_past_b[k+1]);\n"
|
|
"\t\t\tif (f_past_b[k+1]==0)\n"
|
|
"\t\t\t\t`ASSERT(acc[k] == 0);\n"
|
|
"\t\t\tif (f_past_b[k+1]==1)\n"
|
|
"\t\t\tbegin\n"
|
|
"\t\t\t\t`ASSERT(acc[k][(2*k)+3:0]\n"
|
|
"\t\t\t\t == f_past_a[k+1][(2*k)+3:0]);\n"
|
|
"\t\t\t\t`ASSERT(acc[k][(IW+BW-1):(2*k)+4] == 0);\n"
|
|
"\t\t\tend\n"
|
|
"\t\tend\n"
|
|
"\tend endgenerate\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\twire [AW-1:0]\tf_past_a_neg = - f_past_a[TLEN];\n"
|
|
"\twire [BW-1:0]\tf_past_b_neg = - f_past_b[TLEN];\n"
|
|
"\n"
|
|
"\twire [AW-1:0]\tf_past_a_pos = f_past_a[TLEN][AW-1]\n"
|
|
"\t\t\t\t\t? f_past_a_neg : f_past_a[TLEN];\n"
|
|
"\twire [BW-1:0]\tf_past_b_pos = f_past_b[TLEN][BW-1]\n"
|
|
"\t\t\t\t\t? f_past_b_neg : f_past_b[TLEN];\n\n");
|
|
|
|
fprintf(fp,
|
|
"\talways @(posedge i_clk)\n"
|
|
"\tif ((f_past_valid)&&($past(i_ce)))\n"
|
|
"\tbegin\n"
|
|
"\t\tif ((f_past_a[TLEN]==0)||(f_past_b[TLEN]==0))\n"
|
|
"\t\t\t`ASSERT(o_r == 0);\n"
|
|
"\t\telse if (f_past_a[TLEN]==1)\n"
|
|
"\t\tbegin\n"
|
|
"\t\t\tif ((f_sgn_a[TLEN+1]^f_sgn_b[TLEN+1])==0)\n"
|
|
"\t\t\tbegin\n"
|
|
"\t\t\t\t`ASSERT(o_r[BW-1:0] == f_past_b_pos[BW-1:0]);\n"
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:BW] == 0);\n"
|
|
"\t\t\tend else begin // if (f_sgn_b[TLEN+1]) begin\n"
|
|
"\t\t\t\t`ASSERT(o_r[BW-1:0] == f_past_b_neg);\n"
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:BW]\n"
|
|
"\t\t\t\t\t== {(AW){f_past_b_neg[BW-1]}});\n"
|
|
"\t\t\tend\n"
|
|
"\t\tend else if (f_past_b[TLEN]==1)\n"
|
|
"\t\tbegin\n"
|
|
"\t\t\tif ((f_sgn_a[TLEN+1] ^ f_sgn_b[TLEN+1])==0)\n"
|
|
"\t\t\tbegin\n"
|
|
"\t\t\t\t`ASSERT(o_r[AW-1:0] == f_past_a_pos[AW-1:0]);\n"
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:AW] == 0);\n"
|
|
"\t\t\tend else begin\n"
|
|
"\t\t\t\t`ASSERT(o_r[AW-1:0] == f_past_a_neg);\n"
|
|
"\t\t\t\t`ASSERT(o_r[AW+BW-1:AW]\n"
|
|
"\t\t\t\t\t== {(BW){f_past_a_neg[AW-1]}});\n"
|
|
"\t\t\tend\n"
|
|
"\t\tend else begin\n"
|
|
"\t\t\t`ASSERT(o_r != 0);\n"
|
|
"\t\t\tif (!o_r[AW+BW-1:0])\n"
|
|
"\t\t\tbegin\n"
|
|
"\t\t\t\t`ASSERT((o_r[AW-1:0] != f_past_a[TLEN][AW-1:0])\n"
|
|
"\t\t\t\t\t||(o_r[AW+BW-1:AW]!=0));\n"
|
|
"\t\t\t\t`ASSERT((o_r[BW-1:0] != f_past_b[TLEN][BW-1:0])\n"
|
|
"\t\t\t\t\t||(o_r[AW+BW-1:BW]!=0));\n"
|
|
"\t\t\tend else begin\n"
|
|
"\t\t\t\t`ASSERT((o_r[AW-1:0] != f_past_a_neg[AW-1:0])\n"
|
|
"\t\t\t\t\t||(! (&o_r[AW+BW-1:AW])));\n"
|
|
"\t\t\t\t`ASSERT((o_r[BW-1:0] != f_past_b_neg[BW-1:0])\n"
|
|
"\t\t\t\t\t||(! (&o_r[AW+BW-1:BW]!=0)));\n"
|
|
"\t\t\tend\n"
|
|
"\t\tend\n"
|
|
"\tend\n"
|
|
"\n");
|
|
|
|
fprintf(fp,
|
|
"\tgenerate if (IAW <= IBW)\n"
|
|
"\tbegin : NO_PARAM_CHANGE\n"
|
|
"\t\tassign f_past_a_unsorted = (!f_sgn_a[TLEN+1])\n"
|
|
"\t\t\t\t\t? f_past_a[TLEN] : f_past_a_neg;\n"
|
|
"\t\tassign f_past_b_unsorted = (!f_sgn_b[TLEN+1])\n"
|
|
"\t\t\t\t\t? f_past_b[TLEN] : f_past_b_neg;\n"
|
|
"\tend else begin : SWAP_PARAMETERS\n"
|
|
"\t\tassign f_past_a_unsorted = (!f_sgn_b[TLEN+1])\n"
|
|
"\t\t\t\t\t? f_past_b[TLEN] : f_past_b_neg;\n"
|
|
"\t\tassign f_past_b_unsorted = (!f_sgn_a[TLEN+1])\n"
|
|
"\t\t\t\t\t? f_past_a[TLEN] : f_past_a_neg;\n"
|
|
"\tend endgenerate\n");
|
|
|
|
fprintf(fp,
|
|
"`ifdef BUTTERFLY\n"
|
|
"\t// The following properties artificially restrict the inputs\n"
|
|
"\t// to this long binary multiplier to only those values whose\n"
|
|
"\t// absolute value is 0..7. It is used by the formal proof of\n"
|
|
"\t// the BUTTERFLY to artificially limit the scope of the proof.\n"
|
|
"\t// By the time the butterfly sees this code, it will be known\n"
|
|
"\t// that the long binary multiply works. At issue will no longer\n"
|
|
"\t// be whether or not this works, but rather whether it works in\n"
|
|
"\t// context. For that purpose, we'll need to check timing, not\n"
|
|
"\t// results. Checking against inputs of +/- 1 and 0 are perfect\n"
|
|
"\t// for that task. The below assumptions (yes they are assumptions\n"
|
|
"\t// just go a little bit further.\n"
|
|
"\t//\n"
|
|
"\t// THEREFORE, THESE PROPERTIES ARE NOT NECESSARY TO PROVING THAT\n"
|
|
"\t// THIS MODULE WORKS, AND THEY WILL INTERFERE WITH THAT PROOF.\n"
|
|
"\t//\n"
|
|
"\t// This just limits the proof for the butterfly, the parent.\n"
|
|
"\t// module that calls this one\n"
|
|
"\t//\n"
|
|
"\t// Start by assuming that all inputs have an absolute value less\n"
|
|
"\t// than eight.\n"
|
|
"\talways @(*)\n"
|
|
"\t\tassume(u_a[AW-1:3] == 0);\n"
|
|
"\talways @(*)\n"
|
|
"\t\tassume(u_b[BW-1:3] == 0);\n"
|
|
"\n"
|
|
"\t// If the inputs have these properties, then so too do many of\n"
|
|
"\t// our internal values. ASSERT therefore that we never get out\n"
|
|
"\t// of bounds\n"
|
|
"\tgenerate for(k=0; k<TLEN; k=k+1)\n"
|
|
"\tbegin\n"
|
|
"\t\talways @(*)\n"
|
|
"\t\tbegin\n"
|
|
"\t\t\tassert(f_past_a[k][AW-1:3] == 0);\n"
|
|
"\t\t\tassert(f_past_b[k][BW-1:3] == 0);\n"
|
|
"\t\tend\n"
|
|
"\tend endgenerate\n"
|
|
"\n"
|
|
"\tgenerate for(k=0; k<TLEN-1; k=k+1)\n"
|
|
"\tbegin\n"
|
|
"\t\talways @(*)\n"
|
|
"\t\t\tassert(acc[k][IW+BW-1:6] == 0);\n"
|
|
"\tend endgenerate\n"
|
"\n"
|
"\n"
|
|
"\tgenerate for(k=0; k<TLEN-2; k=k+1)\n"
|
|
"\tbegin\n"
|
|
"\t\talways @(*)\n"
|
|
"\t\t\tassert(r_b[k][BW-1:3] == 0);\n"
|
|
"\tend endgenerate\n"
|
|
"`endif // BUTTERFLY\n");
|
|
|
|
|
|
} else {
|
|
fprintf(fp, "// Formal properties have not been enabled\n");
|
|
}
|
|
|
|
fprintf(fp,
|
|
"`endif\t// FORMAL\n"
|
"endmodule\n");
|
"endmodule\n");
|
|
|
fclose(fp);
|
fclose(fp);
|
}
|
}
|
|
|
