Subversion Repositories dblclockfft

////////////////////////////////////////////////////////////////////////////////
//
// Filename:	qtrstage.v
//
// Project:	A General Purpose Pipelined FFT Implementation
//
// Purpose:	This file encapsulates the 4 point stage of a decimation in
//		frequency FFT.  This particular implementation is optimized
//	so that all of the multiplies are accomplished by additions and
//	multiplexers only.
//
// Operation:
// 	The operation of this stage is identical to the regular stages of
// 	the FFT (see them for details), with one additional and critical
// 	difference: this stage doesn't require any hardware multiplication.
// 	The multiplies within it may all be accomplished using additions and
// 	subtractions.
//
// 	Let's see how this is done.  Given x[n] and x[n+2], cause thats the
// 	stage we are working on, with i_sync true for x[0] being input,
// 	produce the output:
//
// 	y[n  ] = x[n] + x[n+2]
// 	y[n+2] = (x[n] - x[n+2]) * e^{-j2pi n/2}	(forward transform)
// 	       = (x[n] - x[n+2]) * -j^n
//
// 	y[n].r = x[n].r + x[n+2].r	(This is the easy part)
// 	y[n].i = x[n].i + x[n+2].i
//
// 	y[2].r = x[0].r - x[2].r
// 	y[2].i = x[0].i - x[2].i
//
// 	y[3].r =   (x[1].i - x[3].i)		(forward transform)
// 	y[3].i = - (x[1].r - x[3].r)
//
// 	y[3].r = - (x[1].i - x[3].i)		(inverse transform)
// 	y[3].i =   (x[1].r - x[3].r)		(INVERSE = 1)
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-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	qtrstage(i_clk, i_reset, i_ce, i_sync, i_data, o_data, o_sync);
	parameter	IWIDTH=16, OWIDTH=IWIDTH+1;
	parameter	LGWIDTH=8, INVERSE=0,SHIFT=0;
	input	wire				i_clk, i_reset, i_ce, i_sync;
	input	wire	[(2*IWIDTH-1):0]	i_data;
	output	reg	[(2*OWIDTH-1):0]	o_data;
	output	reg				o_sync;
 
	reg		wait_for_sync;
	reg	[2:0]	pipeline;
 
	reg	signed [(IWIDTH):0]	sum_r, sum_i, diff_r, diff_i;
 
	reg	[(2*OWIDTH-1):0]	ob_a;
	wire	[(2*OWIDTH-1):0]	ob_b;
	reg	[(OWIDTH-1):0]		ob_b_r, ob_b_i;
	assign	ob_b = { ob_b_r, ob_b_i };
 
	reg	[(LGWIDTH-1):0]		iaddr;
	reg	[(2*IWIDTH-1):0]	imem	[0:1];
 
	wire	signed	[(IWIDTH-1):0]	imem_r, imem_i;
	assign	imem_r = imem[1][(2*IWIDTH-1):(IWIDTH)];
	assign	imem_i = imem[1][(IWIDTH-1):0];
 
	wire	signed	[(IWIDTH-1):0]	i_data_r, i_data_i;
	assign	i_data_r = i_data[(2*IWIDTH-1):(IWIDTH)];
	assign	i_data_i = i_data[(IWIDTH-1):0];
 
	reg	[(2*OWIDTH-1):0]	omem [0:1];
 
	//
	// Round our output values down to OWIDTH bits
	//
	wire	signed	[(OWIDTH-1):0]	rnd_sum_r, rnd_sum_i,
			rnd_diff_r, rnd_diff_i, n_rnd_diff_r, n_rnd_diff_i;
	convround #(IWIDTH+1,OWIDTH,SHIFT)	do_rnd_sum_r(i_clk, i_ce,
				sum_r, rnd_sum_r);
 
	convround #(IWIDTH+1,OWIDTH,SHIFT)	do_rnd_sum_i(i_clk, i_ce,
				sum_i, rnd_sum_i);
 
	convround #(IWIDTH+1,OWIDTH,SHIFT)	do_rnd_diff_r(i_clk, i_ce,
				diff_r, rnd_diff_r);
 
	convround #(IWIDTH+1,OWIDTH,SHIFT)	do_rnd_diff_i(i_clk, i_ce,
				diff_i, rnd_diff_i);
 
	assign n_rnd_diff_r = - rnd_diff_r;
	assign n_rnd_diff_i = - rnd_diff_i;
	initial wait_for_sync = 1'b1;
	initial iaddr = 0;
	always @(posedge i_clk)
		if (i_reset)
		begin
			wait_for_sync <= 1'b1;
			iaddr <= 0;
		end else if ((i_ce)&&((!wait_for_sync)||(i_sync)))
		begin
			iaddr <= iaddr + 1'b1;
			wait_for_sync <= 1'b0;
		end
 
	always @(posedge i_clk)
		if (i_ce)
		begin
			imem[0] <= i_data;
			imem[1] <= imem[0];
		end
 
 
	// Note that we don't check on wait_for_sync or i_sync here.
	// Why not?  Because iaddr will always be zero until after the
	// first i_ce, so we are safe.
	initial pipeline = 3'h0;
	always	@(posedge i_clk)
		if (i_reset)
			pipeline <= 3'h0;
		else if (i_ce) // is our pipeline process full?  Which stages?
			pipeline <= { pipeline[1:0], iaddr[1] };
 
	// This is the pipeline[-1] stage, pipeline[0] will be set next.
	always	@(posedge i_clk)
		if ((i_ce)&&(iaddr[1]))
		begin
			sum_r  <= imem_r + i_data_r;
			sum_i  <= imem_i + i_data_i;
			diff_r <= imem_r - i_data_r;
			diff_i <= imem_i - i_data_i;
		end
 
	// pipeline[1] takes sum_x and diff_x and produces rnd_x
 
	// Now for pipeline[2].  We can actually do this at all i_ce
	// clock times, since nothing will listen unless pipeline[3]
	// on the next clock.  Thus, we simplify this logic and do
	// it independent of pipeline[2].
	always	@(posedge i_clk)
		if (i_ce)
		begin
			ob_a <= { rnd_sum_r, rnd_sum_i };
			// on Even, W = e^{-j2pi 1/4 0} = 1
			if (!iaddr[0])
			begin
				ob_b_r <= rnd_diff_r;
				ob_b_i <= rnd_diff_i;
			end else if (INVERSE==0) begin
				// on Odd, W = e^{-j2pi 1/4} = -j
				ob_b_r <=   rnd_diff_i;
				ob_b_i <= n_rnd_diff_r;
			end else begin
				// on Odd, W = e^{j2pi 1/4} = j
				ob_b_r <= n_rnd_diff_i;
				ob_b_i <=   rnd_diff_r;
			end
		end
 
	always	@(posedge i_clk)
		if (i_ce)
		begin // In sequence, clock = 3
			omem[0] <= ob_b;
			omem[1] <= omem[0];
			if (pipeline[2])
				o_data <= ob_a;
			else
				o_data <= omem[1];
		end
 
	initial	o_sync = 1'b0;
	always	@(posedge i_clk)
		if (i_reset)
			o_sync <= 1'b0;
		else if (i_ce)
			o_sync <= (iaddr[2:0] == 3'b101);
 
`ifdef	FORMAL
	reg	f_past_valid;
	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid = 1'b1;
 
`ifdef	QTRSTAGE
	always @(posedge i_clk)
		assume((i_ce)||($past(i_ce))||($past(i_ce,2)));
`endif
 
	// The below logic only works if the rounding stage does nothing
	initial	assert(IWIDTH+1 == OWIDTH);
 
	reg	signed [IWIDTH-1:0]	f_piped_real	[0:7];
	reg	signed [IWIDTH-1:0]	f_piped_imag	[0:7];
 
	always @(posedge i_clk)
	if (i_ce)
	begin
		f_piped_real[0] <= i_data[2*IWIDTH-1:IWIDTH];
		f_piped_imag[0] <= i_data[  IWIDTH-1:0];
 
		f_piped_real[1] <= f_piped_real[0];
		f_piped_imag[1] <= f_piped_imag[0];
 
		f_piped_real[2] <= f_piped_real[1];
		f_piped_imag[2] <= f_piped_imag[1];
 
		f_piped_real[3] <= f_piped_real[2];
		f_piped_imag[3] <= f_piped_imag[2];
 
		f_piped_real[4] <= f_piped_real[3];
		f_piped_imag[4] <= f_piped_imag[3];
 
		f_piped_real[5] <= f_piped_real[4];
		f_piped_imag[5] <= f_piped_imag[4];
 
		f_piped_real[6] <= f_piped_real[5];
		f_piped_imag[6] <= f_piped_imag[5];
 
		f_piped_real[7] <= f_piped_real[6];
		f_piped_imag[7] <= f_piped_imag[6];
	end
 
	reg	f_rsyncd;
	wire	f_syncd;
 
	initial	f_rsyncd = 0;
	always @(posedge i_clk)
	if(i_reset)
		f_rsyncd <= 1'b0;
	else if (!f_rsyncd)
		f_rsyncd <= (o_sync);
	assign	f_syncd = (f_rsyncd)||(o_sync);
 
	reg	[1:0]	f_state;
 
 
	initial	f_state = 0;
	always @(posedge i_clk)
	if (i_reset)
		f_state <= 0;
	else if ((i_ce)&&((!wait_for_sync)||(i_sync)))
		f_state <= f_state + 1;
 
	always @(*)
	if (f_state != 0)
		assume(!i_sync);
 
	always @(posedge i_clk)
		assert(f_state[1:0] == iaddr[1:0]);
 
	wire	signed [2*IWIDTH-1:0]	f_i_real, f_i_imag;
	assign			f_i_real = i_data[2*IWIDTH-1:IWIDTH];
	assign			f_i_imag = i_data[  IWIDTH-1:0];
 
	wire	signed [OWIDTH-1:0]	f_o_real, f_o_imag;
	assign			f_o_real = o_data[2*OWIDTH-1:OWIDTH];
	assign			f_o_imag = o_data[  OWIDTH-1:0];
 
	always @(posedge i_clk)
	if (f_state == 2'b11)
	begin
		assume(f_piped_real[0] != 3'sb100);
		assume(f_piped_real[2] != 3'sb100);
		assert(sum_r  == f_piped_real[2] + f_piped_real[0]);
		assert(sum_i  == f_piped_imag[2] + f_piped_imag[0]);
 
		assert(diff_r == f_piped_real[2] - f_piped_real[0]);
		assert(diff_i == f_piped_imag[2] - f_piped_imag[0]);
	end
 
	always @(posedge i_clk)
	if ((f_state == 2'b00)&&((f_syncd)||(iaddr >= 4)))
	begin
		assert(rnd_sum_r  == f_piped_real[3]+f_piped_real[1]);
		assert(rnd_sum_i  == f_piped_imag[3]+f_piped_imag[1]);
		assert(rnd_diff_r == f_piped_real[3]-f_piped_real[1]);
		assert(rnd_diff_i == f_piped_imag[3]-f_piped_imag[1]);
	end
 
	always @(posedge i_clk)
	if ((f_state == 2'b10)&&(f_syncd))
	begin
		// assert(o_sync);
		assert(f_o_real == f_piped_real[5] + f_piped_real[3]);
		assert(f_o_imag == f_piped_imag[5] + f_piped_imag[3]);
	end
 
	always @(posedge i_clk)
	if ((f_state == 2'b11)&&(f_syncd))
	begin
		assert(!o_sync);
		assert(f_o_real == f_piped_real[5] + f_piped_real[3]);
		assert(f_o_imag == f_piped_imag[5] + f_piped_imag[3]);
	end
 
	always @(posedge i_clk)
	if ((f_state == 2'b00)&&(f_syncd))
	begin
		assert(!o_sync);
		assert(f_o_real == f_piped_real[7] - f_piped_real[5]);
		assert(f_o_imag == f_piped_imag[7] - f_piped_imag[5]);
	end
 
	always @(*)
	if ((iaddr[2:0] == 0)&&(!wait_for_sync))
		assume(i_sync);
 
	always @(*)
	if (wait_for_sync)
		assert((iaddr == 0)&&(f_state == 2'b00)&&(!o_sync)&&(!f_rsyncd));
 
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_ce))&&($past(i_sync))&&(!$past(i_reset)))
		assert(!wait_for_sync);
 
	always @(posedge i_clk)
	if ((f_state == 2'b01)&&(f_syncd))
	begin
		assert(!o_sync);
		if (INVERSE)
		begin
			assert(f_o_real == -f_piped_imag[7]+f_piped_imag[5]);
			assert(f_o_imag ==  f_piped_real[7]-f_piped_real[5]);
		end else begin
			assert(f_o_real ==  f_piped_imag[7]-f_piped_imag[5]);
			assert(f_o_imag == -f_piped_real[7]+f_piped_real[5]);
		end
	end
 
`endif
endmodule