Subversion Repositories dblclockfft

////////////////////////////////////////////////////////////////////////////////
//
// Filename:	laststage.v
//
// Project:	A General Purpose Pipelined FFT Implementation
//
// Purpose:	This is part of an FPGA implementation that will process
//		the final stage of a decimate-in-frequency FFT, running
//	through the data at one sample per clock.
//
//
// 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	laststage(i_clk, i_reset, i_ce, i_sync, i_val, o_val, o_sync);
	parameter	IWIDTH=16,OWIDTH=IWIDTH+1, SHIFT=0;
	input	wire				i_clk, i_reset, i_ce, i_sync;
	input	wire	[(2*IWIDTH-1):0]	i_val;
	output	wire	[(2*OWIDTH-1):0]	o_val;
	output	reg				o_sync;
 
	reg	signed	[(IWIDTH-1):0]	m_r, m_i;
	wire	signed	[(IWIDTH-1):0]	i_r, i_i;
 
	assign	i_r = i_val[(2*IWIDTH-1):(IWIDTH)]; 
	assign	i_i = i_val[(IWIDTH-1):0]; 
 
	// Don't forget that we accumulate a bit by adding two values
	// together. Therefore our intermediate value must have one more
	// bit than the two originals.
	reg	signed	[(IWIDTH):0]	rnd_r, rnd_i, sto_r, sto_i;
	reg				wait_for_sync, stage;
	reg		[1:0]		sync_pipe;
 
	initial	wait_for_sync = 1'b1;
	initial	stage         = 1'b0;
	always @(posedge i_clk)
		if (i_reset)
		begin
			wait_for_sync <= 1'b1;
			stage         <= 1'b0;
		end else if ((i_ce)&&((!wait_for_sync)||(i_sync))&&(!stage))
		begin
			wait_for_sync <= 1'b0;
			//
			stage <= 1'b1;
			//
		end else if (i_ce)
			stage <= 1'b0;
 
	initial	sync_pipe = 0;
	always @(posedge i_clk)
	if (i_reset)
		sync_pipe <= 0;
	else if (i_ce)
		sync_pipe <= { sync_pipe[0], i_sync };
 
	initial	o_sync = 1'b0;
	always @(posedge i_clk)
	if (i_reset)
		o_sync <= 1'b0;
	else if (i_ce)
		o_sync <= sync_pipe[1];
 
	always @(posedge i_clk)
	if (i_ce)
	begin
		if (!stage)
		begin
			// Clock 1
			m_r <= i_r;
			m_i <= i_i;
			// Clock 3
			rnd_r <= sto_r;
			rnd_i <= sto_i;
			//
		end else begin
			// Clock 2
			rnd_r <= m_r + i_r;
			rnd_i <= m_i + i_i;
			//
			sto_r <= m_r - i_r;
			sto_i <= m_i - i_i;
			//
		end
	end
 
	// Now that we have our results, let's round them and report them
	wire	signed	[(OWIDTH-1):0]	o_r, o_i;
 
	convround #(IWIDTH+1,OWIDTH,SHIFT) do_rnd_r(i_clk, i_ce, rnd_r, o_r);
	convround #(IWIDTH+1,OWIDTH,SHIFT) do_rnd_i(i_clk, i_ce, rnd_i, o_i);
 
	assign	o_val  = { o_r, o_i };
 
`ifdef	FORMAL
	reg	f_past_valid;
	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid <= 1'b1;
 
`ifdef	LASTSTAGE
	always @(posedge i_clk)
		assume((i_ce)||($past(i_ce))||($past(i_ce,2)));
`endif
 
	initial	assert(IWIDTH+1 == OWIDTH);
 
	reg	signed	[IWIDTH-1:0]	f_piped_real	[0:3];
	reg	signed	[IWIDTH-1:0]	f_piped_imag	[0:3];
	always @(posedge i_clk)
	if (i_ce)
	begin
		f_piped_real[0] <= i_val[2*IWIDTH-1:IWIDTH];
		f_piped_imag[0] <= i_val[  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];
	end
 
	wire	f_syncd;
	reg	f_rsyncd;
 
	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	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 @(*)
		assert(stage == f_state[0]);
 
	always @(posedge i_clk)
	if ((f_state == 1'b1)&&(f_syncd))
	begin
		assert(o_r == f_piped_real[2] + f_piped_real[1]);
		assert(o_i == f_piped_imag[2] + f_piped_imag[1]);
	end
 
	always @(posedge i_clk)
	if ((f_state == 1'b0)&&(f_syncd))
	begin
		assert(!o_sync);
		assert(o_r == f_piped_real[3] - f_piped_real[2]);
		assert(o_i == f_piped_imag[3] - f_piped_imag[2]);
	end
 
	always @(*)
	if (wait_for_sync)
	begin
		assert(!f_rsyncd);
		assert(!o_sync);
		assert(f_state == 0);
	end
 
`endif // FORMAL
endmodule