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

Subversion Repositories dblclockfft

[/] [dblclockfft/] [trunk/] [rtl/] [butterfly.v] - Diff between revs 36 and 39

Show entire file | Details | Blame | View Log

Rev 36 Rev 39
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.

powered by: WebSVN 2.1.0

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