Subversion Repositories dblclockfft

////////////////////////////////////////////////////////////////////////////////
//
// Filename:	bitreverse.v
//
// Project:	A General Purpose Pipelined FFT Implementation
//
// Purpose:	This module bitreverses a pipelined FFT input.  It differes
//		from the dblreverse module in that this is just a simple and
//	straightforward bitreverse, rather than one written to handle two
//	words at once.
//
//
// 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	bitreverse(i_clk, i_reset, i_ce, i_in, o_out, o_sync);
	parameter			LGSIZE=5, WIDTH=24;
	input	wire			i_clk, i_reset, i_ce;
	input	wire	[(2*WIDTH-1):0]	i_in;
	output	reg	[(2*WIDTH-1):0]	o_out;
	output	reg			o_sync;
	reg	[(LGSIZE):0]	wraddr;
	wire	[(LGSIZE):0]	rdaddr;
 
	reg	[(2*WIDTH-1):0]	brmem	[0:((1<<(LGSIZE+1))-1)];
 
	genvar	k;
	generate for(k=0; k<LGSIZE; k=k+1)
		assign rdaddr[k] = wraddr[LGSIZE-1-k];
	endgenerate
	assign	rdaddr[LGSIZE] = !wraddr[LGSIZE];
 
	reg	in_reset;
 
	initial	in_reset = 1'b1;
	always @(posedge i_clk)
		if (i_reset)
			in_reset <= 1'b1;
		else if ((i_ce)&&(&wraddr[(LGSIZE-1):0]))
			in_reset <= 1'b0;
 
	initial	wraddr = 0;
	always @(posedge i_clk)
		if (i_reset)
			wraddr <= 0;
		else if (i_ce)
		begin
			brmem[wraddr] <= i_in;
			wraddr <= wraddr + 1;
		end
 
	always @(posedge i_clk)
		if (i_ce) // If (i_reset) we just output junk ... not a problem
			o_out <= brmem[rdaddr]; // w/o a sync pulse
 
	initial	o_sync = 1'b0;
	always @(posedge i_clk)
		if (i_reset)
			o_sync <= 1'b0;
		else if ((i_ce)&&(!in_reset))
			o_sync <= (wraddr[(LGSIZE-1):0] == 0);
 
`ifdef	FORMAL
`define	ASSERT	assert
`ifdef	BITREVERSE
`define	ASSUME	assume
`else
`define	ASSUME	assert
`endif
 
	reg	f_past_valid;
	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid <= 1'b1;
 
	initial	`ASSUME(i_reset);
	always @(posedge i_clk)
	if ((!f_past_valid)||($past(i_reset)))
	begin
		`ASSERT(wraddr == 0);
		`ASSERT(in_reset);
		`ASSERT(!o_sync);
	end
`ifdef	BITREVERSE
	always @(posedge i_clk)
		assume((i_ce)||($past(i_ce))||($past(i_ce,2)));
`endif // BITREVERSE
 
		(* anyconst *) reg	[LGSIZE:0]	f_const_addr;
		wire	[LGSIZE:0]	f_reversed_addr;
		reg			f_addr_loaded;
		reg	[(2*WIDTH-1):0]	f_addr_value;
 
		generate for(k=0; k<LGSIZE; k=k+1)
			assign	f_reversed_addr[k] = f_const_addr[LGSIZE-1-k];
		endgenerate
		assign	f_reversed_addr[LGSIZE] = f_const_addr[LGSIZE];
 
		initial	f_addr_loaded = 1'b0;
		always @(posedge i_clk)
		if (i_reset)
			f_addr_loaded <= 1'b0;
		else if (i_ce)
		begin
			if (wraddr == f_const_addr)
				f_addr_loaded <= 1'b1;
			else if (rdaddr == f_const_addr)
				f_addr_loaded <= 1'b0;
		end
 
		always @(posedge i_clk)
		if ((i_ce)&&(wraddr == f_const_addr))
		begin
			f_addr_value <= i_in;
			`ASSERT(!f_addr_loaded);
		end
 
		always @(posedge i_clk)
		if ((f_past_valid)&&(!$past(i_reset))
				&&($past(f_addr_loaded))&&(!f_addr_loaded))
			assert(o_out == f_addr_value);
 
		always @(*)
		if (o_sync)
			assert(wraddr[LGSIZE-1:0] == 1);
 
		always @(*)
		if ((wraddr[LGSIZE]==f_const_addr[LGSIZE])
				&&(wraddr[LGSIZE-1:0]
						<= f_const_addr[LGSIZE-1:0]))
			`ASSERT(!f_addr_loaded);
 
		always @(*)
		if ((rdaddr[LGSIZE]==f_const_addr[LGSIZE])&&(f_addr_loaded))
			`ASSERT(wraddr[LGSIZE-1:0]
					<= f_reversed_addr[LGSIZE-1:0]+1);
 
		always @(*)
		if (f_addr_loaded)
			`ASSERT(brmem[f_const_addr] == f_addr_value);
 
 
 
`endif	// FORMAL
endmodule