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

Subversion Repositories dblclockfft

[/] [dblclockfft/] [trunk/] [rtl/] [windowfn.v] - Blame information for rev 41

Go to most recent revision | Details | Compare with Previous | View Log


////////////////////////////////////////////////////////////////////////////////
//
// Filename:    windowfn.v
//
// Project:     A General Purpose Pipelined FFT Implementation
//
// Purpose:     Apply a window function to incoming real data points, so as
//              to create an outgoing stream of data samples that can be used
//      in an FFT construct using 50% overlap.  The overlap, coupled with the
//      FFT's requirements, can make for somewhat of a problem.  Hence, there
//      are two 'ce' signals coming into the core.  A primary ce signal when
//      new data is ready, and an alternate that must take place between
//      primary signals.  This allows the second/alternate CE signal to be
//      appropriately spaced between the primary CE signals so that the
//      outgoing signals to the FFT will still meet separation
//      requirements--whatever they would be for the application.
//
//      For this module, the window size is the FFT length.
//
// Ports:
//      i_clk, i_reset  Should be self explanatory.  The reset is assumed to
//                      be synchronous.
//
//      i_tap_wr, i_tap For use when OPT_FIXED_TAPS is zero, i_tap_wr signals
//                      that a "tap" or "coefficient" of the filter should be
//              written.  When i_tap_wr is high, i_tap is taken to be
//              a coefficient to the core.  There's an internal address
//              counter, so no address need be given.  However, the counter is
//              reset on an i_reset signal.
//
//      i_ce, i_alt_ce  As discussed above, these signals need to alternate
//              back and forth.  Following a reset, the first signal coming in
//              should be an i_ce signal.
//
//      i_sample        The incoming sample data, valid any time i_ce is true,
//                      and accepted into the core on that clock tick.
//
//      o_ce            True when the core has a valid output
//      o_sample        The output calculated by the core, ready to pass to
//                      the FFT
//      o_frame         True on the first sample of any frame.  Following a
//                      reset, o_ce will remain false until o_frame is also
//              true with it.  From then on out, o_frame will be true once
//              every FFT length.
//
//      For a timing/signaling diagram, please feel free to run the formal
//      tools in cover mode for this module, 'sby -f windowfn.sby cover',
//      and then check out the generated trace.
//
//
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2018, Gisselquist Technology, LLC
//
// This file is part of the general purpose pipelined FFT project.
//
// 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.
//
// 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:     LGPL, v3, as defined and found on www.gnu.org,
//              http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype        none
//
module  windowfn(i_clk, i_reset, i_tap_wr, i_tap,
                i_ce, i_sample, i_alt_ce,
                o_frame, o_ce, o_sample);
        parameter               IW=16, OW=16, TW=16, LGNFFT = 4;
        parameter       [0:0]     OPT_FIXED_TAPS = 1'b0;
        parameter               INITIAL_COEFFS = "";
        //
        localparam      AW=IW+TW;
        //
        input   wire                    i_clk, i_reset;
        //
        input   wire                    i_tap_wr;
        input   wire    [(TW-1):0]       i_tap;
        //
        input   wire                    i_ce;
        input   wire    [(IW-1):0]       i_sample;
        input   wire                    i_alt_ce;
        //
        output  reg                     o_frame, o_ce;
        output  reg     [(OW-1):0]       o_sample;
 
 
        reg     [(TW-1):0]       cmem    [0:(1<<LGNFFT)-1];
        reg     [(TW-1):0]       dmem    [0:(1<<LGNFFT)-1];
 
        //
        // LOAD THE TAPS
        //
        wire    [LGNFFT-1:0]     tapwidx;
        generate if (OPT_FIXED_TAPS)
        begin : SET_FIXED_TAPS
 
                initial $readmemh(INITIAL_COEFFS, cmem);
 
                assign  tapwidx = 0;
                // Make Verilators -Wall happy
                // Verilator lint_off UNUSED
                wire    [TW:0]   ignored_inputs;
                assign  ignored_inputs = { i_tap_wr, i_tap };
                // Verilator lint_on  UNUSED
 
        end else begin : DYNAMICALLY_SET_TAPS
 
                // Coef memory write index
                reg     [(LGNFFT-1):0]   r_tapwidx;
 
                initial r_tapwidx = 0;
                always @(posedge i_clk)
                        if(i_reset)
                                r_tapwidx <= 0;
                        else if (i_tap_wr)
                                r_tapwidx <= r_tapwidx + 1'b1;
 
                if (INITIAL_COEFFS != 0)
                        initial $readmemh(INITIAL_COEFFS, cmem);
                always @(posedge i_clk)
                        if (i_tap_wr)
                                cmem[r_tapwidx] <= i_tap;
 
                assign  tapwidx = r_tapwidx;
        end endgenerate
 
 
        reg             [LGNFFT-1:0]     dwidx, didx;
        reg             [LGNFFT-1:0]     tidx;
        reg                             top_of_block, first_block;
        reg             [1:0]            frame_count;
        reg                             p_ce, d_ce;
        reg     signed  [IW-1:0] data;
        reg     signed  [TW-1:0] tap;
 
 
 
        //
        //
        // Record the incoming data into a local memory
        //
        //
 
        // Notice how this data writing section is *independent* of the reset,
        // depending only upon new sample data.
 
        initial dwidx = 0;
        always @(posedge i_clk)
        if (i_reset)
                dwidx <= 0;
        else if (i_ce)
                dwidx <= dwidx + 1'b1;
        always @(posedge i_clk)
        if (i_ce)
                dmem[dwidx] <= i_sample;
 
        initial first_block = 1'b1;
        always @(posedge i_clk)
        if (i_reset)
                first_block <= 1'b1;
        else if ((i_alt_ce)&&(&tidx)&&(dwidx==0))
                first_block <= 1'b0;
 
 
        //
        //
        // Keep track of the top of the block.  The top of the block is the
        // first incoming data sample on an FFT or half FFT boundary.  This
        // is where data processing starts from.
        //
        initial top_of_block = 1'b0;
        always @(posedge i_clk)
        if (i_reset)
                top_of_block <= 1'b0;
        else if (i_alt_ce)
                top_of_block <= (&tidx)&&((!first_block)||(dwidx==0));
        else if (i_ce)
                top_of_block <= 1'b0;
 
        //
        // Data and coefficient memory indices.
        //
        initial didx = 0;
        always @(posedge i_clk)
        if (i_reset)
                didx <= 0;
        else if ((i_alt_ce)&&(dwidx[LGNFFT-2:0]==0))
        begin
                didx[LGNFFT-2:0] <= 0;
                didx[LGNFFT-1] <= dwidx[LGNFFT-1];
        end else if ((i_ce)||(i_alt_ce))
                // Process the next point in this FFT
                didx <= didx + 1'b1;
 
        initial tidx = 0;
        always @(posedge i_clk)
        if (i_reset)
                tidx <= 0;
        else if ((i_alt_ce)&&(dwidx[LGNFFT-2:0]==0))
        begin
                // // At the beginning of processing for a given FFT
                tidx <= 0;
        end else if ((i_ce)||(i_alt_ce))
                // Process the next point in the window function
                tidx <= tidx + 1'b1;
 
        initial frame_count = 0;
        always @(posedge i_clk)
        if (i_reset)
                frame_count <= 0;
        else if ((i_ce)&&(top_of_block)&&(!first_block))
                frame_count <= 3;
        else if (frame_count != 0)
                frame_count <= frame_count - 1'b1;
 
        initial o_frame = 1'b0;
        always @(posedge i_clk)
        if (i_reset)
                o_frame <= 1'b0;
        else if (frame_count == 2)
                o_frame <= 1'b1;
        else
                o_frame <= 1'b0;
 
        //
        // Following any initial i_ce, ...
        //      d_ce: The data (and coefficient), read from memory,will be valid
        //      p_ce: The produc of data and coefficient is valid
        //
        initial { p_ce, d_ce } = 2'h0;
        always @(posedge i_clk)
        if (i_reset)
                { p_ce, d_ce } <= 2'h0;
        else
                { p_ce, d_ce } <= { d_ce, (!first_block)&&((i_ce)||(i_alt_ce)) };
 
        // Read the data sample point, and the filter coefficient, from block
        // RAM.  Because this is block RAM, we have to be careful not to
        // do anything else here.
        initial data = 0;
        initial tap = 0;
        always @(posedge i_clk)
        begin
                data <= dmem[didx];
                tap  <= cmem[tidx];
        end
 
        //
        // Multiply the two values together
         reg    signed  [IW+TW-1:0]      product;
`ifdef  FORMAL
        // We'll implement an abstract multiply below--just to make sure the
        // timing is right.
`else
        always @(posedge i_clk)
                product <= data * tap;
`endif
 
        //
        // Output CE
        //
        initial o_ce = 0;
        always @(posedge i_clk)
        if (i_reset)
                o_ce <= 0;
        else
                o_ce <= p_ce;
 
        generate if (OW == AW)
        begin : BIT_ADJUSTMENT_NONE
 
                initial o_sample = 0;
                always @(posedge i_clk)
                if (i_reset)
                        o_sample <= 0;
                else if (p_ce)
                        o_sample <= product;
 
        end else if (OW < AW)
        begin : BIT_ADJUSTMENT_ROUNDING
                wire    [AW-1:0] rounded;
 
                assign  rounded = product + { {(OW){1'b0}}, product[AW-OW],
                                {(AW-OW-1){!product[AW-OW]}} };
 
                initial o_sample = 0;
                always @(posedge i_clk)
                if (i_reset)
                        o_sample <= 0;
                else if (p_ce)
                        o_sample <= rounded[(AW-1):(AW-OW)];
 
                // Make Verilator happy
                // verilator lint_off UNUSED
                wire    [AW-OW-1:0]      unused_rounding_bits;
                assign  unused_rounding_bits = rounded[AW-OW-1:0];
                // verilator lint_on  UNUSED
 
        end else // if (OW > AW)
        begin : BIT_ADJUSTMENT_EXTENDING
 
                always @(posedge i_clk)
                if (i_reset)
                        o_sample <= 0;
                else if (p_ce)
                        o_sample <= { product, {(OW-AW){1'b0}} };
 
        end endgenerate
 
        // Make Verilator happy
        // verilator lint_off UNUSED
        wire    [LGNFFT-1:0]     unused;
        assign  unused = tapwidx;
        // verilator lint_on  UNUSED
 
`ifdef  FORMAL
        reg     f_past_valid;
        initial f_past_valid = 1'b0;
        always @(posedge i_clk)
                f_past_valid <= 1'b1;
 
        // Keep track of the phase of this operation
        reg     [LGNFFT:0]       f_phase;
 
        initial f_phase = 0;
        always @(posedge i_clk)
        if (i_reset)
        begin
                f_phase <= 0;
        end else if ((i_ce)&&(top_of_block))
                f_phase[LGNFFT-1:0] <= 1;
        else if ((i_ce)||(i_alt_ce))
                f_phase <= f_phase + 1;
 
        ///////
        //
        // Assumptions about the input
        always @(posedge i_clk)
        if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_ce)))
                restrict($stable(i_sample));
 
        always @(*)
        if (tapwidx != 0)
                assume(!i_ce);
 
        always @(posedge i_clk)
        if (f_phase[0])
                assume(!i_ce);
 
        always @(posedge i_clk)
        if (!f_phase[0])
                assume(!i_alt_ce);
 
        always @(*)
        if (i_tap_wr)
                assume((!i_ce)&&(!i_alt_ce));
 
        always @(*)
                assume(!i_tap_wr);
 
        always @(*)
        if ((i_ce)&&(top_of_block))
        begin
                assert(dwidx[LGNFFT-2:0]==0);
                assert(didx[LGNFFT-2:0]==0);
        end else if (dwidx[LGNFFT-2:0]!=0)
                assert(!top_of_block);
 
        always @(*)
        if ((dwidx[LGNFFT-2:0]==0)&&(!didx[0]))
                assert(top_of_block||f_first_block||first_block);
        else
                assert(!top_of_block);
 
        always @(posedge i_clk)
        if ((f_past_valid)&&($past(first_block))&&(!first_block))
                assert(top_of_block);
 
        /*
        always @(posedge i_clk)
        if (f_past_valid)
        begin
                if ($past(i_reset))
                        assert(!top_of_block);
                else if ($past(i_ce))
                        assert(top_of_block == ((!first_block)&&(dwidx[LGNFFT-2:0]==0)));
                else
 
                        assert(top_of_block == ((!first_block)&&(&dwidx[LGNFFT-2:1])));
        end
        */
 
        always @(posedge i_clk)
        if ((f_past_valid)&&($past(first_block))&&(!$past(first_block)))
                assert(top_of_block);
 
        //////////////////////////////////////////////////////////////////
        //
        // Assertions about our outputs
        //
        /////////////////////////
        //
        //
//      always @(*)
//      if (o_frame)
//              assert(o_ce);
        always @(*)
        if (first_block)
                assert(!o_ce);
 
        reg     f_waiting_for_first_frame;
 
        initial f_waiting_for_first_frame = 1;
        always @(posedge i_clk)
        if ((i_reset)||(first_block))
                f_waiting_for_first_frame <= 1'b1;
        else if (o_ce)
                f_waiting_for_first_frame <= 1'b0;
 
        always @(*)
        if ((f_waiting_for_first_frame)&&(o_ce))
                assert(o_frame);
        always @(*)
        if (f_phase == 0)
                assert((top_of_block)||(first_block));
 
        always @(*)
        if (f_waiting_for_first_frame)
        begin
                if (f_phase[LGNFFT-1:0] > 3)
                begin
                        assert((first_block)&&(!o_frame));
                        assert({o_ce, p_ce, d_ce} == 0);
                        assert(frame_count == 0);
                end else if (f_phase == 0)
                begin
                        assert((!o_frame)&&({o_ce, p_ce, d_ce} == 0));
                        assert(frame_count == 0);
                end else if ((f_phase > 0)&&(!first_block))
                        assert(|{o_ce, p_ce, d_ce });
                else if ((frame_count != 0)||(first_block))
                        assert(!o_frame);
                else
                        assert(o_frame);
        end
 
        always @(posedge i_clk)
        if ((f_past_valid)&&(!$past(i_reset)))
                assert(o_ce || $stable(o_sample));
 
        /*
        always @(*)
                assert(m_ce == (f_phase == 0));
        always @(*)
                assert(d_ce == (f_phase == 1));
        always @(*)
                assert(p_ce == (f_phase == 2));
        always @(*)
                assert(o_ce == (f_phase == 3));
        always @(*)
                assert(o_frame == (f_phase == 3));
        */
 
        always @(*)
                assert(didx[LGNFFT-2:0] == tidx[LGNFFT-2:0]);
 
        always @(posedge i_clk)
        if ((f_past_valid)&&(!$past(i_reset))
                        &&($past(i_ce))&&($past(top_of_block)))
                assert(tidx == 1);
 
 
        wire    [LGNFFT:0]       f_phase_plus_one;
        always @(*)
                f_phase_plus_one = f_phase + 1;
        /*
        end else if ($past(i_ce))
        begin
// 1 0          // 0    0                Top of block    0
// 2 1          // 1    1       ALT                     0
// 3 1          // 2    1                               1
// 4 2          // 3    2       ALT                     1
// 5 2          // 4    2                               2
// 6 3          // 5    3       ALT                     2
// 7 3          // 6    3                               3
// 0 4          // 7    4       ALT                     3
// 1            // 4    4               Top of block    0
// 2            // 5    5                               0
//              // 6    5       ALT                     1
//              // 7    6                               1
//              // 0    6       ALT                     2
//              // 1    7                               2
//              // 2    7       ALT
//              // 3    0
//              // 0    0        ALT     Top of block
//              // 1    1
//              // 2    1
//              // 3    2
//              // 4    2
        */
        always @(*)
               assert(f_phase_plus_one[LGNFFT:1] == dwidx[LGNFFT-1:0]);
        always @(*)
                assert(f_phase[0] == didx[0]);
        always @(*)
        if (f_phase[LGNFFT])
        begin
                assert(f_phase[LGNFFT-1:0] == {!didx[LGNFFT-1],didx[LGNFFT-2:0]});
                assert((dwidx[LGNFFT-1]==1)
                                ||(dwidx[LGNFFT-2:0]==0));
        end else begin
                assert((dwidx[LGNFFT-1]==0)
                        ||((dwidx[LGNFFT-1])&&(dwidx[LGNFFT-2:0]==0)&&(&f_phase[LGNFFT-1:0])));
                assert(f_phase[LGNFFT-1:0] == didx[LGNFFT-1:0]);
        end
 
        always @(*)
                assert(f_phase[LGNFFT-1:0] == tidx[LGNFFT-1:0]);
        always @(*)
                assert(f_phase[LGNFFT-2:0] == didx[LGNFFT-2:0]);
        wire    [LGNFFT-1:0]     f_diff_idx;
        assign  f_diff_idx = didx - dwidx;
        always @(*)
        if (!first_block)
                assert(f_diff_idx < { 1'b1, {(LGNFFT-1){1'b0}} });
 
 
        always @(*)
                if (top_of_block)
                        assert(!first_block);
 
        reg     f_first_block;
        initial f_first_block = 1'b1;
        always @(posedge i_clk)
        if (i_ce)
                f_first_block <= first_block;
 
        always @(*)
        if ((top_of_block)&&(i_ce)&&(!f_first_block))
                assert(didx[LGNFFT-2:0] == dwidx[LGNFFT-2:0]);
 
        always @(*)
        if ((!f_first_block)&&(!first_block)&&(dwidx[LGNFFT-2:0]==0)
                        &&(didx[LGNFFT-1:0]==0))
                assert(top_of_block);
 
////////////////////////////////////////////////////////////////////////////////
//
//  Abstract Multiply
//
////////////////////////////////////////////////////////////////////////////////
        // Gin up a really quick abstract multiply for formal testing
        // only.  always @(posedge i_clk)
        (* anyconst *) signed reg [IW+TW-1:0] pre_product;
        always @(posedge i_clk)
        if (data == 0)
                assume(pre_product == 0);
        always @(posedge i_clk)
        if (tap == 0)
                assume(pre_product == 0);
        always @(posedge i_clk)
        if (data == 1)
                assume(pre_product == tap);
        always @(posedge i_clk)
        if (tap == 1)
                assume(pre_product == data);
        always @(posedge i_clk)
        if ((i_ce)||(i_alt_ce))
                product <= pre_product;
 
////////////////////////////////////////////////////////////////////////////////
//
//  Arbitrary memory test
//
////////////////////////////////////////////////////////////////////////////////
        (* anyconst *)          reg     [LGNFFT-1:0]     f_addr;
                        signed  reg     [TW-1:0] f_tap;
                        signed  reg     [IW-1:0] f_value, f_tap;
                                reg                     f_this_dce, f_this_pce,
                                                        f_this_oce, f_this_tap;
 
        initial assume(f_tap == cmem[f_addr]);
        always @(*)
                assert(f_tap == cmem[f_addr]);
        always @(posedge i_clk)
        if ((i_tap_wr)&&(f_addr == tapwidx))
                f_tap <= i_tap;
 
        initial f_value = 0;
        initial assume(dmem[f_addr] == f_value);
        always @(*)
                assert(f_value == dmem[f_addr]);
        always @(posedge i_clk)
        if ((i_ce)&&(dwidx == f_addr))
                f_value <= i_sample;
        initial { f_this_oce, f_this_pce, f_this_dce } = 3'h0;
        always @(posedge i_clk)
        if ((i_reset)||(i_tap_wr))
                { f_this_oce, f_this_pce, f_this_dce } <= 3'h0;
        else
                { f_this_oce, f_this_pce, f_this_dce }
                        <= { f_this_pce, f_this_dce,
                                (((i_ce)||(i_alt_ce))
                                        &&(f_past_valid)&&(f_addr == didx)) };
        initial f_this_tap = 0;
        always @(posedge i_clk)
        if (i_reset)
                f_this_tap <= 0;
        else if ((i_ce)||(i_alt_ce))
                f_this_tap <= (f_past_valid)&&(f_addr == tidx);
        else
                f_this_tap <= 0;
 
 
        always @(posedge i_clk)
        if (f_this_tap)
                assert(tap == f_tap);
 
        always @(posedge i_clk)
        if ((f_past_valid)&&(f_this_dce))
                assert(data == $past(f_value));
 
        reg     signed  [IW-1:0] f_past_data;
        reg     signed  [TW-1:0] f_past_tap;
 
        always @(posedge i_clk)
        begin
                f_past_data <= data;
                f_past_tap <= tap;
        end
 
        always @(posedge i_clk)
        if ((f_past_valid)&&(f_this_pce))
        begin
                if (f_past_tap == 0)
                        assert(product == 0);
                if (f_past_data == 0)
                        assert(product == 0);
                if (f_past_tap == 1)
                        assert(product=={{(TW){f_past_data[IW-1]}},f_past_data});
                if (f_past_data == 1)
                        assert(product=={{{IW}{f_past_tap[TW-1]}},f_past_tap});
        end
 
 
////////////////////////////////////////////////////////////////////////////////
//
//  Cover tests
//
////////////////////////////////////////////////////////////////////////////////
        reg     f_second_frame;
        initial f_second_frame = 1'b0;
        always @(posedge i_clk)
        if ((o_ce)&&(o_frame))
                f_second_frame <= 1'b1;
 
        always @(posedge i_clk)
                cover((o_ce)&&(o_frame)&&(f_second_frame));
`endif
endmodule

Browse

Tools

Subversion Repositories dblclockfft

[/] [dblclockfft/] [trunk/] [rtl/] [windowfn.v] - Blame information for rev 41

Line No.	Rev	Author	Line
1	39	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
2			`//`
3			`// Filename: windowfn.v`
4			`//`
5			`// Project: A General Purpose Pipelined FFT Implementation`
6			`//`
7			`// Purpose: Apply a window function to incoming real data points, so as`
8			`// to create an outgoing stream of data samples that can be used`
9			`// in an FFT construct using 50% overlap. The overlap, coupled with the`
10			`// FFT's requirements, can make for somewhat of a problem. Hence, there`
11			`// are two 'ce' signals coming into the core. A primary ce signal when`
12			`// new data is ready, and an alternate that must take place between`
13			`// primary signals. This allows the second/alternate CE signal to be`
14			`// appropriately spaced between the primary CE signals so that the`
15			`// outgoing signals to the FFT will still meet separation`
16			`// requirements--whatever they would be for the application.`
17			`//`
18			`// For this module, the window size is the FFT length.`
19			`//`
20			`// Ports:`
21			`// i_clk, i_reset Should be self explanatory. The reset is assumed to`
22			`// be synchronous.`
23			`//`
24			`// i_tap_wr, i_tap For use when OPT_FIXED_TAPS is zero, i_tap_wr signals`
25			`// that a "tap" or "coefficient" of the filter should be`
26			`// written. When i_tap_wr is high, i_tap is taken to be`
27			`// a coefficient to the core. There's an internal address`
28			`// counter, so no address need be given. However, the counter is`
29			`// reset on an i_reset signal.`
30			`//`
31			`// i_ce, i_alt_ce As discussed above, these signals need to alternate`
32			`// back and forth. Following a reset, the first signal coming in`
33			`// should be an i_ce signal.`
34			`//`
35			`// i_sample The incoming sample data, valid any time i_ce is true,`
36			`// and accepted into the core on that clock tick.`
37			`//`
38			`// o_ce True when the core has a valid output`
39			`// o_sample The output calculated by the core, ready to pass to`
40			`// the FFT`
41			`// o_frame True on the first sample of any frame. Following a`
42			`// reset, o_ce will remain false until o_frame is also`
43			`// true with it. From then on out, o_frame will be true once`
44			`// every FFT length.`
45			`//`
46			`// For a timing/signaling diagram, please feel free to run the formal`
47			`// tools in cover mode for this module, 'sby -f windowfn.sby cover',`
48			`// and then check out the generated trace.`
49			`//`
50			`//`
51			`// Creator: Dan Gisselquist, Ph.D.`
52			`// Gisselquist Technology, LLC`
53			`//`
54			`////////////////////////////////////////////////////////////////////////////////`
55			`//`
56			`// Copyright (C) 2018, Gisselquist Technology, LLC`
57			`//`
58			`// This file is part of the general purpose pipelined FFT project.`
59			`//`
60			`// The pipelined FFT project is free software (firmware): you can redistribute`
61			`// it and/or modify it under the terms of the GNU Lesser General Public License`
62			`// as published by the Free Software Foundation, either version 3 of the`
63			`// License, or (at your option) any later version.`
64			`//`
65			`// The pipelined FFT project is distributed in the hope that it will be useful,`
66			`// but WITHOUT ANY WARRANTY; without even the implied warranty of`
67			`// MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser`
68			`// General Public License for more details.`
69			`//`
70			`// You should have received a copy of the GNU Lesser General Public License`
71			`// along with this program. (It's in the $(ROOT)/doc directory. Run make`
72			`// with no target there if the PDF file isn't present.) If not, see`
73			`// <http://www.gnu.org/licenses/> for a copy.`
74			`//`
75			`// License: LGPL, v3, as defined and found on www.gnu.org,`
76			`// http://www.gnu.org/licenses/lgpl.html`
77			`//`
78			`//`
79			`////////////////////////////////////////////////////////////////////////////////`
80			`//`
81			`//`
82			`default_nettype none
83			`//`
84			`module windowfn(i_clk, i_reset, i_tap_wr, i_tap,`
85			`i_ce, i_sample, i_alt_ce,`
86			`o_frame, o_ce, o_sample);`
87			`parameter IW=16, OW=16, TW=16, LGNFFT = 4;`
88			`parameter [0:0] OPT_FIXED_TAPS = 1'b0;`
89			`parameter INITIAL_COEFFS = "";`
90			`//`
91			`localparam AW=IW+TW;`
92			`//`
93			`input wire i_clk, i_reset;`
94			`//`
95			`input wire i_tap_wr;`
96			`input wire [(TW-1):0] i_tap;`
97			`//`
98			`input wire i_ce;`
99			`input wire [(IW-1):0] i_sample;`
100			`input wire i_alt_ce;`
101			`//`
102			`output reg o_frame, o_ce;`
103			`output reg [(OW-1):0] o_sample;`
104
105
106			`reg [(TW-1):0] cmem [0:(1<<LGNFFT)-1];`
107			`reg [(TW-1):0] dmem [0:(1<<LGNFFT)-1];`
108
109			`//`
110			`// LOAD THE TAPS`
111			`//`
112			`wire [LGNFFT-1:0] tapwidx;`
113			`generate if (OPT_FIXED_TAPS)`
114			`begin : SET_FIXED_TAPS`
115
116			`initial $readmemh(INITIAL_COEFFS, cmem);`
117
118			`assign tapwidx = 0;`
119			`// Make Verilators -Wall happy`
120			`// Verilator lint_off UNUSED`
121			`wire [TW:0] ignored_inputs;`
122			`assign ignored_inputs = { i_tap_wr, i_tap };`
123			`// Verilator lint_on UNUSED`
124
125			`end else begin : DYNAMICALLY_SET_TAPS`
126
127			`// Coef memory write index`
128			`reg [(LGNFFT-1):0] r_tapwidx;`
129
130			`initial r_tapwidx = 0;`
131			`always @(posedge i_clk)`
132			`if(i_reset)`
133			`r_tapwidx <= 0;`
134			`else if (i_tap_wr)`
135			`r_tapwidx <= r_tapwidx + 1'b1;`
136
137			`if (INITIAL_COEFFS != 0)`
138			`initial $readmemh(INITIAL_COEFFS, cmem);`
139			`always @(posedge i_clk)`
140			`if (i_tap_wr)`
141			`cmem[r_tapwidx] <= i_tap;`
142
143			`assign tapwidx = r_tapwidx;`
144			`end endgenerate`
145
146
147			`reg [LGNFFT-1:0] dwidx, didx;`
148			`reg [LGNFFT-1:0] tidx;`
149			`reg top_of_block, first_block;`
150			`reg [1:0] frame_count;`
151			`reg p_ce, d_ce;`
152			`reg signed [IW-1:0] data;`
153			`reg signed [TW-1:0] tap;`
154
155
156
157			`//`
158			`//`
159			`// Record the incoming data into a local memory`
160			`//`
161			`//`
162
163			`// Notice how this data writing section is independent of the reset,`
164			`// depending only upon new sample data.`
165
166			`initial dwidx = 0;`
167			`always @(posedge i_clk)`
168			`if (i_reset)`
169			`dwidx <= 0;`
170			`else if (i_ce)`
171			`dwidx <= dwidx + 1'b1;`
172			`always @(posedge i_clk)`
173			`if (i_ce)`
174			`dmem[dwidx] <= i_sample;`
175
176			`initial first_block = 1'b1;`
177			`always @(posedge i_clk)`
178			`if (i_reset)`
179			`first_block <= 1'b1;`
180			`else if ((i_alt_ce)&&(&tidx)&&(dwidx==0))`
181			`first_block <= 1'b0;`
182
183
184			`//`
185			`//`
186			`// Keep track of the top of the block. The top of the block is the`
187			`// first incoming data sample on an FFT or half FFT boundary. This`
188			`// is where data processing starts from.`
189			`//`
190			`initial top_of_block = 1'b0;`
191			`always @(posedge i_clk)`
192			`if (i_reset)`
193			`top_of_block <= 1'b0;`
194			`else if (i_alt_ce)`
195			`top_of_block <= (&tidx)&&((!first_block)\|\|(dwidx==0));`
196			`else if (i_ce)`
197			`top_of_block <= 1'b0;`
198
199			`//`
200			`// Data and coefficient memory indices.`
201			`//`
202			`initial didx = 0;`
203			`always @(posedge i_clk)`
204			`if (i_reset)`
205			`didx <= 0;`
206			`else if ((i_alt_ce)&&(dwidx[LGNFFT-2:0]==0))`
207			`begin`
208			`didx[LGNFFT-2:0] <= 0;`
209			`didx[LGNFFT-1] <= dwidx[LGNFFT-1];`
210			`end else if ((i_ce)\|\|(i_alt_ce))`
211			`// Process the next point in this FFT`
212			`didx <= didx + 1'b1;`
213
214			`initial tidx = 0;`
215			`always @(posedge i_clk)`
216			`if (i_reset)`
217			`tidx <= 0;`
218			`else if ((i_alt_ce)&&(dwidx[LGNFFT-2:0]==0))`
219			`begin`
220			`// // At the beginning of processing for a given FFT`
221			`tidx <= 0;`
222			`end else if ((i_ce)\|\|(i_alt_ce))`
223			`// Process the next point in the window function`
224			`tidx <= tidx + 1'b1;`
225
226			`initial frame_count = 0;`
227			`always @(posedge i_clk)`
228			`if (i_reset)`
229			`frame_count <= 0;`
230			`else if ((i_ce)&&(top_of_block)&&(!first_block))`
231			`frame_count <= 3;`
232			`else if (frame_count != 0)`
233			`frame_count <= frame_count - 1'b1;`
234
235			`initial o_frame = 1'b0;`
236			`always @(posedge i_clk)`
237			`if (i_reset)`
238			`o_frame <= 1'b0;`
239			`else if (frame_count == 2)`
240			`o_frame <= 1'b1;`
241			`else`
242			`o_frame <= 1'b0;`
243
244			`//`
245			`// Following any initial i_ce, ...`
246			`// d_ce: The data (and coefficient), read from memory,will be valid`
247			`// p_ce: The produc of data and coefficient is valid`
248			`//`
249			`initial { p_ce, d_ce } = 2'h0;`
250			`always @(posedge i_clk)`
251			`if (i_reset)`
252			`{ p_ce, d_ce } <= 2'h0;`
253			`else`
254			`{ p_ce, d_ce } <= { d_ce, (!first_block)&&((i_ce)\|\|(i_alt_ce)) };`
255
256			`// Read the data sample point, and the filter coefficient, from block`
257			`// RAM. Because this is block RAM, we have to be careful not to`
258			`// do anything else here.`
259			`initial data = 0;`
260			`initial tap = 0;`
261			`always @(posedge i_clk)`
262			`begin`
263			`data <= dmem[didx];`
264			`tap <= cmem[tidx];`
265			`end`
266
267			`//`
268			`// Multiply the two values together`
269			`reg signed [IW+TW-1:0] product;`
270			`ifdef FORMAL
271			`// We'll implement an abstract multiply below--just to make sure the`
272			`// timing is right.`
273			`else
274			`always @(posedge i_clk)`
275			`product <= data * tap;`
276			`endif
277
278			`//`
279			`// Output CE`
280			`//`
281			`initial o_ce = 0;`
282			`always @(posedge i_clk)`
283			`if (i_reset)`
284			`o_ce <= 0;`
285			`else`
286			`o_ce <= p_ce;`
287
288			`generate if (OW == AW)`
289			`begin : BIT_ADJUSTMENT_NONE`
290
291			`initial o_sample = 0;`
292			`always @(posedge i_clk)`
293			`if (i_reset)`
294			`o_sample <= 0;`
295			`else if (p_ce)`
296			`o_sample <= product;`
297
298			`end else if (OW < AW)`
299			`begin : BIT_ADJUSTMENT_ROUNDING`
300			`wire [AW-1:0] rounded;`
301
302			`assign rounded = product + { {(OW){1'b0}}, product[AW-OW],`
303			`{(AW-OW-1){!product[AW-OW]}} };`
304
305			`initial o_sample = 0;`
306			`always @(posedge i_clk)`
307			`if (i_reset)`
308			`o_sample <= 0;`
309			`else if (p_ce)`
310			`o_sample <= rounded[(AW-1):(AW-OW)];`
311
312			`// Make Verilator happy`
313			`// verilator lint_off UNUSED`
314			`wire [AW-OW-1:0] unused_rounding_bits;`
315			`assign unused_rounding_bits = rounded[AW-OW-1:0];`
316			`// verilator lint_on UNUSED`
317
318			`end else // if (OW > AW)`
319			`begin : BIT_ADJUSTMENT_EXTENDING`
320
321			`always @(posedge i_clk)`
322			`if (i_reset)`
323			`o_sample <= 0;`
324			`else if (p_ce)`
325			`o_sample <= { product, {(OW-AW){1'b0}} };`
326
327			`end endgenerate`
328
329			`// Make Verilator happy`
330			`// verilator lint_off UNUSED`
331			`wire [LGNFFT-1:0] unused;`
332			`assign unused = tapwidx;`
333			`// verilator lint_on UNUSED`
334
335			`ifdef FORMAL
336			`reg f_past_valid;`
337			`initial f_past_valid = 1'b0;`
338			`always @(posedge i_clk)`
339			`f_past_valid <= 1'b1;`
340
341			`// Keep track of the phase of this operation`
342			`reg [LGNFFT:0] f_phase;`
343
344			`initial f_phase = 0;`
345			`always @(posedge i_clk)`
346			`if (i_reset)`
347			`begin`
348			`f_phase <= 0;`
349			`end else if ((i_ce)&&(top_of_block))`
350			`f_phase[LGNFFT-1:0] <= 1;`
351			`else if ((i_ce)\|\|(i_alt_ce))`
352			`f_phase <= f_phase + 1;`
353
354			`///////`
355			`//`
356			`// Assumptions about the input`
357			`always @(posedge i_clk)`
358			`if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_ce)))`
359			`restrict($stable(i_sample));`
360
361			`always @(*)`
362			`if (tapwidx != 0)`
363			`assume(!i_ce);`
364
365			`always @(posedge i_clk)`
366			`if (f_phase[0])`
367			`assume(!i_ce);`
368
369			`always @(posedge i_clk)`
370			`if (!f_phase[0])`
371			`assume(!i_alt_ce);`
372
373			`always @(*)`
374			`if (i_tap_wr)`
375			`assume((!i_ce)&&(!i_alt_ce));`
376
377			`always @(*)`
378			`assume(!i_tap_wr);`
379
380			`always @(*)`
381			`if ((i_ce)&&(top_of_block))`
382			`begin`
383			`assert(dwidx[LGNFFT-2:0]==0);`
384			`assert(didx[LGNFFT-2:0]==0);`
385			`end else if (dwidx[LGNFFT-2:0]!=0)`
386			`assert(!top_of_block);`
387
388			`always @(*)`
389			`if ((dwidx[LGNFFT-2:0]==0)&&(!didx[0]))`
390			`assert(top_of_block\|\|f_first_block\|\|first_block);`
391			`else`
392			`assert(!top_of_block);`
393
394			`always @(posedge i_clk)`
395			`if ((f_past_valid)&&($past(first_block))&&(!first_block))`
396			`assert(top_of_block);`
397
398			`/*`
399			`always @(posedge i_clk)`
400			`if (f_past_valid)`
401			`begin`
402			`if ($past(i_reset))`
403			`assert(!top_of_block);`
404			`else if ($past(i_ce))`
405			`assert(top_of_block == ((!first_block)&&(dwidx[LGNFFT-2:0]==0)));`
406			`else`
407
408			`assert(top_of_block == ((!first_block)&&(&dwidx[LGNFFT-2:1])));`
409			`end`
410			`*/`
411
412			`always @(posedge i_clk)`
413			`if ((f_past_valid)&&($past(first_block))&&(!$past(first_block)))`
414			`assert(top_of_block);`
415
416			`//////////////////////////////////////////////////////////////////`
417			`//`
418			`// Assertions about our outputs`
419			`//`
420			`/////////////////////////`
421			`//`
422			`//`
423			`// always @(*)`
424			`// if (o_frame)`
425			`// assert(o_ce);`
426			`always @(*)`
427			`if (first_block)`
428			`assert(!o_ce);`
429
430			`reg f_waiting_for_first_frame;`
431
432			`initial f_waiting_for_first_frame = 1;`
433			`always @(posedge i_clk)`
434			`if ((i_reset)\|\|(first_block))`
435			`f_waiting_for_first_frame <= 1'b1;`
436			`else if (o_ce)`
437			`f_waiting_for_first_frame <= 1'b0;`
438
439			`always @(*)`
440			`if ((f_waiting_for_first_frame)&&(o_ce))`
441			`assert(o_frame);`
442			`always @(*)`
443			`if (f_phase == 0)`
444			`assert((top_of_block)\|\|(first_block));`
445
446			`always @(*)`
447			`if (f_waiting_for_first_frame)`
448			`begin`
449			`if (f_phase[LGNFFT-1:0] > 3)`
450			`begin`
451			`assert((first_block)&&(!o_frame));`
452			`assert({o_ce, p_ce, d_ce} == 0);`
453			`assert(frame_count == 0);`
454			`end else if (f_phase == 0)`
455			`begin`
456			`assert((!o_frame)&&({o_ce, p_ce, d_ce} == 0));`
457			`assert(frame_count == 0);`
458			`end else if ((f_phase > 0)&&(!first_block))`
459			`assert(\|{o_ce, p_ce, d_ce });`
460			`else if ((frame_count != 0)\|\|(first_block))`
461			`assert(!o_frame);`
462			`else`
463			`assert(o_frame);`
464			`end`
465
466			`always @(posedge i_clk)`
467			`if ((f_past_valid)&&(!$past(i_reset)))`
468			`assert(o_ce \|\| $stable(o_sample));`
469
470			`/*`
471			`always @(*)`
472			`assert(m_ce == (f_phase == 0));`
473			`always @(*)`
474			`assert(d_ce == (f_phase == 1));`
475			`always @(*)`
476			`assert(p_ce == (f_phase == 2));`
477			`always @(*)`
478			`assert(o_ce == (f_phase == 3));`
479			`always @(*)`
480			`assert(o_frame == (f_phase == 3));`
481			`*/`
482
483			`always @(*)`
484			`assert(didx[LGNFFT-2:0] == tidx[LGNFFT-2:0]);`
485
486			`always @(posedge i_clk)`
487			`if ((f_past_valid)&&(!$past(i_reset))`
488			`&&($past(i_ce))&&($past(top_of_block)))`
489			`assert(tidx == 1);`
490
491
492			`wire [LGNFFT:0] f_phase_plus_one;`
493			`always @(*)`
494			`f_phase_plus_one = f_phase + 1;`
495			`/*`
496			`end else if ($past(i_ce))`
497			`begin`
498			`// 1 0 // 0 0 Top of block 0`
499			`// 2 1 // 1 1 ALT 0`
500			`// 3 1 // 2 1 1`
501			`// 4 2 // 3 2 ALT 1`
502			`// 5 2 // 4 2 2`
503			`// 6 3 // 5 3 ALT 2`
504			`// 7 3 // 6 3 3`
505			`// 0 4 // 7 4 ALT 3`
506			`// 1 // 4 4 Top of block 0`
507			`// 2 // 5 5 0`
508			`// // 6 5 ALT 1`
509			`// // 7 6 1`
510			`// // 0 6 ALT 2`
511			`// // 1 7 2`
512			`// // 2 7 ALT`
513			`// // 3 0`
514			`// // 0 0 ALT Top of block`
515			`// // 1 1`
516			`// // 2 1`
517			`// // 3 2`
518			`// // 4 2`
519			`*/`
520			`always @(*)`
521			`assert(f_phase_plus_one[LGNFFT:1] == dwidx[LGNFFT-1:0]);`
522			`always @(*)`
523			`assert(f_phase[0] == didx[0]);`
524			`always @(*)`
525			`if (f_phase[LGNFFT])`
526			`begin`
527			`assert(f_phase[LGNFFT-1:0] == {!didx[LGNFFT-1],didx[LGNFFT-2:0]});`
528			`assert((dwidx[LGNFFT-1]==1)`
529			`\|\|(dwidx[LGNFFT-2:0]==0));`
530			`end else begin`
531			`assert((dwidx[LGNFFT-1]==0)`
532			`\|\|((dwidx[LGNFFT-1])&&(dwidx[LGNFFT-2:0]==0)&&(&f_phase[LGNFFT-1:0])));`
533			`assert(f_phase[LGNFFT-1:0] == didx[LGNFFT-1:0]);`
534			`end`
535
536			`always @(*)`
537			`assert(f_phase[LGNFFT-1:0] == tidx[LGNFFT-1:0]);`
538			`always @(*)`
539			`assert(f_phase[LGNFFT-2:0] == didx[LGNFFT-2:0]);`
540			`wire [LGNFFT-1:0] f_diff_idx;`
541			`assign f_diff_idx = didx - dwidx;`
542			`always @(*)`
543			`if (!first_block)`
544			`assert(f_diff_idx < { 1'b1, {(LGNFFT-1){1'b0}} });`
545
546
547			`always @(*)`
548			`if (top_of_block)`
549			`assert(!first_block);`
550
551			`reg f_first_block;`
552			`initial f_first_block = 1'b1;`
553			`always @(posedge i_clk)`
554			`if (i_ce)`
555			`f_first_block <= first_block;`
556
557			`always @(*)`
558			`if ((top_of_block)&&(i_ce)&&(!f_first_block))`
559			`assert(didx[LGNFFT-2:0] == dwidx[LGNFFT-2:0]);`
560
561			`always @(*)`
562			`if ((!f_first_block)&&(!first_block)&&(dwidx[LGNFFT-2:0]==0)`
563			`&&(didx[LGNFFT-1:0]==0))`
564			`assert(top_of_block);`
565
566			`////////////////////////////////////////////////////////////////////////////////`
567			`//`
568			`// Abstract Multiply`
569			`//`
570			`////////////////////////////////////////////////////////////////////////////////`
571			`// Gin up a really quick abstract multiply for formal testing`
572			`// only. always @(posedge i_clk)`
573			`(* anyconst *) signed reg [IW+TW-1:0] pre_product;`
574			`always @(posedge i_clk)`
575			`if (data == 0)`
576			`assume(pre_product == 0);`
577			`always @(posedge i_clk)`
578			`if (tap == 0)`
579			`assume(pre_product == 0);`
580			`always @(posedge i_clk)`
581			`if (data == 1)`
582			`assume(pre_product == tap);`
583			`always @(posedge i_clk)`
584			`if (tap == 1)`
585			`assume(pre_product == data);`
586			`always @(posedge i_clk)`
587			`if ((i_ce)\|\|(i_alt_ce))`
588			`product <= pre_product;`
589
590			`////////////////////////////////////////////////////////////////////////////////`
591			`//`
592			`// Arbitrary memory test`
593			`//`
594			`////////////////////////////////////////////////////////////////////////////////`
595			`(* anyconst *) reg [LGNFFT-1:0] f_addr;`
596			`signed reg [TW-1:0] f_tap;`
597			`signed reg [IW-1:0] f_value, f_tap;`
598			`reg f_this_dce, f_this_pce,`
599			`f_this_oce, f_this_tap;`
600
601			`initial assume(f_tap == cmem[f_addr]);`
602			`always @(*)`
603			`assert(f_tap == cmem[f_addr]);`
604			`always @(posedge i_clk)`
605			`if ((i_tap_wr)&&(f_addr == tapwidx))`
606			`f_tap <= i_tap;`
607
608			`initial f_value = 0;`
609			`initial assume(dmem[f_addr] == f_value);`
610			`always @(*)`
611			`assert(f_value == dmem[f_addr]);`
612			`always @(posedge i_clk)`
613			`if ((i_ce)&&(dwidx == f_addr))`
614			`f_value <= i_sample;`
615			`initial { f_this_oce, f_this_pce, f_this_dce } = 3'h0;`
616			`always @(posedge i_clk)`
617			`if ((i_reset)\|\|(i_tap_wr))`
618			`{ f_this_oce, f_this_pce, f_this_dce } <= 3'h0;`
619			`else`
620			`{ f_this_oce, f_this_pce, f_this_dce }`
621			`<= { f_this_pce, f_this_dce,`
622			`(((i_ce)\|\|(i_alt_ce))`
623			`&&(f_past_valid)&&(f_addr == didx)) };`
624			`initial f_this_tap = 0;`
625			`always @(posedge i_clk)`
626			`if (i_reset)`
627			`f_this_tap <= 0;`
628			`else if ((i_ce)\|\|(i_alt_ce))`
629			`f_this_tap <= (f_past_valid)&&(f_addr == tidx);`
630			`else`
631			`f_this_tap <= 0;`
632
633
634			`always @(posedge i_clk)`
635			`if (f_this_tap)`
636			`assert(tap == f_tap);`
637
638			`always @(posedge i_clk)`
639			`if ((f_past_valid)&&(f_this_dce))`
640			`assert(data == $past(f_value));`
641
642			`reg signed [IW-1:0] f_past_data;`
643			`reg signed [TW-1:0] f_past_tap;`
644
645			`always @(posedge i_clk)`
646			`begin`
647			`f_past_data <= data;`
648			`f_past_tap <= tap;`
649			`end`
650
651			`always @(posedge i_clk)`
652			`if ((f_past_valid)&&(f_this_pce))`
653			`begin`
654			`if (f_past_tap == 0)`
655			`assert(product == 0);`
656			`if (f_past_data == 0)`
657			`assert(product == 0);`
658			`if (f_past_tap == 1)`
659			`assert(product=={{(TW){f_past_data[IW-1]}},f_past_data});`
660			`if (f_past_data == 1)`
661			`assert(product=={{{IW}{f_past_tap[TW-1]}},f_past_tap});`
662			`end`
663
664
665			`////////////////////////////////////////////////////////////////////////////////`
666			`//`
667			`// Cover tests`
668			`//`
669			`////////////////////////////////////////////////////////////////////////////////`
670			`reg f_second_frame;`
671			`initial f_second_frame = 1'b0;`
672			`always @(posedge i_clk)`
673			`if ((o_ce)&&(o_frame))`
674			`f_second_frame <= 1'b1;`
675
676			`always @(posedge i_clk)`
677			`cover((o_ce)&&(o_frame)&&(f_second_frame));`
678			`endif
679			`endmodule`