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

Subversion Repositories dblclockfft

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /
    from Rev 36 to Rev 37
    ↔ Reverse comparison
  •

Rev 36 → Rev 37

/dblclockfft/trunk/sw/Makefile
1,8 → 1,8
############################################################################/
################################################################################
##
## Filename: Makefile
##
## Project: A Generic Pipelined FFT Implementation
## Project: A General Purpose Pipelined FFT Implementation
##
## Purpose: This is the main Makefile for the FFT core generator.
## It is very simple in its construction, the most complicated
16,7 → 16,7
## Creator: Dan Gisselquist, Ph.D.
## Gisselquist Technology, LLC
##
##########################################################################/
################################################################################
##
## Copyright (C) 2015,2018, Gisselquist Technology, LLC
##
31,15 → 31,15
## for more details.
##
## 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
## <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,
## http:##www.gnu.org/licenses/gpl.html
## http://www.gnu.org/licenses/gpl.html
##
##
##########################################################################/
################################################################################
##
##
# This is really simple ...
51,8 → 51,8
SOURCES := bitreverse.cpp bldstage.cpp butterfly.cpp fftgen.cpp fftlib.cpp \
legal.cpp rounding.cpp softmpy.cpp
TESTSZ := -f 2048
# CKPCE := -k 1
CKPCE := -2
CKPCE := -1 -k 1
# CKPCE := -2
MPYS := -p 0
IWID := -n 15
FFTPARAMS := -d $(CORED) $(TESTSZ) $(CKPCE) $(MPYS) $(IWID)
218,13 → 218,16
 
.PHONY: clean
clean:
rm fftgen fftgen.o
rm -rf fft-core/
rm -rf fftgen $(OBJDIR)/
rm -rf $(CORED)/obj_dir
rm -rf $(CORED)/fftmain.v $(CORED)/fftstage.v
rm -rf $(CORED)/ifftmain.v $(CORED)/ifftstage.v
rm -rf $(CORED)/qtrstage.v $(CORED)/laststage.v $(CORED)/bitreverse.v
rm -rf $(CORED)/butterfly.v $(CORED)/hwbfly.v
rm -rf $(CORED)/longbimpy.v $(CORED)/bimpy.v
rm -rf $(CORED)/convround.v
rm -rf $(CORED)/*cmem_*.hex
 
#
# The "depends" target, to know what files things depend upon. The depends
259,4 → 262,6
@echo "Generating tags"
@ctags $(SOURCES) $(HEADERS)
 
ifneq ($(MAKECMDGOALS),clean)
-include $(OBJDIR)/depends.txt
endif
/dblclockfft/trunk/sw/bitreverse.cpp
24,7 → 24,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
98,9 → 98,9
fprintf(fp,
"module %s(i_clk, %s, i_ce, i_in, o_out, o_sync);\n"
"\tparameter\t\t\tLGSIZE=%d, WIDTH=24;\n"
"\tinput\t\t\t\ti_clk, %s, i_ce;\n"
"\tinput\t\t[(2*WIDTH-1):0]\ti_in;\n"
"\toutput\twire\t[(2*WIDTH-1):0]\to_out;\n"
"\tinput\twire\t\t\ti_clk, %s, i_ce;\n"
"\tinput\twire\t[(2*WIDTH-1):0]\ti_in;\n"
"\toutput\treg\t[(2*WIDTH-1):0]\to_out;\n"
"\toutput\treg\t\t\to_sync;\n", modulename, resetw.c_str(),
TST_DBLREVERSE_LGSIZE,
resetw.c_str());
113,8 → 113,9
"\n"
" genvar k;\n"
" generate for(k=0; k<LGSIZE; k=k+1)\n"
" begin : DBL\n"
" assign rdaddr[k] = wraddr[LGSIZE-1-k];\n"
" endgenerate\n"
" end endgenerate\n"
" assign rdaddr[LGSIZE] = !wraddr[LGSIZE];\n"
"\n"
" reg in_reset;\n"
164,9 → 165,9
if (formal_property_flag) {
fprintf(fp,
"`ifdef\tFORMAL\n"
"`define\tASSERT assert\n"
"`ifdef BITREVERSE\n"
"`define\tASSUME assume\n"
"`define\tASSERT assert\n");
"`define\tASSUME assume\n");
if (async_reset)
fprintf(fp,
"\n\talways @($global_clock)\n"
175,7 → 176,6
fprintf(fp,
"`else\n"
"`define\tASSUME assert\n"
"`define\tASSERT assume\n"
"`endif\n"
"\n"
"\treg f_past_valid;\n"
393,8 → 393,8
"module %s(i_clk, %s, i_ce, i_in_0, i_in_1,\n"
"\t\to_out_0, o_out_1, o_sync);\n"
"\tparameter\t\t\tLGSIZE=%d, WIDTH=24;\n"
"\tinput\t\t\t\ti_clk, %s, i_ce;\n"
"\tinput\t\t[(2*WIDTH-1):0]\ti_in_0, i_in_1;\n"
"\tinput\twire\t\t\ti_clk, %s, i_ce;\n"
"\tinput\twire\t[(2*WIDTH-1):0]\ti_in_0, i_in_1;\n"
"\toutput\twire\t[(2*WIDTH-1):0]\to_out_0, o_out_1;\n"
"\toutput\treg\t\t\to_sync;\n", modulename,
resetw.c_str(), TST_DBLREVERSE_LGSIZE, resetw.c_str());
466,9 → 466,9
if (formal_property_flag) {
fprintf(fp,
"`ifdef\tFORMAL\n"
"`define\tASSERT assert\n"
"`ifdef BITREVERSE\n"
"`define\tASSUME assume\n"
"`define\tASSERT assert\n");
"`define\tASSUME assume\n");
if (async_reset)
fprintf(fp,
"\n\talways @($global_clock)\n"
477,7 → 477,6
fprintf(fp,
"`else\n"
"`define\tASSUME assert\n"
"`define\tASSERT assume\n"
"`endif\n"
"\n"
"\treg f_past_valid;\n"
/dblclockfft/trunk/sw/bitreverse.h
24,7 → 24,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/bldstage.cpp
4,7 → 4,11
//
// Project: A General Purpose Pipelined FFT Implementation
//
// Purpose:
// Purpose: Builds the logic necessary to implement a single stage of an
// FFT. This includes referencing the butterfly, but not the
// actual butterflies themselves. Further, this file only contains the
// code for the general case of an FFT stage: the special cases of the
// two final stages are described in other files.
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
24,7 → 28,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
63,6 → 67,10
#include "rounding.h"
#include "bldstage.h"
 
//
// Builds the penultimate FFT stage, using integer operations only.
// This stage is called laststage elsewhere.
//
void build_dblstage(const char *fname, ROUND_T rounding,
const bool async_reset, const bool dbg) {
FILE *fp = fopen(fname, "w");
147,8 → 155,8
fprintf(fp,
"module\tlaststage%s(i_clk, %s, i_ce, i_sync, i_left, i_right, o_left, o_right, o_sync%s);\n"
"\tparameter\tIWIDTH=%d,OWIDTH=IWIDTH+1, SHIFT=%d;\n"
"\tinput\t\ti_clk, %s, i_ce, i_sync;\n"
"\tinput\t\t[(2*IWIDTH-1):0]\ti_left, i_right;\n"
"\tinput\twire\ti_clk, %s, i_ce, i_sync;\n"
"\tinput\twire\t[(2*IWIDTH-1):0]\ti_left, i_right;\n"
"\toutput\treg\t[(2*OWIDTH-1):0]\to_left, o_right;\n"
"\toutput\treg\t\t\to_sync;\n"
"\n", (dbg)?"_dbg":"", resetw.c_str(), (dbg)?", o_dbg":"",
186,9 → 194,9
"\tinitial\tr_sync = 1\'b0; // Sync coming out\n",
resetw.c_str());
if (async_reset)
fprintf(fp, "\talways @(posedge i_clk, negdge i_areset_n)\n\t\tif (!i_areset_n)\n");
fprintf(fp, "\talways @(posedge i_clk, negdge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fp, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fp, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fp,
"\t\tbegin\n"
"\t\t\trnd_sync <= 1\'b0;\n"
251,7 → 259,7
if (async_reset)
fprintf(fp, "\talways @(posedge i_clk, negdge i_areset_n)\n\t\tif (!i_areset_n)\n");
else
fprintf(fp, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fp, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fp,
"\t\t\to_sync <= 1\'b0;\n"
"\t\telse if (i_ce)\n"
332,9 → 340,9
"\t// core is built ... Note that the minimum LGSPAN (the base two log\n"
"\t// of the span, or the base two log of the current FFT size) is 3.\n"
"\t// Smaller spans (i.e. the span of 2) must use the dbl laststage module.\n"
"\tparameter\tLGWIDTH=%d, LGSPAN=%d, BFLYSHIFT=0;\n"
"\tparameter\tLGSPAN=%d, BFLYSHIFT=0; // LGWIDTH=%d\n"
"\tparameter\t[0:0] OPT_HWMPY = 1;\n",
lgval(stage), (nwide <= 1) ? lgval(stage)-1 : lgval(stage)-2);
(nwide <= 1) ? lgval(stage)-1 : lgval(stage)-2, lgval(stage));
fprintf(fstage,
"\t// Clocks per CE. If your incoming data rate is less than 50%% of your\n"
"\t// clock speed, you can set CKPCE to 2\'b10, make sure there's at least\n"
363,8 → 371,8
"`endif // VERILATOR\n\n");
 
fprintf(fstage,
"\tinput i_clk, %s, i_ce, i_sync;\n"
"\tinput [(2*IWIDTH-1):0] i_data;\n"
"\tinput wire i_clk, %s, i_ce, i_sync;\n"
"\tinput wire [(2*IWIDTH-1):0] i_data;\n"
"\toutput reg [(2*OWIDTH-1):0] o_data;\n"
"\toutput reg o_sync;\n"
"\n", resetw.c_str());
374,14 → 382,17
"\n");
}
fprintf(fstage,
"\treg wait_for_sync;\n"
"\treg [(2*IWIDTH-1):0] ib_a, ib_b;\n"
"\treg [(2*CWIDTH-1):0] ib_c;\n"
"\treg ib_sync;\n"
"\t// I am using the prefixes\n"
"\t// ib_* to reference the inputs to the butterfly, and\n"
"\t// ob_* to reference the outputs from the butterfly\n"
"\treg wait_for_sync;\n"
"\treg [(2*IWIDTH-1):0] ib_a, ib_b;\n"
"\treg [(2*CWIDTH-1):0] ib_c;\n"
"\treg ib_sync;\n"
"\n"
"\treg b_started;\n"
"\twire ob_sync;\n"
"\twire [(2*OWIDTH-1):0]\tob_a, ob_b;\n");
"\treg b_started;\n"
"\twire ob_sync;\n"
"\twire [(2*OWIDTH-1):0]\tob_a, ob_b;\n");
fprintf(fstage,
"\n"
"\t// cmem is defined as an array of real and complex values,\n"
391,9 → 402,17
"\t// cmem[i] = { (2^(CWIDTH-2)) * cos(2*pi*i/(2^LGWIDTH)),\n"
"\t// (2^(CWIDTH-2)) * sin(2*pi*i/(2^LGWIDTH)) };\n"
"\t//\n"
"\treg [(2*CWIDTH-1):0] cmem [0:((1<<LGSPAN)-1)];\n"
"\tinitial\t$readmemh(COEFFILE,cmem);\n\n");
"\treg [(2*CWIDTH-1):0] cmem [0:((1<<LGSPAN)-1)];\n");
 
if (formal_property_flag)
fprintf(fstage,
"`ifdef FORMAL\n"
"// Let the formal tool pick the coefficients\n"
"`else\n");
fprintf(fstage, "\tinitial\t$readmemh(COEFFILE,cmem);\n\n");
if (formal_property_flag)
fprintf(fstage, "`endif\n\n");
 
// gen_coeff_file(coredir, fname, stage, cbits, nwide, offset, inv);
 
fprintf(fstage,
400,20 → 419,20
"\treg [(LGSPAN):0] iaddr;\n"
"\treg [(2*IWIDTH-1):0] imem [0:((1<<LGSPAN)-1)];\n"
"\n"
"\treg [LGSPAN:0] oB;\n"
"\treg [LGSPAN:0] oaddr;\n"
"\treg [(2*OWIDTH-1):0] omem [0:((1<<LGSPAN)-1)];\n"
"\n"
"\tinitial wait_for_sync = 1\'b1;\n"
"\tinitial iaddr = 0;\n");
if (async_reset)
fprintf(fstage, "\talways @(posedge i_clk, negedge i_areset_n)\n\t\tif (!i_areset_n)\n");
fprintf(fstage, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fstage, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fstage, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
 
fprintf(fstage,
"\tbegin\n"
"\t\t\twait_for_sync <= 1\'b1;\n"
"\t\t\tiaddr <= 0;\n"
"\t\twait_for_sync <= 1\'b1;\n"
"\t\tiaddr <= 0;\n"
"\tend else if ((i_ce)&&((!wait_for_sync)||(i_sync)))\n"
"\tbegin\n"
"\t\t//\n"
431,6 → 450,9
"\t//\n"
"\t// Now, we have all the inputs, so let\'s feed the butterfly\n"
"\t//\n"
"\t// ib_sync is the synchronization bit to the butterfly. It will\n"
"\t// be tracked within the butterfly, and used to create the o_sync\n"
"\t// value when the results from this output are produced\n"
"\tinitial ib_sync = 1\'b0;\n");
if (async_reset)
fprintf(fstage, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
445,6 → 467,8
"\t\t// first valid data out per FFT.\n"
"\t\tib_sync <= (iaddr==(1<<(LGSPAN)));\n"
"\tend\n\n"
"\t// Read the values from our input memory, and use them to feed first of two\n"
"\t// butterfly inputs\n"
"\talways\t@(posedge i_clk)\n"
"\tif (i_ce)\n"
"\tbegin\n"
480,6 → 504,15
"\t\talways @(*) idle = 0;\n\n"
"\tend endgenerate\n\n");
 
if (formal_property_flag)
fprintf(fstage,
"// For the formal proof, we'll assume the outputs of hwbfly and/or\n"
"// butterfly, rather than actually calculating them. This will simplify\n"
"// the proof and (if done properly) will be equivalent. Be careful of\n"
"// defining FORMAL if you want the full logic!\n"
"`ifndef FORMAL\n"
"\t//\n");
 
fprintf(fstage,
"\tgenerate if (OPT_HWMPY)\n"
"\tbegin : HWBFLY\n"
499,51 → 532,256
"\t\t\t\t\t(idle||(!i_ce))?0:ib_b,\n"
"\t\t\t\t\t(ib_sync&&i_ce),\n"
"\t\t\t\t\tob_a, ob_b, ob_sync);\n"
"\tend endgenerate\n\n",
"\tend endgenerate\n",
resetw.c_str(), resetw.c_str());
 
if (formal_property_flag)
fprintf(fstage, "`endif\n\n");
 
fprintf(fstage,
"\t//\n"
"\t// Next step: recover the outputs from the butterfly\n"
"\t//\n"
"\tinitial oB = 0;\n"
"\t// The first output can go immediately to the output of this routine\n"
"\t// The second output must wait until this time in the idle cycle\n"
"\t// oaddr is the output memory address, keeping track of where we are\n"
"\t// in this output cycle.\n"
"\tinitial oaddr = 0;\n"
"\tinitial o_sync = 0;\n"
"\tinitial b_started = 0;\n");
if (async_reset)
fprintf(fstage, "\talways @(posedge i_clk, negedge i_areset_n)\n\t\tif (!i_areset_n)\n");
fprintf(fstage, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fstage, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fstage, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fstage,
"\tbegin\n"
"\t\toB <= 0;\n"
"\t\to_sync <= 0;\n"
"\t\toaddr <= 0;\n"
"\t\to_sync <= 0;\n"
"\t\t// b_started will be true once we've seen the first ob_sync\n"
"\t\tb_started <= 0;\n"
"\tend else if (i_ce)\n"
"\tbegin\n"
"\t\to_sync <= (!oB[LGSPAN])?ob_sync : 1\'b0;\n"
"\t\to_sync <= (!oaddr[LGSPAN])?ob_sync : 1\'b0;\n"
"\t\tif (ob_sync||b_started)\n"
"\t\t\toB <= oB + { {(LGSPAN){1\'b0}}, 1\'b1 };\n"
"\t\tif ((ob_sync)&&(!oB[LGSPAN]))\n"
"\t\t// A butterfly output is available\n"
"\t\t\toaddr <= oaddr + 1\'b1;\n"
"\t\tif ((ob_sync)&&(!oaddr[LGSPAN]))\n"
"\t\t\t// If b_started is true, then a butterfly output is available\n"
"\t\t\tb_started <= 1\'b1;\n"
"\tend\n\n");
fprintf(fstage,
"\treg [(LGSPAN-1):0]\t\tdly_addr;\n"
"\treg [(2*OWIDTH-1):0]\tdly_value;\n"
"\treg [(LGSPAN-1):0]\t\tnxt_oaddr;\n"
"\treg [(2*OWIDTH-1):0]\tpre_ovalue;\n"
"\talways @(posedge i_clk)\n"
"\tif (i_ce)\n"
"\t\tnxt_oaddr[0] <= oaddr[0];\n"
"\tgenerate if (LGSPAN>1)\n"
"\tbegin\n"
"\t\tdly_addr <= oB[(LGSPAN-1):0];\n"
"\t\tdly_value <= ob_b;\n"
"\tend\n"
"\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\tnxt_oaddr[LGSPAN-1:1] <= oaddr[LGSPAN-1:1] + 1\'b1;\n"
"\n"
"\tend endgenerate\n"
"\n"
"\t// Only write to the memory on the first half of the outputs\n"
"\t// We'll use the memory value on the second half of the outputs\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(!oaddr[LGSPAN]))\n"
"\t\tomem[oaddr[(LGSPAN-1):0]] <= ob_b;\n\n");
 
fprintf(fstage,
"\talways @(posedge i_clk)\n"
"\tif (i_ce)\n"
"\t\tomem[dly_addr] <= dly_value;\n"
"\t\tpre_ovalue <= omem[nxt_oaddr[(LGSPAN-1):0]];\n"
"\n");
fprintf(fstage,
"\talways @(posedge i_clk)\n"
"\tif (i_ce)\n"
"\t\to_data <= (!oB[LGSPAN])?ob_a : omem[oB[(LGSPAN-1):0]];\n"
"\t\to_data <= (!oaddr[LGSPAN]) ? ob_a : pre_ovalue;\n"
"\n");
 
fprintf(fstage,
"`ifdef FORMAL\n");
 
 
if (formal_property_flag) {
 
fprintf(fstage,
"\t// An arbitrary processing delay from butterfly input to\n"
"\t// butterfly output(s)\n"
"\t(* anyconst *) reg [LGSPAN:0] f_mpydelay;\n"
"\talways @(*)\n"
"\t\tassume(f_mpydelay > 1);\n"
"\n"
"\treg f_past_valid;\n"
"\tinitial f_past_valid = 1'b0;\n"
"\talways @(posedge i_clk)\n"
"\t\tf_past_valid <= 1'b1;\n"
"\n");
 
if (async_reset)
fprintf(fstage, "\talways @(*)\n\tif ((!f_past_valid)||(!i_areset_n))\n");
else
fprintf(fstage, "\talways @(posedge i_clk)\n"
"\tif ((!f_past_valid)||($past(i_reset)))\n");
fprintf(fstage,
"\tbegin\n"
"\t\tassert(iaddr == 0);\n"
"\t\tassert(wait_for_sync);\n"
"\t\tassert(o_sync == 0);\n"
"\t\tassert(oaddr == 0);\n"
"\t\tassert(!b_started);\n"
"\t\tassert(!o_sync);\n"
"\tend\n\n");
 
fprintf(fstage,
"\t/////////////////////////////////////////\n"
"\t//\n"
"\t// Formally verify the input half, from the inputs to this module\n"
"\t// to the inputs of the butterfly\n"
"\t//\n"
"\t/////////////////////////////////////////\n"
"\t//\n"
"\t// Let's verify a specific set of inputs\n"
"\t(* anyconst *) reg [LGSPAN:0] f_addr;\n"
"\treg [2*IWIDTH-1:0] f_left, f_right;\n"
"\twire [LGSPAN:0] f_next_addr;\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((!$past(i_ce))&&(!$past(i_ce,2))&&(!$past(i_ce,3))&&(!$past(i_ce,4)))\n"
"\tassume(!i_ce);\n"
"\n"
"\talways @(*)\n"
"\t\tassume(f_addr[LGSPAN]==1'b0);\n"
"\n"
"\tassign\tf_next_addr = f_addr + 1'b1;\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(iaddr[LGSPAN:0] == f_addr))\n"
"\t\tf_left <= i_data;\n"
"\n"
"\talways @(*)\n"
"\tif (wait_for_sync)\n"
"\t\tassert(iaddr == 0);\n"
"\n"
"\twire [LGSPAN:0]\tf_last_addr = iaddr - 1'b1;\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((!wait_for_sync)&&(f_last_addr >= { 1'b0, f_addr[LGSPAN-1:0]}))\n"
"\t\tassert(f_left == imem[f_addr[LGSPAN-1:0]]);\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(iaddr == { 1'b1, f_addr[LGSPAN-1:0]}))\n"
"\t\tf_right <= i_data;\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(!wait_for_sync)&&(f_last_addr == { 1'b1, f_addr[LGSPAN-1:0]}))\n"
"\tbegin\n"
"\t\tassert(ib_a == f_left);\n"
"\t\tassert(ib_b == f_right);\n"
"\t\tassert(ib_c == cmem[f_addr[LGSPAN-1:0]]);\n"
"\tend\n\n");
 
fprintf(fstage,
"\t/////////////////////////////////////////\n"
"\t//\n"
"\t// Formally verify the output half, from the output of the butterfly\n"
"\t// to the outputs of this module\n"
"\t//\n"
"\t/////////////////////////////////////////\n"
"\treg [2*OWIDTH-1:0] f_oleft, f_oright;\n"
"\treg [LGSPAN:0] f_oaddr;\n"
"\twire [LGSPAN:0] f_oaddr_m1 = f_oaddr - 1'b1;\n\n");
 
fprintf(fstage,
"\talways @(*)\n"
"\t\tf_oaddr = iaddr - f_mpydelay + {1'b1,{(LGSPAN-1){1'b0}}};\n"
"\n"
"\tassign\tf_oaddr_m1 = f_oaddr - 1'b1;\n"
"\n");
 
fprintf(fstage,
"\treg f_output_active;\n"
"\tinitial\tf_output_active = 1'b0;\n");
if (async_reset)
fprintf(fstage, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fstage, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fstage,
"\t\tf_output_active <= 1'b0;\n"
"\telse if ((i_ce)&&(ob_sync))\n"
"\t\tf_output_active <= 1'b1;\n"
"\n"
"\talways @(*)\n"
"\t\tassert(f_output_active == b_started);\n"
"\n"
"\talways @(*)\n"
"\tif (wait_for_sync)\n"
"\t\tassert(!f_output_active);\n\n");
 
fprintf(fstage,
"\talways @(*)\n"
"\tif (f_output_active)\n"
"\t\tassert(oaddr == f_oaddr);\n"
"\telse\n"
"\t\tassert(oaddr == 0);\n"
"\n");
 
 
fprintf(fstage,
"\talways @(*)\n"
"\tif (wait_for_sync)\n"
"\t\tassume(!ob_sync);\n"
"\n"
"\talways @(*)\n"
"\t\tassume(ob_sync == (f_oaddr == 0));\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((f_past_valid)&&(!$past(i_ce)))\n"
"\tbegin\n"
"\t\tassume($stable(ob_a));\n"
"\t\tassume($stable(ob_b));\n"
"\tend\n\n");
 
fprintf(fstage,
"\tinitial f_oleft = 0;\n"
"\tinitial f_oright = 0;\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(f_oaddr == f_addr))\n"
"\tbegin\n"
"\t\tf_oleft <= ob_a;\n"
"\t\tf_oright <= ob_b;\n"
"\tend\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((f_output_active)&&(f_oaddr_m1 >= { 1'b0, f_addr[LGSPAN-1:0]}))\n"
"\t\tassert(omem[f_addr[LGSPAN-1:0]] == f_oright);\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(f_oaddr_m1 == 0)&&(f_output_active))\n"
"\t\tassert(o_sync);\n"
"\telse if ((i_ce)||(!f_output_active))\n"
"\t\tassert(!o_sync);\n"
"\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(f_output_active)&&(f_oaddr_m1 == f_addr))\n"
"\t\tassert(o_data == f_oleft);\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(f_output_active)&&(f_oaddr[LGSPAN])\n"
"\t\t\t&&(f_oaddr[LGSPAN-1:0] == f_addr[LGSPAN-1:0]))\n"
"\t\tassert(pre_ovalue == f_oright);\n"
"\talways @(posedge i_clk)\n"
"\tif ((i_ce)&&(f_output_active)&&(f_oaddr_m1[LGSPAN])\n"
"\t\t\t&&(f_oaddr_m1[LGSPAN-1:0] == f_addr[LGSPAN-1:0]))\n"
"\t\tassert(o_data == f_oright);\n"
"\n");
} else { // If no formal properties
fprintf(fstage, "// Formal properties exist, but are not enabled"
" in this build\n");
} // End of the formal properties section
 
fprintf(fstage,
"`endif\n");
 
fprintf(fstage, "endmodule\n");
}
/dblclockfft/trunk/sw/bldstage.h
24,7 → 24,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/butterfly.cpp
4,7 → 4,9
//
// Project: A General Purpose Pipelined FFT Implementation
//
// Purpose:
// Purpose: Builds one of two butterflies: either a butterfly implementation
// using hardware optimized multiplies, or one that uses a logic
// soft-multiply.
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
13,23 → 15,25
//
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// This file is part of the general purpose pipelined FFT project.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
// The pipelined FFT project is free software (firmware): you can redistribute
// it and/or modify it under the terms of the GNU Lesser General Public License
// as published by the Free Software Foundation, either version 3 of the
// License, or (at your option) any later version.
//
// 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
// target there if the PDF file isn't present.) If not, see
// The pipelined FFT project is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser
// General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along 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
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
258,12 → 262,46
 
 
fprintf(fp,
"\tinput\t\ti_clk, %s, i_ce;\n"
"\tinput\t\t[(2*CWIDTH-1):0] i_coef;\n"
"\tinput\t\t[(2*IWIDTH-1):0] i_left, i_right;\n"
"\tinput\t\ti_aux;\n"
"\tinput\twire\ti_clk, %s, i_ce;\n"
"\tinput\twire\t[(2*CWIDTH-1):0] i_coef;\n"
"\tinput\twire\t[(2*IWIDTH-1):0] i_left, i_right;\n"
"\tinput\twire\ti_aux;\n"
"\toutput\twire [(2*OWIDTH-1):0] o_left, o_right;\n"
"\toutput\treg\to_aux;\n\n", resetw.c_str());
 
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\tlocalparam F_LGDEPTH = (AUXLEN > 64) ? 7\n"
"\t\t\t: (AUXLEN > 32) ? 6\n"
"\t\t\t: (AUXLEN > 16) ? 5\n"
"\t\t\t: (AUXLEN > 8) ? 4\n"
"\t\t\t: (AUXLEN > 4) ? 3 : 2;\n"
"\n"
"\tlocalparam F_DEPTH = AUXLEN;\n"
"\tlocalparam [F_LGDEPTH-1:0] F_D = F_DEPTH[F_LGDEPTH-1:0]-1;\n"
"\n"
"\treg signed [IWIDTH-1:0] f_dlyleft_r [0:F_DEPTH-1];\n"
"\treg signed [IWIDTH-1:0] f_dlyleft_i [0:F_DEPTH-1];\n"
"\treg signed [IWIDTH-1:0] f_dlyright_r [0:F_DEPTH-1];\n"
"\treg signed [IWIDTH-1:0] f_dlyright_i [0:F_DEPTH-1];\n"
"\treg signed [CWIDTH-1:0] f_dlycoeff_r [0:F_DEPTH-1];\n"
"\treg signed [CWIDTH-1:0] f_dlycoeff_i [0:F_DEPTH-1];\n"
"\treg signed [F_DEPTH-1:0] f_dlyaux;\n"
"\n"
"\twire signed [IWIDTH:0] f_predifr, f_predifi;\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_predifrx, f_predifix;\n"
"\twire signed [CWIDTH:0] f_sumcoef;\n"
"\twire signed [IWIDTH+1:0] f_sumdiff;\n"
"\twire signed [IWIDTH:0] f_sumr, f_sumi;\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_sumrx, f_sumix;\n"
"\twire signed [IWIDTH:0] f_difr, f_difi;\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_difrx, f_difix;\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_widecoeff_r, f_widecoeff_i;\n"
"\n"
"\twire [(CWIDTH):0] fp_one_ic, fp_two_ic, fp_three_ic, f_p3c_in;\n"
"\twire [(IWIDTH+1):0] fp_one_id, fp_two_id, fp_three_id, f_p3d_in;\n"
"`endif\n\n");
 
fprintf(fp,
"\treg\t[(2*IWIDTH-1):0]\tr_left, r_right;\n"
"\treg\t[(2*CWIDTH-1):0]\tr_coef, r_coef_2;\n"
283,20 → 321,20
fprintf(fp,
"\t// Set up the input to the multiply\n"
"\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\tbegin\n"
"\t\t\t// One clock just latches the inputs\n"
"\t\t\tr_left <= i_left; // No change in # of bits\n"
"\t\t\tr_right <= i_right;\n"
"\t\t\tr_coef <= i_coef;\n"
"\t\t\t// Next clock adds/subtracts\n"
"\t\t\tr_sum_r <= r_left_r + r_right_r; // Now IWIDTH+1 bits\n"
"\t\t\tr_sum_i <= r_left_i + r_right_i;\n"
"\t\t\tr_dif_r <= r_left_r - r_right_r;\n"
"\t\t\tr_dif_i <= r_left_i - r_right_i;\n"
"\t\t\t// Other inputs are simply delayed on second clock\n"
"\t\t\tr_coef_2<= r_coef;\n"
"\t\tend\n"
"\tif (i_ce)\n"
"\tbegin\n"
"\t\t// One clock just latches the inputs\n"
"\t\tr_left <= i_left; // No change in # of bits\n"
"\t\tr_right <= i_right;\n"
"\t\tr_coef <= i_coef;\n"
"\t\t// Next clock adds/subtracts\n"
"\t\tr_sum_r <= r_left_r + r_right_r; // Now IWIDTH+1 bits\n"
"\t\tr_sum_i <= r_left_i + r_right_i;\n"
"\t\tr_dif_r <= r_left_r - r_right_r;\n"
"\t\tr_dif_i <= r_left_i - r_right_i;\n"
"\t\t// Other inputs are simply delayed on second clock\n"
"\t\tr_coef_2<= r_coef;\n"
"\tend\n"
"\n");
fprintf(fp,
"\t// Don\'t forget to record the even side, since it doesn\'t need\n"
304,20 → 342,20
"\t// with the answer when it is ready.\n"
"\tinitial fifo_addr = 0;\n");
if (async_reset)
fprintf(fp, "\talways @(posedge i_clk, negedge i_areset_n)\n\t\tif (!i_areset_n)\n");
fprintf(fp, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fp, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fp, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fp,
"\t\t\tfifo_addr <= 0;\n"
"\t\telse if (i_ce)\n"
"\t\t\t// Need to delay the sum side--nothing else happens\n"
"\t\t\t// to it, but it needs to stay synchronized with the\n"
"\t\t\t// right side.\n"
"\t\t\tfifo_addr <= fifo_addr + 1;\n"
"\t\tfifo_addr <= 0;\n"
"\telse if (i_ce)\n"
"\t\t// Need to delay the sum side--nothing else happens\n"
"\t\t// to it, but it needs to stay synchronized with the\n"
"\t\t// right side.\n"
"\t\tfifo_addr <= fifo_addr + 1;\n"
"\n"
"\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\tfifo_left[fifo_addr] <= { r_sum_r, r_sum_i };\n"
"\tif (i_ce)\n"
"\t\tfifo_left[fifo_addr] <= { r_sum_r, r_sum_i };\n"
"\n"
"\twire\tsigned\t[(CWIDTH-1):0] ir_coef_r, ir_coef_i;\n"
"\tassign\tir_coef_r = r_coef_2[(2*CWIDTH-1):CWIDTH];\n"
372,12 → 410,30
"\t\t// simpler, multiply.\n"
"\t\tlongbimpy #(CWIDTH+1,IWIDTH+2) p1(i_clk, i_ce,\n"
"\t\t\t\t{ir_coef_r[CWIDTH-1],ir_coef_r},\n"
"\t\t\t\t{r_dif_r[IWIDTH],r_dif_r}, p_one);\n"
"\t\t\t\t{r_dif_r[IWIDTH],r_dif_r}, p_one");
if (formal_property_flag) fprintf(fp,
"\n`ifdef\tFORMAL\n"
"\t\t\t\t, fp_one_ic, fp_one_id\n"
"`endif\n"
"\t\t\t");
fprintf(fp, ");\n"
"\t\tlongbimpy #(CWIDTH+1,IWIDTH+2) p2(i_clk, i_ce,\n"
"\t\t\t\t{ir_coef_i[CWIDTH-1],ir_coef_i},\n"
"\t\t\t\t{r_dif_i[IWIDTH],r_dif_i}, p_two);\n"
"\t\t\t\t{r_dif_i[IWIDTH],r_dif_i}, p_two");
if (formal_property_flag) fprintf(fp,
"\n`ifdef\tFORMAL\n"
"\t\t\t\t, fp_two_ic, fp_two_id\n"
"`endif\n"
"\t\t\t");
fprintf(fp, ");\n"
"\t\tlongbimpy #(CWIDTH+1,IWIDTH+2) p3(i_clk, i_ce,\n"
"\t\t\t\tp3c_in, p3d_in, p_three);\n"
"\t\t\t\tp3c_in, p3d_in, p_three");
if (formal_property_flag) fprintf(fp,
"\n`ifdef\tFORMAL\n"
"\t\t\t\t, fp_three_ic, fp_three_id\n"
"`endif\n"
"\t\t\t");
fprintf(fp, ");\n"
"\n");
 
///////////////////////////////////////////
405,7 → 461,21
"\n"
"\t\treg signed [(CWIDTH+IWIDTH+3)-1:0] mpy_pipe_out;\n"
"\t\treg signed [IWIDTH+CWIDTH+3-1:0] longmpy;\n"
"\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\twire [CWIDTH:0] f_past_ic;\n"
"\t\twire [IWIDTH+1:0] f_past_id;\n"
"\t\twire [CWIDTH:0] f_past_mux_ic;\n"
"\t\twire [IWIDTH+1:0] f_past_mux_id;\n"
"\n"
"\t\treg [CWIDTH:0] f_rpone_ic, f_rptwo_ic, f_rpthree_ic,\n"
"\t\t\t\t\tf_rp2one_ic, f_rp2two_ic, f_rp2three_ic;\n"
"\t\treg [IWIDTH+1:0] f_rpone_id, f_rptwo_id, f_rpthree_id,\n"
"\t\t\t\t\tf_rp2one_id, f_rp2two_id, f_rp2three_id;\n"
"`endif\n\n");
 
fprintf(fp,
"\n"
"\t\tinitial ce_phase = 1'b0;\n"
"\t\talways @(posedge i_clk)\n"
440,7 → 510,12
"\n");
fprintf(fp,
"\t\tlongbimpy #(CWIDTH+1,IWIDTH+2) mpy0(i_clk, mpy_pipe_v,\n"
"\t\t\t\tmpy_cof_sum, mpy_dif_sum, longmpy);\n"
"\t\t\t\tmpy_cof_sum, mpy_dif_sum, longmpy\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\t\t, f_past_ic, f_past_id\n"
"`endif\n");
fprintf(fp,"\t\t\t);\n"
"\n");
 
fprintf(fp,
447,7 → 522,13
"\t\tlongbimpy #(CWIDTH+1,IWIDTH+2) mpy1(i_clk, mpy_pipe_v,\n"
"\t\t\t\t{ mpy_pipe_vc[CWIDTH-1], mpy_pipe_vc },\n"
"\t\t\t\t{ mpy_pipe_vd[IWIDTH ], mpy_pipe_vd },\n"
"\t\t\t\tmpy_pipe_out);\n\n");
"\t\t\t\tmpy_pipe_out\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\t\t, f_past_mux_ic, f_past_mux_id\n"
"`endif\n");
fprintf(fp,"\t\t\t);\n"
"\n");
 
fprintf(fp,
"\t\treg\tsigned\t[((IWIDTH+2)+(CWIDTH+1)-1):0]\n"
457,28 → 538,69
"\t\talways @(posedge i_clk)\n"
"\t\tif (((i_ce)&&(!MPYDELAY[0]))\n"
"\t\t\t||((ce_phase)&&(MPYDELAY[0])))\n"
"\t\t\trp_one <= mpy_pipe_out;\n"
"\t\tbegin\n"
"\t\t\trp_one <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\tf_rpone_ic <= f_past_mux_ic;\n"
"\t\t\tf_rpone_id <= f_past_mux_id;\n"
"`endif\n");
fprintf(fp,
"\t\tend\n\n");
fprintf(fp,
"\t\talways @(posedge i_clk)\n"
"\t\tif (((i_ce)&&(MPYDELAY[0]))\n"
"\t\t\t||((ce_phase)&&(!MPYDELAY[0])))\n"
"\t\t\trp_two <= mpy_pipe_out;\n"
"\t\tbegin\n"
"\t\t\trp_two <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\tf_rptwo_ic <= f_past_mux_ic;\n"
"\t\t\tf_rptwo_id <= f_past_mux_id;\n"
"`endif\n");
fprintf(fp,
"\t\tend\n\n");
fprintf(fp,
"\t\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\trp_three <= longmpy;\n"
"\n"
"\t\tbegin\n"
"\t\t\trp_three <= longmpy;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\tf_rpthree_ic <= f_past_ic;\n"
"\t\t\tf_rpthree_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\tend\n"
"\n\n");
 
 
fprintf(fp,
"\t\t// Our outputs *MUST* be set on a clock where i_ce is\n"
"\t\t// true for the following logic to work. Make that\n"
"\t\t// happen here.\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\tbegin\n"
"\t\t\trp2_one<= rp_one;\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\trp2_two <= rp_two;\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\trp2_three<= rp_three;\n"
"\t\t\trp2_three<= rp_three;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\tf_rp2one_ic <= f_rpone_ic;\n"
"\t\t\tf_rp2one_id <= f_rpone_id;\n"
"\n"
 
"\t\t\tf_rp2two_ic <= f_rptwo_ic;\n"
"\t\t\tf_rp2two_id <= f_rptwo_id;\n"
"\n"
 
"\t\t\tf_rp2three_ic <= f_rpthree_ic;\n"
"\t\t\tf_rp2three_id <= f_rpthree_id;\n"
"`endif\n");
fprintf(fp,
"\t\tend\n"
"\n"
"\t\tassign p_one = rp2_one;\n"
"\t\tassign p_two = (!MPYDELAY[0])? rp2_two : rp_two;\n"
"\t\tassign p_three = ( MPYDELAY[0])? rp_three : rp2_three;\n"
488,7 → 610,19
"\t\tassign\tunused = { rp2_two, rp2_three };\n"
"\t\t// verilator lint_on UNUSED\n"
"\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\tassign fp_one_ic = f_rp2one_ic;\n"
"\t\tassign fp_one_id = f_rp2one_id;\n"
"\n"
"\t\tassign fp_two_ic = (!MPYDELAY[0])? f_rp2two_ic : f_rptwo_ic;\n"
"\t\tassign fp_two_id = (!MPYDELAY[0])? f_rp2two_id : f_rptwo_id;\n"
"\n"
"\t\tassign fp_three_ic= (MPYDELAY[0])? f_rpthree_ic : f_rp2three_ic;\n"
"\t\tassign fp_three_id= (MPYDELAY[0])? f_rpthree_id : f_rp2three_id;\n"
"`endif\n\n");
 
 
/////////////////////////
///
/// Three clock per CE, so CE, no-ce, no-ce*, CE
512,6 → 646,20
"\n"
"\t\treg\tsigned [ (CWIDTH+IWIDTH+3)-1:0] mpy_pipe_out;\n"
"\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\twire\t[CWIDTH:0] f_past_ic;\n"
"\t\twire\t[IWIDTH+1:0] f_past_id;\n"
"\n"
"\t\treg\t[CWIDTH:0] f_rpone_ic, f_rptwo_ic, f_rpthree_ic,\n"
"\t\t\t\t\tf_rp2one_ic, f_rp2two_ic, f_rp2three_ic,\n"
"\t\t\t\t\tf_rp3one_ic;\n"
"\t\treg\t[IWIDTH+1:0] f_rpone_id, f_rptwo_id, f_rpthree_id,\n"
"\t\t\t\t\tf_rp2one_id, f_rp2two_id, f_rp2three_id,\n"
"\t\t\t\t\tf_rp3one_id;\n"
"`endif\n"
"\n");
 
fprintf(fp,
"\t\tinitial\tce_phase = 3'b011;\n"
"\t\talways @(posedge i_clk)\n"
528,29 → 676,35
 
fprintf(fp,
"\t\talways @(posedge i_clk)\n"
"\t\t\tif (ce_phase == 3\'b000)\n"
"\t\t\tbegin\n"
"\t\t\t\t// Second clock\n"
"\t\t\t\tmpy_pipe_c[3*(CWIDTH+1)-1:(CWIDTH+1)] <= {\n"
"\t\t\t\t\tir_coef_r[CWIDTH-1], ir_coef_r,\n"
"\t\t\t\t\tir_coef_i[CWIDTH-1], ir_coef_i };\n"
"\t\t\t\tmpy_pipe_c[CWIDTH:0] <= ir_coef_i + ir_coef_r;\n"
"\t\t\t\tmpy_pipe_d[3*(IWIDTH+2)-1:(IWIDTH+2)] <= {\n"
"\t\t\t\t\tr_dif_r[IWIDTH], r_dif_r,\n"
"\t\t\t\t\tr_dif_i[IWIDTH], r_dif_i };\n"
"\t\t\t\tmpy_pipe_d[(IWIDTH+2)-1:0] <= r_dif_r + r_dif_i;\n"
"\t\tif (ce_phase == 3\'b000)\n"
"\t\tbegin\n"
"\t\t\t// Second clock\n"
"\t\t\tmpy_pipe_c[3*(CWIDTH+1)-1:(CWIDTH+1)] <= {\n"
"\t\t\t\tir_coef_r[CWIDTH-1], ir_coef_r,\n"
"\t\t\t\tir_coef_i[CWIDTH-1], ir_coef_i };\n"
"\t\t\tmpy_pipe_c[CWIDTH:0] <= ir_coef_i + ir_coef_r;\n"
"\t\t\tmpy_pipe_d[3*(IWIDTH+2)-1:(IWIDTH+2)] <= {\n"
"\t\t\t\tr_dif_r[IWIDTH], r_dif_r,\n"
"\t\t\t\tr_dif_i[IWIDTH], r_dif_i };\n"
"\t\t\tmpy_pipe_d[(IWIDTH+2)-1:0] <= r_dif_r + r_dif_i;\n"
"\n"
"\t\t\tend else if (mpy_pipe_v)\n"
"\t\t\tbegin\n"
"\t\t\t\tmpy_pipe_c[3*(CWIDTH+1)-1:0] <= {\n"
"\t\t\t\t\tmpy_pipe_c[2*(CWIDTH+1)-1:0], {(CWIDTH+1){1\'b0}} };\n"
"\t\t\t\tmpy_pipe_d[3*(IWIDTH+2)-1:0] <= {\n"
"\t\t\t\t\tmpy_pipe_d[2*(IWIDTH+2)-1:0], {(IWIDTH+2){1\'b0}} };\n"
"\t\t\tend\n"
"\t\tend else if (mpy_pipe_v)\n"
"\t\tbegin\n"
"\t\t\tmpy_pipe_c[3*(CWIDTH+1)-1:0] <= {\n"
"\t\t\t\tmpy_pipe_c[2*(CWIDTH+1)-1:0], {(CWIDTH+1){1\'b0}} };\n"
"\t\t\tmpy_pipe_d[3*(IWIDTH+2)-1:0] <= {\n"
"\t\t\t\tmpy_pipe_d[2*(IWIDTH+2)-1:0], {(IWIDTH+2){1\'b0}} };\n"
"\t\tend\n"
"\n");
fprintf(fp,
"\t\tlongbimpy #(CWIDTH+1,IWIDTH+2) mpy(i_clk, mpy_pipe_v,\n"
"\t\t\t\tmpy_pipe_vc, mpy_pipe_vd, mpy_pipe_out);\n"
"\t\t\t\tmpy_pipe_vc, mpy_pipe_vd, mpy_pipe_out\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\t\t, f_past_ic, f_past_id\n"
"`endif\n");
fprintf(fp,
"\t\t\t);\n"
"\n");
 
fprintf(fp,
565,27 → 719,93
"\t\tif (MPYREMAINDER == 0)\n"
"\t\tbegin\n\n"
"\t\t if (i_ce)\n"
"\t\t rp_two <= mpy_pipe_out;\n"
"\t\t else if (ce_phase == 3'b000)\n"
"\t\t rp_three <= mpy_pipe_out;\n"
"\t\t else if (ce_phase == 3'b001)\n"
"\t\t rp_one <= mpy_pipe_out;\n\n"
"\t\t begin\n"
"\t\t rp_two <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rptwo_ic <= f_past_ic;\n"
"\t\t f_rptwo_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end else if (ce_phase == 3'b000)\n"
"\t\t begin\n"
"\t\t rp_three <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rpthree_ic <= f_past_ic;\n"
"\t\t f_rpthree_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end else if (ce_phase == 3'b001)\n"
"\t\t begin\n"
"\t\t rp_one <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rpone_ic <= f_past_ic;\n"
"\t\t f_rpone_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end\n"
"\t\tend else if (MPYREMAINDER == 1)\n"
"\t\tbegin\n\n"
"\t\t if (i_ce)\n"
"\t\t rp_one <= mpy_pipe_out;\n"
"\t\t else if (ce_phase == 3'b000)\n"
"\t\t rp_two <= mpy_pipe_out;\n"
"\t\t else if (ce_phase == 3'b001)\n"
"\t\t rp_three <= mpy_pipe_out;\n\n"
"\t\t begin\n"
"\t\t rp_one <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rpone_ic <= f_past_ic;\n"
"\t\t f_rpone_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end else if (ce_phase == 3'b000)\n"
"\t\t begin\n"
"\t\t rp_two <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rptwo_ic <= f_past_ic;\n"
"\t\t f_rptwo_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end else if (ce_phase == 3'b001)\n"
"\t\t begin\n"
"\t\t rp_three <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rpthree_ic <= f_past_ic;\n"
"\t\t f_rpthree_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end\n"
"\t\tend else // if (MPYREMAINDER == 2)\n"
"\t\tbegin\n\n"
"\t\t if (i_ce)\n"
"\t\t rp_three <= mpy_pipe_out;\n"
"\t\t else if (ce_phase == 3'b000)\n"
"\t\t rp_one <= mpy_pipe_out;\n"
"\t\t else if (ce_phase == 3'b001)\n"
"\t\t rp_two <= mpy_pipe_out;\n\n"
"\t\t begin\n"
"\t\t rp_three <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rpthree_ic <= f_past_ic;\n"
"\t\t f_rpthree_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end else if (ce_phase == 3'b000)\n"
"\t\t begin\n"
"\t\t rp_one <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rpone_ic <= f_past_ic;\n"
"\t\t f_rpone_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end else if (ce_phase == 3'b001)\n"
"\t\t begin\n"
"\t\t rp_two <= mpy_pipe_out;\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t f_rptwo_ic <= f_past_ic;\n"
"\t\t f_rptwo_id <= f_past_id;\n"
"`endif\n");
fprintf(fp,
"\t\t end\n"
"\t\tend\n\n");
 
fprintf(fp,
595,14 → 815,42
"\t\t\trp2_one <= rp_one;\n"
"\t\t\trp2_two <= rp_two;\n"
"\t\t\trp2_three <= (MPYREMAINDER == 2) ? mpy_pipe_out : rp_three;\n"
"\t\t\trp3_one <= (MPYREMAINDER == 0) ? rp2_one : rp_one;\n"
"\t\tend\n");
"\t\t\trp3_one <= (MPYREMAINDER == 0) ? rp2_one : rp_one;\n");
 
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\t\tf_rp2one_ic <= f_rpone_ic;\n"
"\t\t\tf_rp2one_id <= f_rpone_id;\n"
"\n"
"\t\t\tf_rp2two_ic <= f_rptwo_ic;\n"
"\t\t\tf_rp2two_id <= f_rptwo_id;\n"
"\n"
"\t\t\tf_rp2three_ic <= (MPYREMAINDER==2) ? f_past_ic : f_rpthree_ic;\n"
"\t\t\tf_rp2three_id <= (MPYREMAINDER==2) ? f_past_id : f_rpthree_id;\n"
"\t\t\tf_rp3one_ic <= (MPYREMAINDER==0) ? f_rp2one_ic : f_rpone_ic;\n"
"\t\t\tf_rp3one_id <= (MPYREMAINDER==0) ? f_rp2one_id : f_rpone_id;\n"
"`endif\n");
 
 
fprintf(fp,
 
"\t\tend\n"
"\n"
"\t\tassign\tp_one = rp3_one;\n"
"\t\tassign\tp_two = rp2_two;\n"
"\t\tassign\tp_three = rp2_three;\n"
"\n");
if (formal_property_flag) fprintf(fp,
"`ifdef FORMAL\n"
"\t\tassign fp_one_ic = f_rp3one_ic;\n"
"\t\tassign fp_one_id = f_rp3one_id;\n"
"\n"
"\t\tassign fp_two_ic = f_rp2two_ic;\n"
"\t\tassign fp_two_id = f_rp2two_id;\n"
"\n"
"\t\tassign fp_three_ic = f_rp2three_ic;\n"
"\t\tassign fp_three_id = f_rp2three_id;\n"
"`endif\n"
"\n");
 
fprintf(fp,
"\tend endgenerate\n");
616,8 → 864,10
"\t// extension.\n"
"\twire\tsigned\t[(IWIDTH+CWIDTH):0] fifo_i, fifo_r;\n"
"\treg\t\t[(2*IWIDTH+1):0] fifo_read;\n"
"\tassign\tfifo_r = { {2{fifo_read[2*(IWIDTH+1)-1]}}, fifo_read[(2*(IWIDTH+1)-1):(IWIDTH+1)], {(CWIDTH-2){1\'b0}} };\n"
"\tassign\tfifo_i = { {2{fifo_read[(IWIDTH+1)-1]}}, fifo_read[((IWIDTH+1)-1):0], {(CWIDTH-2){1\'b0}} };\n"
"\tassign\tfifo_r = { {2{fifo_read[2*(IWIDTH+1)-1]}},\n"
"\t\tfifo_read[(2*(IWIDTH+1)-1):(IWIDTH+1)], {(CWIDTH-2){1\'b0}} };\n"
"\tassign\tfifo_i = { {2{fifo_read[(IWIDTH+1)-1]}},\n"
"\t\tfifo_read[((IWIDTH+1)-1):0], {(CWIDTH-2){1\'b0}} };\n"
"\n"
"\n"
"\treg\tsigned\t[(CWIDTH+IWIDTH+3-1):0] mpy_r, mpy_i;\n"
672,17 → 922,17
"\t\t\t\tmpy_i, rnd_right_i);\n\n", rnd_string);
fprintf(fp,
"\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\tbegin\n"
"\t\t\t// First clock, recover all values\n"
"\t\t\tfifo_read <= fifo_left[fifo_read_addr];\n"
"\t\t\t// These values are IWIDTH+CWIDTH+3 bits wide\n"
"\t\t\t// although they only need to be (IWIDTH+1)\n"
"\t\t\t// + (CWIDTH) bits wide. (We\'ve got two\n"
"\t\t\t// extra bits we need to get rid of.)\n"
"\t\t\tmpy_r <= p_one - p_two;\n"
"\t\t\tmpy_i <= p_three - p_one - p_two;\n"
"\t\tend\n"
"\tif (i_ce)\n"
"\tbegin\n"
"\t\t// First clock, recover all values\n"
"\t\tfifo_read <= fifo_left[fifo_read_addr];\n"
"\t\t// These values are IWIDTH+CWIDTH+3 bits wide\n"
"\t\t// although they only need to be (IWIDTH+1)\n"
"\t\t// + (CWIDTH) bits wide. (We\'ve got two\n"
"\t\t// extra bits we need to get rid of.)\n"
"\t\tmpy_r <= p_one - p_two;\n"
"\t\tmpy_i <= p_three - p_one - p_two;\n"
"\tend\n"
"\n");
 
fprintf(fp,
689,27 → 939,27
"\treg\t[(AUXLEN-1):0]\taux_pipeline;\n"
"\tinitial\taux_pipeline = 0;\n");
if (async_reset)
fprintf(fp, "\talways @(posedge i_clk, negedge i_areset_n)\n\t\tif (!i_areset_n)\n");
fprintf(fp, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fp, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fp, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fp,
"\t\t\taux_pipeline <= 0;\n"
"\t\telse if (i_ce)\n"
"\t\t\taux_pipeline <= { aux_pipeline[(AUXLEN-2):0], i_aux };\n"
"\t\taux_pipeline <= 0;\n"
"\telse if (i_ce)\n"
"\t\taux_pipeline <= { aux_pipeline[(AUXLEN-2):0], i_aux };\n"
"\n");
fprintf(fp,
"\tinitial o_aux = 1\'b0;\n");
if (async_reset)
fprintf(fp, "\talways @(posedge i_clk, negedge i_areset_n)\n\t\tif (!i_areset_n)\n");
fprintf(fp, "\talways @(posedge i_clk, negedge i_areset_n)\n\tif (!i_areset_n)\n");
else
fprintf(fp, "\talways @(posedge i_clk)\n\t\tif (i_reset)\n");
fprintf(fp, "\talways @(posedge i_clk)\n\tif (i_reset)\n");
fprintf(fp,
"\t\t\to_aux <= 1\'b0;\n"
"\t\telse if (i_ce)\n"
"\t\tbegin\n"
"\t\t\t// Second clock, latch for final clock\n"
"\t\t\to_aux <= aux_pipeline[AUXLEN-1];\n"
"\t\tend\n"
"\t\to_aux <= 1\'b0;\n"
"\telse if (i_ce)\n"
"\tbegin\n"
"\t\t// Second clock, latch for final clock\n"
"\t\to_aux <= aux_pipeline[AUXLEN-1];\n"
"\tend\n"
"\n");
 
fprintf(fp,
721,28 → 971,10
"\tassign o_right= { rnd_right_r,rnd_right_i};\n"
"\n");
 
fprintf(fp,
"`ifdef FORMAL\n");
if (formal_property_flag) {
fprintf(fp,
"`ifdef VERILATOR\n"
"`define FORMAL\n"
"`endif\n"
"`ifdef FORMAL\n"
"\tlocalparam F_LGDEPTH = (AUXLEN > 64) ? 7\n"
"\t\t\t: (AUXLEN > 32) ? 6\n"
"\t\t\t: (AUXLEN > 16) ? 5\n"
"\t\t\t: (AUXLEN > 8) ? 4\n"
"\t\t\t: (AUXLEN > 4) ? 3 : 2;\n\n"
"\tlocalparam F_DEPTH = AUXLEN;\n"
"\tlocalparam [F_LGDEPTH-1:0] F_D = F_DEPTH[F_LGDEPTH-1:0]-1;\n"
"\n"
"\treg signed [IWIDTH-1:0] f_dlyleft_r [0:F_DEPTH-1];\n"
"\treg signed [IWIDTH-1:0] f_dlyleft_i [0:F_DEPTH-1];\n"
"\treg signed [IWIDTH-1:0] f_dlyright_r [0:F_DEPTH-1];\n"
"\treg signed [IWIDTH-1:0] f_dlyright_i [0:F_DEPTH-1];\n"
"\treg signed [CWIDTH-1:0] f_dlycoeff_r [0:F_DEPTH-1];\n"
"\treg signed [CWIDTH-1:0] f_dlycoeff_i [0:F_DEPTH-1];\n"
"\treg signed [F_DEPTH-1:0] f_dlyaux;\n"
"\n"
"\tinitial\tf_dlyaux[0] = 0;\n"
"\talways @(posedge i_clk)\n"
"\tif (i_reset)\n"
780,30 → 1012,78
"\tend endgenerate\n"
"\n"
"`ifndef VERILATOR\n"
"\talways @(posedge i_clk)\n"
"\tif ((!$past(i_ce))&&(!$past(i_ce,2))&&(!$past(i_ce,3))\n"
"\t &&(!$past(i_ce,4)))\n"
"\t assume(i_ce);\n"
"\n"
"\t//\n"
"\t// Make some i_ce restraining assumptions. These are necessary\n"
"\t// to get the design to pass induction.\n"
"\t//\n"
"\tgenerate if (CKPCE <= 1)\n"
"\tbegin\n"
"\n"
"\t // i_ce is allowed to be anything in this mode\n"
"\t\t// No primary i_ce assumption. i_ce can be anything\n"
"\t\t//\n"
"\t\t// First induction i_ce assumption: No more than one\n"
"\t\t// empty cycle between used cycles. Without this\n"
"\t\t// assumption, or one like it, induction would never\n"
"\t\t// complete.\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif ((!$past(i_ce)))\n"
"\t\t\tassume(i_ce);\n"
"\n"
"\t\t// Second induction i_ce assumption: avoid skipping an\n"
"\t\t// i_ce and thus stretching out the i_ce cycle two i_ce\n"
"\t\t// cycles in a row. Without this assumption, induction\n"
"\t\t// would still complete, it would just take longer\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif (($past(i_ce))&&(!$past(i_ce,2)))\n"
"\t\t\tassume(i_ce);\n"
"\n"
"\tend else if (CKPCE == 2)\n"
"\tbegin : F_CKPCE_TWO\n"
"\n"
"\t always @(posedge i_clk)\n"
"\t if ($past(i_ce))\n"
"\t assume(!i_ce);\n"
"\t\t// Primary i_ce assumption: Every i_ce cycle is followed\n"
"\t\t// by a non-i_ce cycle, so the multiplies can be\n"
"\t\t// multiplexed\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif ($past(i_ce))\n"
"\t\t\tassume(!i_ce);\n"
 
"\t\t// First induction assumption: Don't let this stretch\n"
"\t\t// out too far. This is necessary to pass induction\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif ((!$past(i_ce))&&(!$past(i_ce,2)))\n"
"\t\t\tassume(i_ce);\n"
"\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif ((!$past(i_ce))&&($past(i_ce,2))\n"
"\t\t\t\t&&(!$past(i_ce,3))&&(!$past(i_ce,4)))\n"
"\t\t\tassume(i_ce);\n"
"\n"
"\tend else if (CKPCE == 3)\n"
"\tbegin : F_CKPCE_THREE\n"
"\n"
"\t always @(posedge i_clk)\n"
"\t if (($past(i_ce))||($past(i_ce,2)))\n"
"\t assume(!i_ce);\n"
"\t\t// Primary i_ce assumption: Following any i_ce cycle,\n"
"\t\t// there must be two clock cycles with i_ce de-asserted\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif (($past(i_ce))||($past(i_ce,2)))\n"
"\t\t\tassume(!i_ce);\n"
"\n"
"\t\t// Induction assumption: Allow i_ce's every third or\n"
"\t\t// fourth clock, but don't allow them to be separated\n"
"\t\t// further than that\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif ((!$past(i_ce))&&(!$past(i_ce,2))&&(!$past(i_ce,3)))\n"
"\t\t\tassume(i_ce);\n"
"\n"
"\t\t// Second induction assumption, to speed up the proof:\n"
"\t\t// If it's the earliest possible opportunity for an\n"
"\t\t// i_ce, and the last i_ce was late, don't let this one\n"
"\t\t// be late as well.\n"
"\t\talways @(posedge i_clk)\n"
"\t\tif ((!$past(i_ce))&&(!$past(i_ce,2))\n"
"\t\t\t&&($past(i_ce,3))&&(!$past(i_ce,4))\n"
"\t\t\t&&(!$past(i_ce,5))&&(!$past(i_ce,6)))\n"
"\t\t\tassume(i_ce);\n"
"\n"
"\tend endgenerate\n"
"`endif\n"
"\n"
815,7 → 1095,6
"\telse if ((i_ce)&&(!(&f_startup_counter)))\n"
"\t f_startup_counter <= f_startup_counter + 1;\n"
"\n"
"\twire signed [IWIDTH:0] f_sumr, f_sumi;\n"
"\talways @(*)\n"
"\tbegin\n"
"\t f_sumr = f_dlyleft_r[F_D] + f_dlyright_r[F_D];\n"
822,11 → 1101,9
"\t f_sumi = f_dlyleft_i[F_D] + f_dlyright_i[F_D];\n"
"\tend\n"
"\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_sumrx, f_sumix;\n"
"\tassign\tf_sumrx = { {(4){f_sumr[IWIDTH]}}, f_sumr, {(CWIDTH-2){1'b0}} };\n"
"\tassign\tf_sumix = { {(4){f_sumi[IWIDTH]}}, f_sumi, {(CWIDTH-2){1'b0}} };\n"
"\n"
"\twire signed [IWIDTH:0] f_difr, f_difi;\n"
"\talways @(*)\n"
"\tbegin\n"
"\t f_difr = f_dlyleft_r[F_D] - f_dlyright_r[F_D];\n"
833,11 → 1110,9
"\t f_difi = f_dlyleft_i[F_D] - f_dlyright_i[F_D];\n"
"\tend\n"
"\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_difrx, f_difix;\n"
"\tassign\tf_difrx = { {(CWIDTH+2){f_difr[IWIDTH]}}, f_difr };\n"
"\tassign\tf_difix = { {(CWIDTH+2){f_difi[IWIDTH]}}, f_difi };\n"
"\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_widecoeff_r, f_widecoeff_i;\n"
"\tassign\tf_widecoeff_r ={ {(IWIDTH+3){f_dlycoeff_r[F_D][CWIDTH-1]}},\n"
"\t\t\t\t\t\tf_dlycoeff_r[F_D] };\n"
"\tassign\tf_widecoeff_i ={ {(IWIDTH+3){f_dlycoeff_i[F_D][CWIDTH-1]}},\n"
894,7 → 1169,6
"\t// help induction finish one (or more) clocks ealier than\n"
"\t// otherwise\n"
"\n\n"
"\twire signed [IWIDTH:0] f_predifr, f_predifi;\n"
"\talways @(*)\n"
"\tbegin\n"
"\t\tf_predifr = f_dlyleft_r[F_D-1] - f_dlyright_r[F_D-1];\n"
901,12 → 1175,9
"\t\tf_predifi = f_dlyleft_i[F_D-1] - f_dlyright_i[F_D-1];\n"
"\tend\n"
"\n"
"\twire signed [IWIDTH+CWIDTH+3-1:0] f_predifrx, f_predifix;\n"
"\tassign f_predifrx = { {(CWIDTH+2){f_predifr[IWIDTH]}}, f_predifr };\n"
"\tassign f_predifix = { {(CWIDTH+2){f_predifi[IWIDTH]}}, f_predifi };\n"
"\n"
"\twire signed [CWIDTH:0] f_sumcoef;\n"
"\twire signed [IWIDTH+1:0] f_sumdiff;\n"
"\talways @(*)\n"
"\tbegin\n"
"\t\tf_sumcoef = f_dlycoeff_r[F_D-1] + f_dlycoeff_i[F_D-1];\n"
950,6 → 1221,8
"\t\t\tassert(p_three == f_sumcoef);\n"
"\t\t// verilator lint_on WIDTH\n"
"`ifdef VERILATOR\n"
"\t\t// Check that the multiplies match--but *ONLY* if using\n"
"\t\t// Verilator, and not if using formal proper\n"
"\t\tassert(p_one == f_predifr * f_dlycoeff_r[F_D-1]);\n"
"\t\tassert(p_two == f_predifi * f_dlycoeff_i[F_D-1]);\n"
"\t\tassert(p_three == f_sumdiff * f_sumcoef);\n"
957,6 → 1230,31
"\tend\n\n");
 
fprintf(fp,
"\t// The following logic formally insists that our version of the\n"
"\t// inputs to the multiply matches what the (multiclock) multiply\n"
"\t// thinks its inputs were. While this may seem redundant, the\n"
"\t// proof will not complete in any reasonable amount of time\n"
"\t// without these assertions.\n"
"\n"
"\tassign\tf_p3c_in = f_dlycoeff_i[F_D-1] + f_dlycoeff_r[F_D-1];\n"
"\tassign\tf_p3d_in = f_predifi + f_predifr;\n"
"\n"
"\talways @(*)\n"
"\tif (f_startup_counter >= { 1'b0, F_D })\n"
"\tbegin\n"
"\t\tassert(fp_one_ic == { f_dlycoeff_r[F_D-1][CWIDTH-1],\n"
"\t\t\t\tf_dlycoeff_r[F_D-1][CWIDTH-1:0] });\n"
"\t\tassert(fp_two_ic == { f_dlycoeff_i[F_D-1][CWIDTH-1],\n"
"\t\t\t\tf_dlycoeff_i[F_D-1][CWIDTH-1:0] });\n"
"\t\tassert(fp_one_id == { f_predifr[IWIDTH], f_predifr });\n"
"\t\tassert(fp_two_id == { f_predifi[IWIDTH], f_predifi });\n"
"\t\tassert(fp_three_ic == f_p3c_in);\n"
"\t\tassert(fp_three_id == f_p3d_in);\n"
"\tend\n"
"\n");
 
 
fprintf(fp,
"\t// F_CHECK will be set externally by the solver, so that we can\n"
"\t// double check that the solver is actually testing what we think\n"
"\t// it is testing. We'll set it here to MPYREMAINDER, which will\n"
965,9 → 1263,12
"\tparameter F_CHECK = MPYREMAINDER;\n"
"\tinitial assert(MPYREMAINDER == F_CHECK);\n\n");
 
} else {
fprintf(fp, "// Set the formal_property_flag to enable formal\n"
"// property generation\n");
}
fprintf(fp,
"`endif // FORMAL\n");
}
 
fprintf(fp,
"endmodule\n");
1051,10 → 1352,10
ckpce);
 
fprintf(fp,
"\tinput\t\ti_clk, %s, i_ce;\n"
"\tinput\t\t[(2*CWIDTH-1):0]\ti_coef;\n"
"\tinput\t\t[(2*IWIDTH-1):0]\ti_left, i_right;\n"
"\tinput\t\ti_aux;\n"
"\tinput\twire\ti_clk, %s, i_ce;\n"
"\tinput\twire\t[(2*CWIDTH-1):0]\ti_coef;\n"
"\tinput\twire\t[(2*IWIDTH-1):0]\ti_left, i_right;\n"
"\tinput\twire\ti_aux;\n"
"\toutput\twire\t[(2*OWIDTH-1):0]\to_left, o_right;\n"
"\toutput\treg\to_aux;\n\n"
"\n", resetw.c_str());
1544,9 → 1845,6
 
if (formal_property_flag) {
fprintf(fp,
"`ifdef VERILATOR\n"
"`define FORMAL\n"
"`endif\n"
"`ifdef FORMAL\n"
"\tlocalparam F_LGDEPTH = 3;\n"
"\tlocalparam F_DEPTH = 5;\n"
/dblclockfft/trunk/sw/butterfly.h
24,7 → 24,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/defaults.h
4,7 → 4,12
//
// Project: A General Purpose Pipelined FFT Implementation
//
// Purpose:
// Purpose: This defaults file contains defaults used throughout the design.
// These primarily consist of whether or not the project contains
// formal properties, the default directory the core will be placed into,
// as well as the default parameters of the various modules--parameters
// which will be overridden in operation but are kept as is for bench-test
// simulation.
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
24,7 → 29,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/fftgen.cpp
40,7 → 40,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
150,8 → 150,8
"\t// core is built ... Note that the minimum LGSPAN is 2. Smaller\n"
"\t// spans must use the fftdoubles stage.\n"
"\tparameter\tLGWIDTH=%d, ODD=0, INVERSE=0,SHIFT=0;\n"
"\tinput\t i_clk, %s, i_ce, i_sync;\n"
"\tinput\t [(2*IWIDTH-1):0] i_data;\n"
"\tinput\twire i_clk, %s, i_ce, i_sync;\n"
"\tinput\twire [(2*IWIDTH-1):0] i_data;\n"
"\toutput\treg [(2*OWIDTH-1):0] o_data;\n"
"\toutput\treg o_sync;\n"
"\t\n", (dbg)?"_dbg":"",
402,8 → 402,8
"module\tqtrstage%s(i_clk, %s, i_ce, i_sync, i_data, o_data, o_sync%s);\n"
"\tparameter IWIDTH=%d, OWIDTH=IWIDTH+1;\n"
"\tparameter\tLGWIDTH=%d, INVERSE=0,SHIFT=0;\n"
"\tinput\t i_clk, %s, i_ce, i_sync;\n"
"\tinput\t [(2*IWIDTH-1):0] i_data;\n"
"\tinput\twire i_clk, %s, i_ce, i_sync;\n"
"\tinput\twire [(2*IWIDTH-1):0] i_data;\n"
"\toutput\treg [(2*OWIDTH-1):0] o_data;\n"
"\toutput\treg o_sync;\n"
"\t\n", (dbg)?"_dbg":"", resetw.c_str(),
763,8 → 763,8
fprintf(fp,
"module laststage(i_clk, %s, i_ce, i_sync, i_val, o_val, o_sync);\n"
" parameter IWIDTH=16,OWIDTH=IWIDTH+1, SHIFT=0;\n"
" input i_clk, %s, i_ce, i_sync;\n"
" input [(2*IWIDTH-1):0] i_val;\n"
" input wire i_clk, %s, i_ce, i_sync;\n"
" input wire [(2*IWIDTH-1):0] i_val;\n"
" output wire [(2*OWIDTH-1):0] o_val;\n"
" output reg o_sync;\n\n",
resetw.c_str(), resetw.c_str());
992,6 → 992,8
"\t\tmultipliers.\n"
"\t-r\tBuild a real-FFT at four input points per sample, rather than a\n"
"\t\tcomplex FFT. (Default is a Complex FFT.)\n"
"\t\tThis option is a place-holder. The real-FFT has not (yet) been\n"
"\t\timplemented.\n"
"\t-s\tSkip the final bit reversal stage. This is useful in\n"
"\t\talgorithms that need to apply a filter without needing to do\n"
"\t\tbin shifting, as these algorithms can, with this option, just\n"
1022,7 → 1024,7
const char *EMPTYSTR = "";
bool bitreverse = true, inverse=false,
verbose_flag = false,
single_clock = false,
single_clock = true,
real_fft = false,
async_reset = false;
FILE *vmain;
1419,6 → 1421,9
"//\n");
fprintf(vmain, "//\t\t%% %s\n", cmdline.c_str());
fprintf(vmain, "//\n");
fprintf(vmain, "//\tThis core will use hardware accelerated multiplies (DSPs)\n"
"//\tfor %d of the %d stages\n", mpy_stages, lgval(fftsize));
fprintf(vmain, "//\n");
fprintf(vmain, "%s", creator);
fprintf(vmain, "//\n");
fprintf(vmain, "%s", cpyleft);
1441,15 → 1446,22
fprintf(vmain, "\t\to_left, o_right, o_sync%s);\n",
(dbg)?", o_dbg":"");
}
fprintf(vmain, "\tparameter\tIWIDTH=%d, OWIDTH=%d, LGWIDTH=%d;\n\t//\n", nbitsin, nbitsout, lgsize);
fprintf(vmain,
"\t// The bit-width of the input, IWIDTH, output, OWIDTH, and the log\n"
"\t// of the FFT size. These are localparams, rather than parameters,\n"
"\t// because once the core has been generated, they can no longer be\n"
"\t// changed. (These values can be adjusted by running the core\n"
"\t// generator again.) The reason is simply that these values have\n"
"\t// been hardwired into the core at several places.\n");
fprintf(vmain, "\tlocalparam\tIWIDTH=%d, OWIDTH=%d, LGWIDTH=%d;\n\t//\n", nbitsin, nbitsout, lgsize);
assert(lgsize > 0);
fprintf(vmain, "\tinput\t\t\t\t\ti_clk, %s, i_ce;\n\t//\n",
fprintf(vmain, "\tinput\twire\t\t\t\ti_clk, %s, i_ce;\n\t//\n",
resetw.c_str());
if (single_clock) {
fprintf(vmain, "\tinput\t\t[(2*IWIDTH-1):0]\ti_sample;\n");
fprintf(vmain, "\tinput\twire\t[(2*IWIDTH-1):0]\ti_sample;\n");
fprintf(vmain, "\toutput\treg\t[(2*OWIDTH-1):0]\to_result;\n");
} else {
fprintf(vmain, "\tinput\t\t[(2*IWIDTH-1):0]\ti_left, i_right;\n");
fprintf(vmain, "\tinput\twire\t[(2*IWIDTH-1):0]\ti_left, i_right;\n");
fprintf(vmain, "\toutput\treg\t[(2*OWIDTH-1):0]\to_left, o_right;\n");
}
fprintf(vmain, "\toutput\treg\t\t\t\to_sync;\n");
1500,20 → 1512,20
// since the multiplies can be done by adds
mpystage = ((lgtmp-2) <= mpy_stages);
 
fprintf(vmain, "\n\n");
if (mpystage)
fprintf(vmain, "\t// A hardware optimized FFT stage\n");
fprintf(vmain, "\n\n");
fprintf(vmain, "\twire\t\tw_s%d;\n", fftsize);
if (single_clock) {
fprintf(vmain, "\twire\t[%d:0]\tw_d%d;\n", 2*(obits+xtrapbits)-1, fftsize);
cmem = gen_coeff_fname(EMPTYSTR, fftsize, 1, 0, inverse);
cmem = gen_coeff_fname(coredir.c_str(), fftsize, 1, 0, inverse);
cmemfp = gen_coeff_open(cmem.c_str());
gen_coeffs(cmemfp, fftsize, nbitsin+xtracbits, 1, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(IWIDTH,IWIDTH+%d,%d,%d,%d,0,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_%d(i_clk, %s, i_ce,\n",
cmem = gen_coeff_fname(EMPTYSTR, fftsize, 1, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(IWIDTH,IWIDTH+%d,%d,%d,0,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_%d(i_clk, %s, i_ce,\n",
((dbg)&&(dbgstage == fftsize))?"_dbg":"",
xtracbits, obits+xtrapbits,
lgsize, lgtmp-1,
(mpystage)?1:0,
lgtmp-1, (mpystage)?1:0,
ckpce, cmem.c_str(),
fftsize, resetw.c_str());
fprintf(vmain, "\t\t\t(%s%s), i_sample, w_d%d, w_s%d%s);\n",
1524,14 → 1536,14
} else {
fprintf(vmain, "\t// verilator lint_off UNUSED\n\twire\t\tw_os%d;\n\t// verilator lint_on UNUSED\n", fftsize);
fprintf(vmain, "\twire\t[%d:0]\tw_e%d, w_o%d;\n", 2*(obits+xtrapbits)-1, fftsize, fftsize);
cmem = gen_coeff_fname(EMPTYSTR, fftsize, 2, 0, inverse);
cmem = gen_coeff_fname(coredir.c_str(), fftsize, 2, 0, inverse);
cmemfp = gen_coeff_open(cmem.c_str());
gen_coeffs(cmemfp, fftsize, nbitsin+xtracbits, 2, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(IWIDTH,IWIDTH+%d,%d,%d,%d,0,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_e%d(i_clk, %s, i_ce,\n",
cmem = gen_coeff_fname(EMPTYSTR, fftsize, 2, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(IWIDTH,IWIDTH+%d,%d,%d,0,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_e%d(i_clk, %s, i_ce,\n",
((dbg)&&(dbgstage == fftsize))?"_dbg":"",
xtracbits, obits+xtrapbits,
lgsize, lgtmp-2,
(mpystage)?1:0,
lgtmp-2, (mpystage)?1:0,
ckpce, cmem.c_str(),
fftsize, resetw.c_str());
fprintf(vmain, "\t\t\t(%s%s), i_left, w_e%d, w_s%d%s);\n",
1538,13 → 1550,13
(async_reset)?"":"!", resetw.c_str(),
fftsize, fftsize,
((dbg)&&(dbgstage == fftsize))?", o_dbg":"");
cmem = gen_coeff_fname(EMPTYSTR, fftsize, 2, 1, inverse);
cmem = gen_coeff_fname(coredir.c_str(), fftsize, 2, 1, inverse);
cmemfp = gen_coeff_open(cmem.c_str());
gen_coeffs(cmemfp, fftsize, nbitsin+xtracbits, 2, 1, inverse);
fprintf(vmain, "\tfftstage\t#(IWIDTH,IWIDTH+%d,%d,%d,%d,0,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_o%d(i_clk, %s, i_ce,\n",
cmem = gen_coeff_fname(EMPTYSTR, fftsize, 2, 1, inverse);
fprintf(vmain, "\tfftstage\t#(IWIDTH,IWIDTH+%d,%d,%d,0,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_o%d(i_clk, %s, i_ce,\n",
xtracbits, obits+xtrapbits,
lgsize, lgtmp-2,
(mpystage)?1:0,
lgtmp-2, (mpystage)?1:0,
ckpce, cmem.c_str(),
fftsize, resetw.c_str());
fprintf(vmain, "\t\t\t(%s%s), i_right, w_o%d, w_os%d);\n",
1565,7 → 1577,7
if (single_clock)
build_stage(fname.c_str(), fftsize, 1, 0, nbits, xtracbits, ckpce, async_reset, true);
else
build_stage(fname.c_str(), fftsize/2, 2, 1, nbits, xtracbits, ckpce, async_reset, true);
build_stage(fname.c_str(), fftsize, 2, 1, nbits, xtracbits, ckpce, async_reset, true);
}
 
fname += ".v";
1576,7 → 1588,7
} else {
// All stages use the same Verilog, so we only
// need to build one
build_stage(fname.c_str(), fftsize/2, 2, 1,
build_stage(fname.c_str(), fftsize, 2, 1,
nbits, xtracbits, ckpce, async_reset, false);
}
}
1604,17 → 1616,17
fprintf(vmain,"\twire\t[%d:0]\tw_d%d;\n",
2*(obits+xtrapbits)-1,
tmp_size);
cmem = gen_coeff_fname(EMPTYSTR, tmp_size, 1, 0, inverse);
cmem = gen_coeff_fname(coredir.c_str(), tmp_size, 1, 0, inverse);
cmemfp = gen_coeff_open(cmem.c_str());
gen_coeffs(cmemfp, tmp_size,
nbits+xtracbits+xtrapbits, 1, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(%d,%d,%d,%d,%d,%d,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_%d(i_clk, %s, i_ce,\n",
cmem = gen_coeff_fname(EMPTYSTR, tmp_size, 1, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(%d,%d,%d,%d,%d,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_%d(i_clk, %s, i_ce,\n",
((dbg)&&(dbgstage==tmp_size))?"_dbg":"",
nbits+xtrapbits,
nbits+xtracbits+xtrapbits,
obits+xtrapbits,
lgsize, lgtmp-1,
(dropbit)?0:0, (mpystage)?1:0,
lgtmp-1, (dropbit)?0:0, (mpystage)?1:0,
ckpce,
cmem.c_str(), tmp_size,
resetw.c_str());
1629,17 → 1641,17
fprintf(vmain,"\twire\t[%d:0]\tw_e%d, w_o%d;\n",
2*(obits+xtrapbits)-1,
tmp_size, tmp_size);
cmem = gen_coeff_fname(EMPTYSTR, tmp_size, 2, 0, inverse);
cmem = gen_coeff_fname(coredir.c_str(), tmp_size, 2, 0, inverse);
cmemfp = gen_coeff_open(cmem.c_str());
gen_coeffs(cmemfp, tmp_size,
nbits+xtracbits+xtrapbits, 2, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(%d,%d,%d,%d,%d,%d,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_e%d(i_clk, %s, i_ce,\n",
cmem = gen_coeff_fname(EMPTYSTR, tmp_size, 2, 0, inverse);
fprintf(vmain, "\tfftstage%s\t#(%d,%d,%d,%d,%d,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_e%d(i_clk, %s, i_ce,\n",
((dbg)&&(dbgstage==tmp_size))?"_dbg":"",
nbits+xtrapbits,
nbits+xtracbits+xtrapbits,
obits+xtrapbits,
lgsize, lgtmp-2,
(dropbit)?0:0, (mpystage)?1:0,
lgtmp-2, (dropbit)?0:0, (mpystage)?1:0,
ckpce,
cmem.c_str(), tmp_size,
resetw.c_str());
1648,18 → 1660,19
tmp_size, tmp_size,
((dbg)&&(dbgstage == tmp_size))
?", o_dbg":"");
cmem = gen_coeff_fname(EMPTYSTR,
cmem = gen_coeff_fname(coredir.c_str(),
tmp_size, 2, 1, inverse);
cmemfp = gen_coeff_open(cmem.c_str());
gen_coeffs(cmemfp, tmp_size,
nbits+xtracbits+xtrapbits,
2, 1, inverse);
fprintf(vmain, "\tfftstage\t#(%d,%d,%d,%d,%d,%d,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_o%d(i_clk, %s, i_ce,\n",
cmem = gen_coeff_fname(EMPTYSTR,
tmp_size, 2, 1, inverse);
fprintf(vmain, "\tfftstage\t#(%d,%d,%d,%d,%d,\n\t\t\t%d, %d, \"%s\")\n\t\tstage_o%d(i_clk, %s, i_ce,\n",
nbits+xtrapbits,
nbits+xtracbits+xtrapbits,
obits+xtrapbits,
lgsize, lgtmp-2,
(dropbit)?0:0, (mpystage)?1:0,
lgtmp-2, (dropbit)?0:0, (mpystage)?1:0,
ckpce, cmem.c_str(), tmp_size,
resetw.c_str());
fprintf(vmain, "\t\t\tw_s%d, w_o%d, w_o%d, w_os%d);\n",
1726,8 → 1739,10
fprintf(vmain, "\twire\t[%d:0]\tw_e2, w_o2;\n",
2*obits-1);
}
/*
if ((nbits+xtrapbits+1 == obits)&&(!dropbit))
printf("WARNING: SCALING OFF BY A FACTOR OF TWO--should\'ve dropped a bit in the last stage.\n");
printf("Warning: Less than optimal scaling\n");
*/
 
if (single_clock) {
fprintf(vmain, "\tlaststage\t#(%d,%d,%d)\tstage_2(i_clk, %s, i_ce,\n",
/dblclockfft/trunk/sw/fftlib.cpp
24,7 → 24,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
120,11 → 120,11
// width of the FFT at this point. If thiss is a 2x at a time FFT,
// nwide will be equal to 2, and offset will be one or two.
//
assert(nwide > 0);
assert(offset < nwide);
assert(stage / nwide > 1);
assert(stage % nwide == 0);
printf("GEN-COEFFS(): stage =%4d, bits =%2d, nwide = %d, offset = %d, nverse = %d\n", stage, cbits, nwide, offset, inv);
// assert(nwide > 0);
// assert(offset < nwide);
// assert(stage / nwide > 1);
// assert(stage % nwide == 0);
// printf("GEN-COEFFS(): stage =%4d, bits =%2d, nwide = %d, offset = %d, nverse = %d\n", stage, cbits, nwide, offset, inv);
int ncoeffs = stage/nwide/2;
for(int i=0; i<ncoeffs; i++) {
int k = nwide*i+offset;
/dblclockfft/trunk/sw/fftlib.h
24,7 → 24,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/legal.cpp
13,7 → 13,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
26,7 → 26,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
42,25 → 42,27
const char cpyleft[] =
SLASHLINE
"//\n"
"// Copyright (C) 2015-2018, Gisselquist Technology, LLC\n"
"// Copyright (C) 2015-2019, Gisselquist Technology, LLC\n"
"//\n"
"// This program is free software (firmware): you can redistribute it and/or\n"
"// modify it under the terms of the GNU General Public License as published\n"
"// by the Free Software Foundation, either version 3 of the License, or (at\n"
"// your option) any later version.\n"
"// This file is part of the general purpose pipelined FFT project.\n"
"//\n"
"// This program is distributed in the hope that it will be useful, but WITHOUT\n"
"// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or\n"
"// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License\n"
"// for more details.\n"
"// The pipelined FFT project is free software (firmware): you can redistribute\n"
"// it and/or modify it under the terms of the GNU Lesser General Public License\n"
"// as published by the Free Software Foundation, either version 3 of the\n"
"// License, or (at your option) any later version.\n"
"//\n"
"// You should have received a copy of the GNU General Public License along\n"
"// with this program. (It's in the $(ROOT)/doc directory, run make with no\n"
"// target there if the PDF file isn\'t present.) If not, see\n"
"// The pipelined FFT project is distributed in the hope that it will be useful,\n"
"// but WITHOUT ANY WARRANTY; without even the implied warranty of\n"
"// MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser\n"
"// General Public License for more details.\n"
"//\n"
"// You should have received a copy of the GNU Lesser General Public License\n"
"// along with this program. (It's in the $(ROOT)/doc directory. Run make\n"
"// with no target there if the PDF file isn't present.) If not, see\n"
"// <http://www.gnu.org/licenses/> for a copy.\n"
"//\n"
"// License: GPL, v3, as defined and found on www.gnu.org,\n"
"// http://www.gnu.org/licenses/gpl.html\n"
"// License: LGPL, v3, as defined and found on www.gnu.org,\n"
"// http://www.gnu.org/licenses/lgpl.html\n"
"//\n"
"//\n"
SLASHLINE;
/dblclockfft/trunk/sw/legal.h
26,7 → 26,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/rounding.cpp
25,7 → 25,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
91,8 → 91,8
fprintf(fp,
"module truncate(i_clk, i_ce, i_val, o_val);\n"
"\tparameter\tIWID=16, OWID=8, SHIFT=0;\n"
"\tinput\t\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\tsigned\t[(IWID-1):0]\ti_val;\n"
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
"\tinput\twire\tsigned\t[(IWID-1):0]\ti_val;\n"
"\toutput\treg\tsigned\t[(OWID-1):0]\to_val;\n"
"\n"
"\talways @(posedge i_clk)\n"
132,8 → 132,8
fprintf(fp,
"module roundhalfup(i_clk, i_ce, i_val, o_val);\n"
"\tparameter\tIWID=16, OWID=8, SHIFT=0;\n"
"\tinput\t\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\tsigned\t[(IWID-1):0]\ti_val;\n"
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
"\tinput\twire\tsigned\t[(IWID-1):0]\ti_val;\n"
"\toutput\treg\tsigned\t[(OWID-1):0]\to_val;\n"
"\n"
"\t// Let's deal with two cases to be as general as we can be here\n"
211,8 → 211,8
fprintf(fp,
"module roundfromzero(i_clk, i_ce, i_val, o_val);\n"
"\tparameter\tIWID=16, OWID=8, SHIFT=0;\n"
"\tinput\t\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\tsigned\t[(IWID-1):0]\ti_val;\n"
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
"\tinput\twire\tsigned\t[(IWID-1):0]\ti_val;\n"
"\toutput\treg\tsigned\t[(OWID-1):0]\to_val;\n"
"\n"
"\t// Let's deal with three cases to be as general as we can be here\n"
321,8 → 321,8
fprintf(fp,
"module convround(i_clk, i_ce, i_val, o_val);\n"
"\tparameter\tIWID=16, OWID=8, SHIFT=0;\n"
"\tinput\t\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\tsigned\t[(IWID-1):0]\ti_val;\n"
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
"\tinput\twire\tsigned\t[(IWID-1):0]\ti_val;\n"
"\toutput\treg\tsigned\t[(OWID-1):0]\to_val;\n"
"\n"
"\t// Let's deal with three cases to be as general as we can be here\n"
/dblclockfft/trunk/sw/rounding.h
25,7 → 25,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
/dblclockfft/trunk/sw/softmpy.cpp
26,7 → 26,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//
105,9 → 105,9
fprintf(fp, "AWIDTH;\n");
#endif
fprintf(fp,
"\tinput\t\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\t[(AWIDTH-1):0]\t\ti_a;\n"
"\tinput\t\t[(BWIDTH-1):0]\t\ti_b;\n"
"\tinput\twire\t\t\t\ti_clk, i_ce;\n"
"\tinput\twire\t[(AWIDTH-1):0]\t\ti_a;\n"
"\tinput\twire\t[(BWIDTH-1):0]\t\ti_b;\n"
"\toutput\treg\t[(AWIDTH+BWIDTH-1):0]\to_r;\n"
"\n"
"\treg\t[(AWIDTH-1):0]\tu_a;\n"
200,11 → 200,11
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
fprintf(fp,
"module bimpy(i_clk, i_ce, i_a, i_b, o_r);\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"
"\tinput\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\t[(LUTB-1):0]\ti_a;\n"
"\tinput\t\t[(BW-1):0]\ti_b;\n"
"\tparameter\tBW=18; // Number of bits in i_b\n"
"\tlocalparam\tLUTB=2; // Number of bits in i_a for our LUT multiply\n"
"\tinput\twire\t\t\ti_clk, i_ce;\n"
"\tinput\twire\t[(LUTB-1):0]\ti_a;\n"
"\tinput\twire\t[(BW-1):0]\ti_b;\n"
"\toutput\treg\t[(BW+LUTB-1):0] o_r;\n"
"\n"
"\twire [(BW+LUTB-2):0] w_r;\n"
215,10 → 215,56
"\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"
"\n"
"\tinitial o_r = 0;\n"
"\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\to_r <= w_r + { c, 2'b0 };\n"
"\tif (i_ce)\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"
"`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");
 
fclose(fp);
255,7 → 301,14
fprintf(fp, "%s", cpyleft);
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
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"
"\t\t\tIBW=", TST_LONGBIMPY_AW);
#ifdef TST_LONGBIMPY_BW
275,11 → 328,18
"\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\tTLEN=(AW+(LUTB-1))/LUTB; // Nmbr of rows in our tableau\n"
"\tinput\t\t\t\ti_clk, i_ce;\n"
"\tinput\t\t[(IAW-1):0]\ti_a_unsorted;\n"
"\tinput\t\t[(IBW-1):0]\ti_b_unsorted;\n"
"\tinput\twire\t\t\ti_clk, i_ce;\n"
"\tinput\twire\t[(IAW-1):0]\ti_a_unsorted;\n"
"\tinput\twire\t[(IBW-1):0]\ti_b_unsorted;\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// Swap parameter order, so that AW <= BW -- for performance\n"
"\t// reasons\n"
313,23 → 373,26
"\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// within the number of bits given (for now).\n"
"\tinitial u_a = 0;\n"
"\tgenerate if (IW > AW)\n"
"\tbegin\n"
"\tbegin : ABS_AND_ADD_BIT_TO_A\n"
"\t\talways @(posedge i_clk)\n"
"\t\t\tif (i_ce)\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\t\tif (i_ce)\n"
"\t\t\t\tu_a <= (i_a[AW-1])?(-i_a):(i_a);\n"
"\tend endgenerate\n"
"\n"
"\tinitial sgn = 0;\n"
"\tinitial u_b = 0;\n"
"\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\tbegin\n"
"\t\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\tend\n"
"\tif (i_ce)\n"
"\tbegin : ABS_B\n"
"\t\tu_b <= (i_b[BW-1])?(-i_b):(i_b);\n"
"\t\tsgn <= i_a[AW-1] ^ i_b[BW-1];\n"
"\tend\n"
"\n"
"\twire [(BW+LUTB-1):0] pr_a, pr_b;\n"
"\n"
343,6 → 406,10
"\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_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"
"\t\tif (i_ce) r_a[0] <= u_a[(IW-1):(2*LUTB)];\n"
"\talways @(posedge i_clk)\n"
349,13 → 416,18
"\t\tif (i_ce) r_b[0] <= u_b;\n"
"\talways @(posedge i_clk)\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"
"\t\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"
"\tif (i_ce) acc[0] <= { {(IW-LUTB){1\'b0}}, pr_a}\n"
"\t\t +{ {(IW-(2*LUTB)){1\'b0}}, pr_b, {(LUTB){1\'b0}} };\n"
"\n"
"\tgenerate // Keep track of intermediate values, before multiplying them\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\tif (i_ce)\n"
"\t\tbegin\n"
367,24 → 439,31
"\n"
"\tgenerate // The actual multiply and accumulate stage\n"
"\tif (TLEN > 2) for(k=0; k<TLEN-2; k=k+1)\n"
"\tbegin : genstages\n"
"\tbegin : GENSTAGES\n"
"\t\twire\t[(BW+LUTB-1):0] genp;\n"
"\n"
"\t\t// First, the multiply: 2-bits times BW bits\n"
"\t\twire\t[(BW+LUTB-1):0] genp;\n"
"\t\tbimpy #(BW) genmpy(i_clk,i_ce,r_a[k][(LUTB-1):0],r_b[k], genp);\n"
"\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\t\tif (i_ce)\n"
"\t\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\tif (i_ce)\n"
"\t\t\tacc[k+1] <= acc[k] + {{(IW-LUTB*(k+3)){1\'b0}},\n"
"\t\t\t\tgenp, {(LUTB*(k+2)){1\'b0}} };\n"
"\tend endgenerate\n"
"\n"
"\twire [(IW+BW-1):0] w_r;\n"
"\tassign\tw_r = (r_s[TLEN-1]) ? (-acc[TLEN-2]) : acc[TLEN-2];\n"
"\n"
"\tinitial o_r = 0;\n"
"\talways @(posedge i_clk)\n"
"\t\tif (i_ce)\n"
"\t\t\to_r <= w_r[(AW+BW-1):0];\n"
"\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"
"\tbegin : VUNUSED\n"
"\t\t// verilator lint_off UNUSED\n"
392,7 → 471,273
"\t\tassign\tunused = w_r[(IW+BW-1):(AW+BW)];\n"
"\t\t// verilator lint_on UNUSED\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"
"\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");
 
fclose(fp);
/dblclockfft/trunk/sw/softmpy.h
26,7 → 26,7
// for more details.
//
// 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
// <http://www.gnu.org/licenses/> for a copy.
//

powered by: WebSVN 2.1.0

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