| Line 75... |
Line 75... |
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
|
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
|
//
|
//
|
// This program is free software (firmware): you can redistribute it and/or
|
// This file is part of the general purpose pipelined FFT project.
|
// 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
|
// The pipelined FFT project is free software (firmware): you can redistribute
|
// your option) any later version.
|
// 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
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
// License, or (at your option) any later version.
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
//
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// The pipelined FFT project is distributed in the hope that it will be useful,
|
// for more details.
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of
|
//
|
// MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser
|
// You should have received a copy of the GNU General Public License along
|
// General Public License for more details.
|
// 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
|
// 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.
|
// <http://www.gnu.org/licenses/> for a copy.
|
//
|
//
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// License: LGPL, v3, as defined and found on www.gnu.org,
|
// http://www.gnu.org/licenses/gpl.html
|
// http://www.gnu.org/licenses/lgpl.html
|
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
| Line 145... |
Line 147... |
: 2;
|
: 2;
|
localparam AUXLEN=(LCLDELAY+3);
|
localparam AUXLEN=(LCLDELAY+3);
|
localparam MPYREMAINDER = MPYDELAY - CKPCE*(MPYDELAY/CKPCE);
|
localparam MPYREMAINDER = MPYDELAY - CKPCE*(MPYDELAY/CKPCE);
|
|
|
|
|
input i_clk, i_reset, i_ce;
|
input wire i_clk, i_reset, i_ce;
|
input [(2*CWIDTH-1):0] i_coef;
|
input wire [(2*CWIDTH-1):0] i_coef;
|
input [(2*IWIDTH-1):0] i_left, i_right;
|
input wire [(2*IWIDTH-1):0] i_left, i_right;
|
input i_aux;
|
input wire i_aux;
|
output wire [(2*OWIDTH-1):0] o_left, o_right;
|
output wire [(2*OWIDTH-1):0] o_left, o_right;
|
output reg o_aux;
|
output reg o_aux;
|
|
|
|
`ifdef FORMAL
|
|
localparam F_LGDEPTH = (AUXLEN > 64) ? 7
|
|
: (AUXLEN > 32) ? 6
|
|
: (AUXLEN > 16) ? 5
|
|
: (AUXLEN > 8) ? 4
|
|
: (AUXLEN > 4) ? 3 : 2;
|
|
|
|
localparam F_DEPTH = AUXLEN;
|
|
localparam [F_LGDEPTH-1:0] F_D = F_DEPTH[F_LGDEPTH-1:0]-1;
|
|
|
|
reg signed [IWIDTH-1:0] f_dlyleft_r [0:F_DEPTH-1];
|
|
reg signed [IWIDTH-1:0] f_dlyleft_i [0:F_DEPTH-1];
|
|
reg signed [IWIDTH-1:0] f_dlyright_r [0:F_DEPTH-1];
|
|
reg signed [IWIDTH-1:0] f_dlyright_i [0:F_DEPTH-1];
|
|
reg signed [CWIDTH-1:0] f_dlycoeff_r [0:F_DEPTH-1];
|
|
reg signed [CWIDTH-1:0] f_dlycoeff_i [0:F_DEPTH-1];
|
|
reg signed [F_DEPTH-1:0] f_dlyaux;
|
|
|
|
wire signed [IWIDTH:0] f_predifr, f_predifi;
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_predifrx, f_predifix;
|
|
wire signed [CWIDTH:0] f_sumcoef;
|
|
wire signed [IWIDTH+1:0] f_sumdiff;
|
|
wire signed [IWIDTH:0] f_sumr, f_sumi;
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_sumrx, f_sumix;
|
|
wire signed [IWIDTH:0] f_difr, f_difi;
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_difrx, f_difix;
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_widecoeff_r, f_widecoeff_i;
|
|
|
|
wire [(CWIDTH):0] fp_one_ic, fp_two_ic, fp_three_ic, f_p3c_in;
|
|
wire [(IWIDTH+1):0] fp_one_id, fp_two_id, fp_three_id, f_p3d_in;
|
|
`endif
|
|
|
reg [(2*IWIDTH-1):0] r_left, r_right;
|
reg [(2*IWIDTH-1):0] r_left, r_right;
|
reg [(2*CWIDTH-1):0] r_coef, r_coef_2;
|
reg [(2*CWIDTH-1):0] r_coef, r_coef_2;
|
wire signed [(IWIDTH-1):0] r_left_r, r_left_i, r_right_r, r_right_i;
|
wire signed [(IWIDTH-1):0] r_left_r, r_left_i, r_right_r, r_right_i;
|
assign r_left_r = r_left[ (2*IWIDTH-1):(IWIDTH)];
|
assign r_left_r = r_left[ (2*IWIDTH-1):(IWIDTH)];
|
assign r_left_i = r_left[ (IWIDTH-1):0];
|
assign r_left_i = r_left[ (IWIDTH-1):0];
|
| Line 251... |
Line 285... |
// We need to pad these first two multiplies by an extra
|
// We need to pad these first two multiplies by an extra
|
// bit just to keep them aligned with the third,
|
// bit just to keep them aligned with the third,
|
// simpler, multiply.
|
// simpler, multiply.
|
longbimpy #(CWIDTH+1,IWIDTH+2) p1(i_clk, i_ce,
|
longbimpy #(CWIDTH+1,IWIDTH+2) p1(i_clk, i_ce,
|
{ir_coef_r[CWIDTH-1],ir_coef_r},
|
{ir_coef_r[CWIDTH-1],ir_coef_r},
|
{r_dif_r[IWIDTH],r_dif_r}, p_one);
|
{r_dif_r[IWIDTH],r_dif_r}, p_one
|
|
`ifdef FORMAL
|
|
, fp_one_ic, fp_one_id
|
|
`endif
|
|
);
|
longbimpy #(CWIDTH+1,IWIDTH+2) p2(i_clk, i_ce,
|
longbimpy #(CWIDTH+1,IWIDTH+2) p2(i_clk, i_ce,
|
{ir_coef_i[CWIDTH-1],ir_coef_i},
|
{ir_coef_i[CWIDTH-1],ir_coef_i},
|
{r_dif_i[IWIDTH],r_dif_i}, p_two);
|
{r_dif_i[IWIDTH],r_dif_i}, p_two
|
|
`ifdef FORMAL
|
|
, fp_two_ic, fp_two_id
|
|
`endif
|
|
);
|
longbimpy #(CWIDTH+1,IWIDTH+2) p3(i_clk, i_ce,
|
longbimpy #(CWIDTH+1,IWIDTH+2) p3(i_clk, i_ce,
|
p3c_in, p3d_in, p_three);
|
p3c_in, p3d_in, p_three
|
|
`ifdef FORMAL
|
|
, fp_three_ic, fp_three_id
|
|
`endif
|
|
);
|
|
|
end else if (CKPCE == 2)
|
end else if (CKPCE == 2)
|
begin : CKPCE_TWO
|
begin : CKPCE_TWO
|
// Coefficient multiply inputs
|
// Coefficient multiply inputs
|
reg [2*(CWIDTH)-1:0] mpy_pipe_c;
|
reg [2*(CWIDTH)-1:0] mpy_pipe_c;
|
| Line 279... |
Line 325... |
reg ce_phase;
|
reg ce_phase;
|
|
|
reg signed [(CWIDTH+IWIDTH+3)-1:0] mpy_pipe_out;
|
reg signed [(CWIDTH+IWIDTH+3)-1:0] mpy_pipe_out;
|
reg signed [IWIDTH+CWIDTH+3-1:0] longmpy;
|
reg signed [IWIDTH+CWIDTH+3-1:0] longmpy;
|
|
|
|
`ifdef FORMAL
|
|
wire [CWIDTH:0] f_past_ic;
|
|
wire [IWIDTH+1:0] f_past_id;
|
|
wire [CWIDTH:0] f_past_mux_ic;
|
|
wire [IWIDTH+1:0] f_past_mux_id;
|
|
|
|
reg [CWIDTH:0] f_rpone_ic, f_rptwo_ic, f_rpthree_ic,
|
|
f_rp2one_ic, f_rp2two_ic, f_rp2three_ic;
|
|
reg [IWIDTH+1:0] f_rpone_id, f_rptwo_id, f_rpthree_id,
|
|
f_rp2one_id, f_rp2two_id, f_rp2three_id;
|
|
`endif
|
|
|
|
|
initial ce_phase = 1'b0;
|
initial ce_phase = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
ce_phase <= 1'b0;
|
ce_phase <= 1'b0;
|
| Line 312... |
Line 370... |
mpy_pipe_d[2*(IWIDTH+1)-1:0] <= {
|
mpy_pipe_d[2*(IWIDTH+1)-1:0] <= {
|
mpy_pipe_d[(IWIDTH+1)-1:0], {(IWIDTH+1){1'b0}} };
|
mpy_pipe_d[(IWIDTH+1)-1:0], {(IWIDTH+1){1'b0}} };
|
end
|
end
|
|
|
longbimpy #(CWIDTH+1,IWIDTH+2) mpy0(i_clk, mpy_pipe_v,
|
longbimpy #(CWIDTH+1,IWIDTH+2) mpy0(i_clk, mpy_pipe_v,
|
mpy_cof_sum, mpy_dif_sum, longmpy);
|
mpy_cof_sum, mpy_dif_sum, longmpy
|
|
`ifdef FORMAL
|
|
, f_past_ic, f_past_id
|
|
`endif
|
|
);
|
|
|
longbimpy #(CWIDTH+1,IWIDTH+2) mpy1(i_clk, mpy_pipe_v,
|
longbimpy #(CWIDTH+1,IWIDTH+2) mpy1(i_clk, mpy_pipe_v,
|
{ mpy_pipe_vc[CWIDTH-1], mpy_pipe_vc },
|
{ mpy_pipe_vc[CWIDTH-1], mpy_pipe_vc },
|
{ mpy_pipe_vd[IWIDTH ], mpy_pipe_vd },
|
{ mpy_pipe_vd[IWIDTH ], mpy_pipe_vd },
|
mpy_pipe_out);
|
mpy_pipe_out
|
|
`ifdef FORMAL
|
|
, f_past_mux_ic, f_past_mux_id
|
|
`endif
|
|
);
|
|
|
reg signed [((IWIDTH+2)+(CWIDTH+1)-1):0]
|
reg signed [((IWIDTH+2)+(CWIDTH+1)-1):0]
|
rp_one, rp_two, rp_three,
|
rp_one, rp_two, rp_three,
|
rp2_one, rp2_two, rp2_three;
|
rp2_one, rp2_two, rp2_three;
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (((i_ce)&&(!MPYDELAY[0]))
|
if (((i_ce)&&(!MPYDELAY[0]))
|
||((ce_phase)&&(MPYDELAY[0])))
|
||((ce_phase)&&(MPYDELAY[0])))
|
|
begin
|
rp_one <= mpy_pipe_out;
|
rp_one <= mpy_pipe_out;
|
|
`ifdef FORMAL
|
|
f_rpone_ic <= f_past_mux_ic;
|
|
f_rpone_id <= f_past_mux_id;
|
|
`endif
|
|
end
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (((i_ce)&&(MPYDELAY[0]))
|
if (((i_ce)&&(MPYDELAY[0]))
|
||((ce_phase)&&(!MPYDELAY[0])))
|
||((ce_phase)&&(!MPYDELAY[0])))
|
|
begin
|
rp_two <= mpy_pipe_out;
|
rp_two <= mpy_pipe_out;
|
|
`ifdef FORMAL
|
|
f_rptwo_ic <= f_past_mux_ic;
|
|
f_rptwo_id <= f_past_mux_id;
|
|
`endif
|
|
end
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_ce)
|
if (i_ce)
|
|
begin
|
rp_three <= longmpy;
|
rp_three <= longmpy;
|
|
`ifdef FORMAL
|
|
f_rpthree_ic <= f_past_ic;
|
|
f_rpthree_id <= f_past_id;
|
|
`endif
|
|
end
|
|
|
|
|
// Our outputs *MUST* be set on a clock where i_ce is
|
// Our outputs *MUST* be set on a clock where i_ce is
|
// true for the following logic to work. Make that
|
// true for the following logic to work. Make that
|
// happen here.
|
// happen here.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_ce)
|
if (i_ce)
|
|
begin
|
rp2_one<= rp_one;
|
rp2_one<= rp_one;
|
always @(posedge i_clk)
|
|
if (i_ce)
|
|
rp2_two <= rp_two;
|
rp2_two <= rp_two;
|
always @(posedge i_clk)
|
|
if (i_ce)
|
|
rp2_three<= rp_three;
|
rp2_three<= rp_three;
|
|
`ifdef FORMAL
|
|
f_rp2one_ic <= f_rpone_ic;
|
|
f_rp2one_id <= f_rpone_id;
|
|
|
|
f_rp2two_ic <= f_rptwo_ic;
|
|
f_rp2two_id <= f_rptwo_id;
|
|
|
|
f_rp2three_ic <= f_rpthree_ic;
|
|
f_rp2three_id <= f_rpthree_id;
|
|
`endif
|
|
end
|
|
|
assign p_one = rp2_one;
|
assign p_one = rp2_one;
|
assign p_two = (!MPYDELAY[0])? rp2_two : rp_two;
|
assign p_two = (!MPYDELAY[0])? rp2_two : rp_two;
|
assign p_three = ( MPYDELAY[0])? rp_three : rp2_three;
|
assign p_three = ( MPYDELAY[0])? rp_three : rp2_three;
|
|
|
// verilator lint_off UNUSED
|
// verilator lint_off UNUSED
|
wire [2*(IWIDTH+CWIDTH+3)-1:0] unused;
|
wire [2*(IWIDTH+CWIDTH+3)-1:0] unused;
|
assign unused = { rp2_two, rp2_three };
|
assign unused = { rp2_two, rp2_three };
|
// verilator lint_on UNUSED
|
// verilator lint_on UNUSED
|
|
|
|
`ifdef FORMAL
|
|
assign fp_one_ic = f_rp2one_ic;
|
|
assign fp_one_id = f_rp2one_id;
|
|
|
|
assign fp_two_ic = (!MPYDELAY[0])? f_rp2two_ic : f_rptwo_ic;
|
|
assign fp_two_id = (!MPYDELAY[0])? f_rp2two_id : f_rptwo_id;
|
|
|
|
assign fp_three_ic= (MPYDELAY[0])? f_rpthree_ic : f_rp2three_ic;
|
|
assign fp_three_id= (MPYDELAY[0])? f_rpthree_id : f_rp2three_id;
|
|
`endif
|
|
|
end else if (CKPCE <= 3)
|
end else if (CKPCE <= 3)
|
begin : CKPCE_THREE
|
begin : CKPCE_THREE
|
// Coefficient multiply inputs
|
// Coefficient multiply inputs
|
reg [3*(CWIDTH+1)-1:0] mpy_pipe_c;
|
reg [3*(CWIDTH+1)-1:0] mpy_pipe_c;
|
// Data multiply inputs
|
// Data multiply inputs
|
| Line 374... |
Line 480... |
reg mpy_pipe_v;
|
reg mpy_pipe_v;
|
reg [2:0] ce_phase;
|
reg [2:0] ce_phase;
|
|
|
reg signed [ (CWIDTH+IWIDTH+3)-1:0] mpy_pipe_out;
|
reg signed [ (CWIDTH+IWIDTH+3)-1:0] mpy_pipe_out;
|
|
|
|
`ifdef FORMAL
|
|
wire [CWIDTH:0] f_past_ic;
|
|
wire [IWIDTH+1:0] f_past_id;
|
|
|
|
reg [CWIDTH:0] f_rpone_ic, f_rptwo_ic, f_rpthree_ic,
|
|
f_rp2one_ic, f_rp2two_ic, f_rp2three_ic,
|
|
f_rp3one_ic;
|
|
reg [IWIDTH+1:0] f_rpone_id, f_rptwo_id, f_rpthree_id,
|
|
f_rp2one_id, f_rp2two_id, f_rp2three_id,
|
|
f_rp3one_id;
|
|
`endif
|
|
|
initial ce_phase = 3'b011;
|
initial ce_phase = 3'b011;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
ce_phase <= 3'b011;
|
ce_phase <= 3'b011;
|
else if (i_ce)
|
else if (i_ce)
|
| Line 408... |
Line 526... |
mpy_pipe_d[3*(IWIDTH+2)-1:0] <= {
|
mpy_pipe_d[3*(IWIDTH+2)-1:0] <= {
|
mpy_pipe_d[2*(IWIDTH+2)-1:0], {(IWIDTH+2){1'b0}} };
|
mpy_pipe_d[2*(IWIDTH+2)-1:0], {(IWIDTH+2){1'b0}} };
|
end
|
end
|
|
|
longbimpy #(CWIDTH+1,IWIDTH+2) mpy(i_clk, mpy_pipe_v,
|
longbimpy #(CWIDTH+1,IWIDTH+2) mpy(i_clk, mpy_pipe_v,
|
mpy_pipe_vc, mpy_pipe_vd, mpy_pipe_out);
|
mpy_pipe_vc, mpy_pipe_vd, mpy_pipe_out
|
|
`ifdef FORMAL
|
|
, f_past_ic, f_past_id
|
|
`endif
|
|
);
|
|
|
reg signed [((IWIDTH+2)+(CWIDTH+1)-1):0]
|
reg signed [((IWIDTH+2)+(CWIDTH+1)-1):0]
|
rp_one, rp_two, rp_three,
|
rp_one, rp_two, rp_three,
|
rp2_one, rp2_two, rp2_three,
|
rp2_one, rp2_two, rp2_three,
|
rp3_one;
|
rp3_one;
|
| Line 420... |
Line 542... |
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (MPYREMAINDER == 0)
|
if (MPYREMAINDER == 0)
|
begin
|
begin
|
|
|
if (i_ce)
|
if (i_ce)
|
|
begin
|
rp_two <= mpy_pipe_out;
|
rp_two <= mpy_pipe_out;
|
else if (ce_phase == 3'b000)
|
`ifdef FORMAL
|
|
f_rptwo_ic <= f_past_ic;
|
|
f_rptwo_id <= f_past_id;
|
|
`endif
|
|
end else if (ce_phase == 3'b000)
|
|
begin
|
rp_three <= mpy_pipe_out;
|
rp_three <= mpy_pipe_out;
|
else if (ce_phase == 3'b001)
|
`ifdef FORMAL
|
|
f_rpthree_ic <= f_past_ic;
|
|
f_rpthree_id <= f_past_id;
|
|
`endif
|
|
end else if (ce_phase == 3'b001)
|
|
begin
|
rp_one <= mpy_pipe_out;
|
rp_one <= mpy_pipe_out;
|
|
`ifdef FORMAL
|
|
f_rpone_ic <= f_past_ic;
|
|
f_rpone_id <= f_past_id;
|
|
`endif
|
|
end
|
end else if (MPYREMAINDER == 1)
|
end else if (MPYREMAINDER == 1)
|
begin
|
begin
|
|
|
if (i_ce)
|
if (i_ce)
|
|
begin
|
rp_one <= mpy_pipe_out;
|
rp_one <= mpy_pipe_out;
|
else if (ce_phase == 3'b000)
|
`ifdef FORMAL
|
|
f_rpone_ic <= f_past_ic;
|
|
f_rpone_id <= f_past_id;
|
|
`endif
|
|
end else if (ce_phase == 3'b000)
|
|
begin
|
rp_two <= mpy_pipe_out;
|
rp_two <= mpy_pipe_out;
|
else if (ce_phase == 3'b001)
|
`ifdef FORMAL
|
|
f_rptwo_ic <= f_past_ic;
|
|
f_rptwo_id <= f_past_id;
|
|
`endif
|
|
end else if (ce_phase == 3'b001)
|
|
begin
|
rp_three <= mpy_pipe_out;
|
rp_three <= mpy_pipe_out;
|
|
`ifdef FORMAL
|
|
f_rpthree_ic <= f_past_ic;
|
|
f_rpthree_id <= f_past_id;
|
|
`endif
|
|
end
|
end else // if (MPYREMAINDER == 2)
|
end else // if (MPYREMAINDER == 2)
|
begin
|
begin
|
|
|
if (i_ce)
|
if (i_ce)
|
|
begin
|
rp_three <= mpy_pipe_out;
|
rp_three <= mpy_pipe_out;
|
else if (ce_phase == 3'b000)
|
`ifdef FORMAL
|
|
f_rpthree_ic <= f_past_ic;
|
|
f_rpthree_id <= f_past_id;
|
|
`endif
|
|
end else if (ce_phase == 3'b000)
|
|
begin
|
rp_one <= mpy_pipe_out;
|
rp_one <= mpy_pipe_out;
|
else if (ce_phase == 3'b001)
|
`ifdef FORMAL
|
|
f_rpone_ic <= f_past_ic;
|
|
f_rpone_id <= f_past_id;
|
|
`endif
|
|
end else if (ce_phase == 3'b001)
|
|
begin
|
rp_two <= mpy_pipe_out;
|
rp_two <= mpy_pipe_out;
|
|
`ifdef FORMAL
|
|
f_rptwo_ic <= f_past_ic;
|
|
f_rptwo_id <= f_past_id;
|
|
`endif
|
|
end
|
end
|
end
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_ce)
|
if (i_ce)
|
begin
|
begin
|
rp2_one <= rp_one;
|
rp2_one <= rp_one;
|
rp2_two <= rp_two;
|
rp2_two <= rp_two;
|
rp2_three <= (MPYREMAINDER == 2) ? mpy_pipe_out : rp_three;
|
rp2_three <= (MPYREMAINDER == 2) ? mpy_pipe_out : rp_three;
|
rp3_one <= (MPYREMAINDER == 0) ? rp2_one : rp_one;
|
rp3_one <= (MPYREMAINDER == 0) ? rp2_one : rp_one;
|
|
`ifdef FORMAL
|
|
f_rp2one_ic <= f_rpone_ic;
|
|
f_rp2one_id <= f_rpone_id;
|
|
|
|
f_rp2two_ic <= f_rptwo_ic;
|
|
f_rp2two_id <= f_rptwo_id;
|
|
|
|
f_rp2three_ic <= (MPYREMAINDER==2) ? f_past_ic : f_rpthree_ic;
|
|
f_rp2three_id <= (MPYREMAINDER==2) ? f_past_id : f_rpthree_id;
|
|
f_rp3one_ic <= (MPYREMAINDER==0) ? f_rp2one_ic : f_rpone_ic;
|
|
f_rp3one_id <= (MPYREMAINDER==0) ? f_rp2one_id : f_rpone_id;
|
|
`endif
|
end
|
end
|
|
|
assign p_one = rp3_one;
|
assign p_one = rp3_one;
|
assign p_two = rp2_two;
|
assign p_two = rp2_two;
|
assign p_three = rp2_three;
|
assign p_three = rp2_three;
|
|
|
|
`ifdef FORMAL
|
|
assign fp_one_ic = f_rp3one_ic;
|
|
assign fp_one_id = f_rp3one_id;
|
|
|
|
assign fp_two_ic = f_rp2two_ic;
|
|
assign fp_two_id = f_rp2two_id;
|
|
|
|
assign fp_three_ic = f_rp2three_ic;
|
|
assign fp_three_id = f_rp2three_id;
|
|
`endif
|
|
|
end endgenerate
|
end endgenerate
|
// These values are held in memory and delayed during the
|
// These values are held in memory and delayed during the
|
// multiply. Here, we recover them. During the multiply,
|
// multiply. Here, we recover them. During the multiply,
|
// values were multiplied by 2^(CWIDTH-2)*exp{-j*2*pi*...},
|
// values were multiplied by 2^(CWIDTH-2)*exp{-j*2*pi*...},
|
// therefore, the left_x values need to be right shifted by
|
// therefore, the left_x values need to be right shifted by
|
// CWIDTH-2 as well. The additional bits come from a sign
|
// CWIDTH-2 as well. The additional bits come from a sign
|
// extension.
|
// extension.
|
wire signed [(IWIDTH+CWIDTH):0] fifo_i, fifo_r;
|
wire signed [(IWIDTH+CWIDTH):0] fifo_i, fifo_r;
|
reg [(2*IWIDTH+1):0] fifo_read;
|
reg [(2*IWIDTH+1):0] fifo_read;
|
assign fifo_r = { {2{fifo_read[2*(IWIDTH+1)-1]}}, fifo_read[(2*(IWIDTH+1)-1):(IWIDTH+1)], {(CWIDTH-2){1'b0}} };
|
assign fifo_r = { {2{fifo_read[2*(IWIDTH+1)-1]}},
|
assign fifo_i = { {2{fifo_read[(IWIDTH+1)-1]}}, fifo_read[((IWIDTH+1)-1):0], {(CWIDTH-2){1'b0}} };
|
fifo_read[(2*(IWIDTH+1)-1):(IWIDTH+1)], {(CWIDTH-2){1'b0}} };
|
|
assign fifo_i = { {2{fifo_read[(IWIDTH+1)-1]}},
|
|
fifo_read[((IWIDTH+1)-1):0], {(CWIDTH-2){1'b0}} };
|
|
|
|
|
reg signed [(CWIDTH+IWIDTH+3-1):0] mpy_r, mpy_i;
|
reg signed [(CWIDTH+IWIDTH+3-1):0] mpy_r, mpy_i;
|
|
|
// Let's do some rounding and remove unnecessary bits.
|
// Let's do some rounding and remove unnecessary bits.
|
| Line 556... |
Line 749... |
// has (2*OWIDTH) bits in it, with the top half being the real
|
// has (2*OWIDTH) bits in it, with the top half being the real
|
// portion and the bottom half being the imaginary portion.
|
// portion and the bottom half being the imaginary portion.
|
assign o_left = { rnd_left_r, rnd_left_i };
|
assign o_left = { rnd_left_r, rnd_left_i };
|
assign o_right= { rnd_right_r,rnd_right_i};
|
assign o_right= { rnd_right_r,rnd_right_i};
|
|
|
`ifdef VERILATOR
|
|
`define FORMAL
|
|
`endif
|
|
`ifdef FORMAL
|
`ifdef FORMAL
|
localparam F_LGDEPTH = (AUXLEN > 64) ? 7
|
|
: (AUXLEN > 32) ? 6
|
|
: (AUXLEN > 16) ? 5
|
|
: (AUXLEN > 8) ? 4
|
|
: (AUXLEN > 4) ? 3 : 2;
|
|
|
|
localparam F_DEPTH = AUXLEN;
|
|
localparam [F_LGDEPTH-1:0] F_D = F_DEPTH[F_LGDEPTH-1:0]-1;
|
|
|
|
reg signed [IWIDTH-1:0] f_dlyleft_r [0:F_DEPTH-1];
|
|
reg signed [IWIDTH-1:0] f_dlyleft_i [0:F_DEPTH-1];
|
|
reg signed [IWIDTH-1:0] f_dlyright_r [0:F_DEPTH-1];
|
|
reg signed [IWIDTH-1:0] f_dlyright_i [0:F_DEPTH-1];
|
|
reg signed [CWIDTH-1:0] f_dlycoeff_r [0:F_DEPTH-1];
|
|
reg signed [CWIDTH-1:0] f_dlycoeff_i [0:F_DEPTH-1];
|
|
reg signed [F_DEPTH-1:0] f_dlyaux;
|
|
|
|
initial f_dlyaux[0] = 0;
|
initial f_dlyaux[0] = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
f_dlyaux <= 0;
|
f_dlyaux <= 0;
|
else if (i_ce)
|
else if (i_ce)
|
| Line 614... |
Line 787... |
end
|
end
|
|
|
end endgenerate
|
end endgenerate
|
|
|
`ifndef VERILATOR
|
`ifndef VERILATOR
|
always @(posedge i_clk)
|
//
|
if ((!$past(i_ce))&&(!$past(i_ce,2))&&(!$past(i_ce,3))
|
// Make some i_ce restraining assumptions. These are necessary
|
&&(!$past(i_ce,4)))
|
// to get the design to pass induction.
|
assume(i_ce);
|
//
|
|
|
generate if (CKPCE <= 1)
|
generate if (CKPCE <= 1)
|
begin
|
begin
|
|
|
// i_ce is allowed to be anything in this mode
|
// No primary i_ce assumption. i_ce can be anything
|
|
//
|
|
// First induction i_ce assumption: No more than one
|
|
// empty cycle between used cycles. Without this
|
|
// assumption, or one like it, induction would never
|
|
// complete.
|
|
always @(posedge i_clk)
|
|
if ((!$past(i_ce)))
|
|
assume(i_ce);
|
|
|
|
// Second induction i_ce assumption: avoid skipping an
|
|
// i_ce and thus stretching out the i_ce cycle two i_ce
|
|
// cycles in a row. Without this assumption, induction
|
|
// would still complete, it would just take longer
|
|
always @(posedge i_clk)
|
|
if (($past(i_ce))&&(!$past(i_ce,2)))
|
|
assume(i_ce);
|
|
|
end else if (CKPCE == 2)
|
end else if (CKPCE == 2)
|
begin : F_CKPCE_TWO
|
begin : F_CKPCE_TWO
|
|
|
|
// Primary i_ce assumption: Every i_ce cycle is followed
|
|
// by a non-i_ce cycle, so the multiplies can be
|
|
// multiplexed
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ($past(i_ce))
|
if ($past(i_ce))
|
assume(!i_ce);
|
assume(!i_ce);
|
|
// First induction assumption: Don't let this stretch
|
|
// out too far. This is necessary to pass induction
|
|
always @(posedge i_clk)
|
|
if ((!$past(i_ce))&&(!$past(i_ce,2)))
|
|
assume(i_ce);
|
|
|
|
always @(posedge i_clk)
|
|
if ((!$past(i_ce))&&($past(i_ce,2))
|
|
&&(!$past(i_ce,3))&&(!$past(i_ce,4)))
|
|
assume(i_ce);
|
|
|
end else if (CKPCE == 3)
|
end else if (CKPCE == 3)
|
begin : F_CKPCE_THREE
|
begin : F_CKPCE_THREE
|
|
|
|
// Primary i_ce assumption: Following any i_ce cycle,
|
|
// there must be two clock cycles with i_ce de-asserted
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (($past(i_ce))||($past(i_ce,2)))
|
if (($past(i_ce))||($past(i_ce,2)))
|
assume(!i_ce);
|
assume(!i_ce);
|
|
|
|
// Induction assumption: Allow i_ce's every third or
|
|
// fourth clock, but don't allow them to be separated
|
|
// further than that
|
|
always @(posedge i_clk)
|
|
if ((!$past(i_ce))&&(!$past(i_ce,2))&&(!$past(i_ce,3)))
|
|
assume(i_ce);
|
|
|
|
// Second induction assumption, to speed up the proof:
|
|
// If it's the earliest possible opportunity for an
|
|
// i_ce, and the last i_ce was late, don't let this one
|
|
// be late as well.
|
|
always @(posedge i_clk)
|
|
if ((!$past(i_ce))&&(!$past(i_ce,2))
|
|
&&($past(i_ce,3))&&(!$past(i_ce,4))
|
|
&&(!$past(i_ce,5))&&(!$past(i_ce,6)))
|
|
assume(i_ce);
|
|
|
end endgenerate
|
end endgenerate
|
`endif
|
`endif
|
|
|
reg [F_LGDEPTH:0] f_startup_counter;
|
reg [F_LGDEPTH:0] f_startup_counter;
|
initial f_startup_counter = 0;
|
initial f_startup_counter = 0;
|
| Line 649... |
Line 869... |
if (i_reset)
|
if (i_reset)
|
f_startup_counter <= 0;
|
f_startup_counter <= 0;
|
else if ((i_ce)&&(!(&f_startup_counter)))
|
else if ((i_ce)&&(!(&f_startup_counter)))
|
f_startup_counter <= f_startup_counter + 1;
|
f_startup_counter <= f_startup_counter + 1;
|
|
|
wire signed [IWIDTH:0] f_sumr, f_sumi;
|
|
always @(*)
|
always @(*)
|
begin
|
begin
|
f_sumr = f_dlyleft_r[F_D] + f_dlyright_r[F_D];
|
f_sumr = f_dlyleft_r[F_D] + f_dlyright_r[F_D];
|
f_sumi = f_dlyleft_i[F_D] + f_dlyright_i[F_D];
|
f_sumi = f_dlyleft_i[F_D] + f_dlyright_i[F_D];
|
end
|
end
|
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_sumrx, f_sumix;
|
|
assign f_sumrx = { {(4){f_sumr[IWIDTH]}}, f_sumr, {(CWIDTH-2){1'b0}} };
|
assign f_sumrx = { {(4){f_sumr[IWIDTH]}}, f_sumr, {(CWIDTH-2){1'b0}} };
|
assign f_sumix = { {(4){f_sumi[IWIDTH]}}, f_sumi, {(CWIDTH-2){1'b0}} };
|
assign f_sumix = { {(4){f_sumi[IWIDTH]}}, f_sumi, {(CWIDTH-2){1'b0}} };
|
|
|
wire signed [IWIDTH:0] f_difr, f_difi;
|
|
always @(*)
|
always @(*)
|
begin
|
begin
|
f_difr = f_dlyleft_r[F_D] - f_dlyright_r[F_D];
|
f_difr = f_dlyleft_r[F_D] - f_dlyright_r[F_D];
|
f_difi = f_dlyleft_i[F_D] - f_dlyright_i[F_D];
|
f_difi = f_dlyleft_i[F_D] - f_dlyright_i[F_D];
|
end
|
end
|
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_difrx, f_difix;
|
|
assign f_difrx = { {(CWIDTH+2){f_difr[IWIDTH]}}, f_difr };
|
assign f_difrx = { {(CWIDTH+2){f_difr[IWIDTH]}}, f_difr };
|
assign f_difix = { {(CWIDTH+2){f_difi[IWIDTH]}}, f_difi };
|
assign f_difix = { {(CWIDTH+2){f_difi[IWIDTH]}}, f_difi };
|
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_widecoeff_r, f_widecoeff_i;
|
|
assign f_widecoeff_r ={ {(IWIDTH+3){f_dlycoeff_r[F_D][CWIDTH-1]}},
|
assign f_widecoeff_r ={ {(IWIDTH+3){f_dlycoeff_r[F_D][CWIDTH-1]}},
|
f_dlycoeff_r[F_D] };
|
f_dlycoeff_r[F_D] };
|
assign f_widecoeff_i ={ {(IWIDTH+3){f_dlycoeff_i[F_D][CWIDTH-1]}},
|
assign f_widecoeff_i ={ {(IWIDTH+3){f_dlycoeff_i[F_D][CWIDTH-1]}},
|
f_dlycoeff_i[F_D] };
|
f_dlycoeff_i[F_D] };
|
|
|
| Line 727... |
Line 942... |
// moving our test one clock earlier. If nothing else, it should
|
// moving our test one clock earlier. If nothing else, it should
|
// help induction finish one (or more) clocks ealier than
|
// help induction finish one (or more) clocks ealier than
|
// otherwise
|
// otherwise
|
|
|
|
|
wire signed [IWIDTH:0] f_predifr, f_predifi;
|
|
always @(*)
|
always @(*)
|
begin
|
begin
|
f_predifr = f_dlyleft_r[F_D-1] - f_dlyright_r[F_D-1];
|
f_predifr = f_dlyleft_r[F_D-1] - f_dlyright_r[F_D-1];
|
f_predifi = f_dlyleft_i[F_D-1] - f_dlyright_i[F_D-1];
|
f_predifi = f_dlyleft_i[F_D-1] - f_dlyright_i[F_D-1];
|
end
|
end
|
|
|
wire signed [IWIDTH+CWIDTH+3-1:0] f_predifrx, f_predifix;
|
|
assign f_predifrx = { {(CWIDTH+2){f_predifr[IWIDTH]}}, f_predifr };
|
assign f_predifrx = { {(CWIDTH+2){f_predifr[IWIDTH]}}, f_predifr };
|
assign f_predifix = { {(CWIDTH+2){f_predifi[IWIDTH]}}, f_predifi };
|
assign f_predifix = { {(CWIDTH+2){f_predifi[IWIDTH]}}, f_predifi };
|
|
|
wire signed [CWIDTH:0] f_sumcoef;
|
|
wire signed [IWIDTH+1:0] f_sumdiff;
|
|
always @(*)
|
always @(*)
|
begin
|
begin
|
f_sumcoef = f_dlycoeff_r[F_D-1] + f_dlycoeff_i[F_D-1];
|
f_sumcoef = f_dlycoeff_r[F_D-1] + f_dlycoeff_i[F_D-1];
|
f_sumdiff = f_predifr + f_predifi;
|
f_sumdiff = f_predifr + f_predifi;
|
end
|
end
|
| Line 783... |
Line 994... |
assert(p_three == f_sumdiff);
|
assert(p_three == f_sumdiff);
|
if (f_sumdiff == 1)
|
if (f_sumdiff == 1)
|
assert(p_three == f_sumcoef);
|
assert(p_three == f_sumcoef);
|
// verilator lint_on WIDTH
|
// verilator lint_on WIDTH
|
`ifdef VERILATOR
|
`ifdef VERILATOR
|
|
// Check that the multiplies match--but *ONLY* if using
|
|
// Verilator, and not if using formal proper
|
assert(p_one == f_predifr * f_dlycoeff_r[F_D-1]);
|
assert(p_one == f_predifr * f_dlycoeff_r[F_D-1]);
|
assert(p_two == f_predifi * f_dlycoeff_i[F_D-1]);
|
assert(p_two == f_predifi * f_dlycoeff_i[F_D-1]);
|
assert(p_three == f_sumdiff * f_sumcoef);
|
assert(p_three == f_sumdiff * f_sumcoef);
|
`endif // VERILATOR
|
`endif // VERILATOR
|
end
|
end
|
|
|
|
// The following logic formally insists that our version of the
|
|
// inputs to the multiply matches what the (multiclock) multiply
|
|
// thinks its inputs were. While this may seem redundant, the
|
|
// proof will not complete in any reasonable amount of time
|
|
// without these assertions.
|
|
|
|
assign f_p3c_in = f_dlycoeff_i[F_D-1] + f_dlycoeff_r[F_D-1];
|
|
assign f_p3d_in = f_predifi + f_predifr;
|
|
|
|
always @(*)
|
|
if (f_startup_counter >= { 1'b0, F_D })
|
|
begin
|
|
assert(fp_one_ic == { f_dlycoeff_r[F_D-1][CWIDTH-1],
|
|
f_dlycoeff_r[F_D-1][CWIDTH-1:0] });
|
|
assert(fp_two_ic == { f_dlycoeff_i[F_D-1][CWIDTH-1],
|
|
f_dlycoeff_i[F_D-1][CWIDTH-1:0] });
|
|
assert(fp_one_id == { f_predifr[IWIDTH], f_predifr });
|
|
assert(fp_two_id == { f_predifi[IWIDTH], f_predifi });
|
|
assert(fp_three_ic == f_p3c_in);
|
|
assert(fp_three_id == f_p3d_in);
|
|
end
|
|
|
// F_CHECK will be set externally by the solver, so that we can
|
// F_CHECK will be set externally by the solver, so that we can
|
// double check that the solver is actually testing what we think
|
// double check that the solver is actually testing what we think
|
// it is testing. We'll set it here to MPYREMAINDER, which will
|
// it is testing. We'll set it here to MPYREMAINDER, which will
|
// essentially eliminate the check--unless overridden by the
|
// essentially eliminate the check--unless overridden by the
|
// solver.
|
// solver.
|
