SVIncCompil/Testcases/YosysDsp/fastfir.v - third_party/Surelog - Git at Google

 ////////////////////////////////////////////////////////////////////////////////
 //
 // Filename: 	fastfir.v
 //
 // Project:	DSP Filtering Example Project
 //
 // Purpose:	Implement a high speed (1-output per clock), adjustable tap
 //		FIR.  Unlike our previous example in genericfir.v, this example
 //	attempts to optimize the algorithm via the use of a better delay
 //	structure for the input samples.
 //
 // Creator:	Dan Gisselquist, Ph.D.
 //		Gisselquist Technology, LLC
 //
 ////////////////////////////////////////////////////////////////////////////////
 //
 // Copyright (C) 2017-2019, Gisselquist Technology, LLC
 //
 // This file is part of the DSP filtering set of designs.
 //
 // The DSP filtering designs are free RTL designs: you can redistribute them
 // and/or modify any of them 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 DSP filtering designs are distributed in the hope that they 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 these designs.  (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	fastfir(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_result);
 `ifdef	FORMAL
 	parameter		NTAPS=16, IW=9, TW=IW, OW=2*IW+5;
 `else
 	parameter		NTAPS=128, IW=12, TW=IW, OW=2*IW+7;
 `endif
 	parameter [0:0]		FIXED_TAPS=0;
 	input	wire			i_clk, i_reset;
 	//
 	input	wire			i_tap_wr;	// Ignored if FIXED_TAPS
 	input	wire	[(TW-1):0]	i_tap;		// Ignored if FIXED_TAPS
 	//
 	input	wire			i_ce;
 	input	wire	[(IW-1):0]	i_sample;
 	output	wire	[(OW-1):0]	o_result;

 	wire	[(TW-1):0] tap		[NTAPS:0];
 	wire	[(TW-1):0] tapout	[NTAPS:0];
 	wire	[(IW-1):0] sample	[NTAPS:0];
 	wire	[(OW-1):0] result	[NTAPS:0];
 	wire		tap_wr;

 	// The first sample in our sample chain is the sample we are given
 	assign	sample[0]	= i_sample;
 	// Initialize the partial summing accumulator with zero
 	assign	result[0]	= 0;

 	genvar	k;
 	generate
 	if(FIXED_TAPS)
 	begin
 		initial $readmemh("taps.hex", tap);

 		assign	tap_wr = 1'b0;
 	end else begin
 		assign	tap_wr = i_tap_wr;
 		assign	tap[0] = i_tap;
 	end

 	assign	tapout[0] = 0;

 	for(k=0; k<NTAPS; k=k+1)
 	begin: FILTER

 		firtap #(.FIXED_TAPS(FIXED_TAPS),
 				.IW(IW), .OW(OW), .TW(TW),
 				.INITIAL_VALUE(0))
 			tapk(i_clk, i_reset,
 				// Tap update circuitry
 				tap_wr, tap[k], tapout[k+1],
 				// Sample delay line
 				// We'll let the optimizer trim away sample[k+1]
 				i_ce, sample[0], sample[k+1],
 				// The output accumulator
 				result[k], result[k+1]);

 		if (!FIXED_TAPS)
 			assign	tap[k+1] = tapout[k+1];

 		// Make verilator happy
 		// verilator lint_off UNUSED
 		wire	[(TW-1):0]	unused_tap;
 		if (FIXED_TAPS)
 			assign	unused_tap    = tapout[k+1];
 		// verilator lint_on UNUSED
 	end endgenerate

 	assign	o_result = result[NTAPS];

 	// Make verilator happy
 	// verilator lint_off UNUSED
 	wire	[(TW):0]	unused;
 	assign	unused = { i_tap_wr, i_tap };
 	// verilator lint_on UNUSED

 `ifdef	FORMAL
 `define	PHASE_ONE_ASSERT	assert
 `define	PHASE_TWO_ASSERT	assert

 `ifdef	PHASE_TWO
 `undef	PHASE_ONE_ASSERT
 `define	PHASE_ONE_ASSERT	assume
 `endif

 	reg	f_past_valid;
 	initial	f_past_valid = 1'b0;
 	always @(posedge i_clk)
 		f_past_valid <= 1'b1;


 	///////////////////////////
 	//
 	// Assumptions
 	//
 	///////////////////////////

 	always @(posedge i_clk)
 	if ((f_past_valid)&&(!$past(i_ce))
 			//&&($past(f_past_valid))&&(!$past(i_ce,2))
 			)
 		assume(i_ce);
 	// always @(*) if (!i_reset) assume(i_ce);

 	always @(posedge i_clk)
 	if ((!f_past_valid)||(i_reset)||($past(i_reset)))
 		assume(i_sample == 0);

 ////////////////////////////////////////////////////////////////////////////////
 //
 // The Contract
 //
 // 1. Given an impulse, either +/- 2^k, return an impulse response
 // 2. No overflowing
 //
 ////////////////////////////////////////////////////////////////////////////////


 	wire	[IW-1:0]	f_impulse;
 	assign			f_impulse = $anyconst;
 	wire			f_is_impulse, f_sign;
 	wire	[4:0]		f_zeros;

 	integer	m;
 	always @(*)
 	begin
 		f_is_impulse = 1'b0;
 		f_zeros = 5'h0;
 		if (f_impulse == { 1'b1, {(IW-1){1'b0}}})
 		begin
 			f_is_impulse = 1'b1;
 			f_zeros = IW-1;
 		end else if (f_impulse == {(IW){1'b1}})
 		begin
 			f_is_impulse = 1'b1;
 			f_zeros = 0;
 		end else if (f_impulse[IW-1])
 		begin
 			// Signed impulse
 			for(m=0; m<IW-1; m=m+1)
 			begin
 				if (f_impulse == (-1 << m))
 				begin
 					f_is_impulse = 1'b1;
 					f_zeros = m;
 				end
 			end
 		end else begin
 			// Unsigned impulse
 			for(m=0; m<IW-1; m=m+1)
 			begin
 				if (f_impulse == (1 << m))
 				begin
 					f_is_impulse = 1'b1;
 					f_zeros = m;
 				end
 			end
 		end

 		f_sign = f_impulse[IW-1];
 		assume(f_is_impulse);
 	end

 	reg	[9:0]	f_counts_to_clear, f_counts_since_impulse;
 	initial	f_counts_to_clear = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		f_counts_to_clear <= 0;
 	else if (i_tap_wr)
 		f_counts_to_clear <= NTAPS;
 	else if (i_ce)
 	begin
 		if ((i_sample != 0)||(i_tap_wr))
 			f_counts_to_clear <= NTAPS;
 		else // if (i_sample == 0)
 			f_counts_to_clear <= f_counts_to_clear - 1'b1;
 	end

 	always @(*)
 	if (f_counts_to_clear == 0)
 		`PHASE_ONE_ASSERT((f_counts_since_impulse == 0)
 			||(f_counts_since_impulse>NTAPS));

 	initial	f_counts_since_impulse = 0;
 	always @(posedge i_clk)
 	if ((i_reset)||(!f_past_valid)||($past(i_reset))||(i_tap_wr))
 		f_counts_since_impulse <= 0;
 	else if (f_counts_since_impulse > NTAPS)
 		f_counts_since_impulse <= 0;
 	else if (i_ce)
 	begin
 		if ((i_sample != 0)&&(i_sample != f_impulse))
 			f_counts_since_impulse <= 0;
 		else if (i_sample == f_impulse)
 			f_counts_since_impulse <= (f_counts_to_clear == 0);
 		else if (f_counts_since_impulse > 0) // &&(i_sample == 0)
 			f_counts_since_impulse <= f_counts_since_impulse + 1'b1;
 	end


 	///////////////////////////////////////
 	//
 	// Verify no overflow
 	//
 	///////////////////////////////////////
 	always @(*)
 	begin
 		for(m=0; m<NTAPS; m=m+1)
 		begin
 			`PHASE_ONE_ASSERT((result[m][OW-1:OW-2] == 2'b00)
 				||(result[m][OW-1:OW-2] == 2'b11));
 		end
 		`PHASE_ONE_ASSERT((o_result[OW-1:OW-2] == 2'b00)
 			||(o_result[OW-1:OW-2] == 2'b11));
 	end

 	///////////////////////////////////////
 	//
 	// Verify the reset
 	//
 	///////////////////////////////////////
 	always @(posedge i_clk)
 	if ((!f_past_valid)||($past(i_reset)))
 	begin
 		for(m=1; m<NTAPS; m=m+1)
 			`PHASE_ONE_ASSERT(sample[m] == 0);

 		for(m=0; m<NTAPS; m=m+1)
 			`PHASE_ONE_ASSERT(result[m] == 0);

 		`PHASE_ONE_ASSERT(result[NTAPS] == 0);
 	end

 	always @(*)
 	begin
 		for(m=0; m<NTAPS; m=m+1)
 			`PHASE_ONE_ASSERT((f_counts_to_clear > m)||(result[NTAPS-1-m] == 0));
 	end

 	//////////////////////////////////////////////
 	always @(*)
 	if (f_counts_since_impulse > 0)
 		`PHASE_ONE_ASSERT(f_counts_to_clear == NTAPS + 1 - f_counts_since_impulse);


 `ifdef	PHASE_TWO
 	///////////////////////////////////////
 	//
 	// Verify the impulse response
 	//
 	///////////////////////////////////////
 	always @(posedge i_clk)
 	if ((!f_past_valid)||($past(i_reset)))
 		`PHASE_TWO_ASSERT(o_result == 0);
 	else if (!$past(i_ce))
 		`PHASE_TWO_ASSERT($stable(o_result));
 	else if ((f_counts_since_impulse > 1)&&(f_counts_since_impulse <= NTAPS))
 	begin
 		if (f_sign)
 			`PHASE_TWO_ASSERT(o_result == (-tapout[NTAPS-(f_counts_since_impulse-2)]<<f_zeros));
 		else
 			`PHASE_TWO_ASSERT(o_result == ( tapout[NTAPS-(f_counts_since_impulse-2)]<<f_zeros));
 	end


 	wire	[IW+TW-1:0]	widetaps	[0:NTAPS];
 	wire	[IW+TW-1:0]	staps		[0:NTAPS];
 	genvar	gk;

 	generate begin for(gk=0; gk <= NTAPS; gk=gk+1)
 	begin

 		assign	widetaps[gk] = { {(IW){tapout[gk][TW-1]}}, tapout[gk][TW-1:0] };
 		assign	staps[gk] = widetaps[gk] << f_zeros;

 	end end endgenerate

 	//
 	// Insure that our internal variables are properly set between the
 	// impulse and its output
 	//
 	always @(*)
 	begin
 	if ((f_counts_since_impulse >= 2)&&(f_counts_since_impulse < 2+NTAPS))
 	begin
 	for(m=0; m<NTAPS; m=m+1)
 		if ((m >= (f_counts_since_impulse-2))&&(f_sign))
 			`PHASE_TWO_ASSERT(result[m+1]
 				== (-staps[m-(f_counts_since_impulse-2)+1]));
 		else if (m >= (f_counts_since_impulse-2))
 			`PHASE_TWO_ASSERT(result[m+1]
 				== (staps[m-(f_counts_since_impulse-2)+1]));
 		else
 			`PHASE_TWO_ASSERT(result[m+1] == 0);
 	end
 `endif // PHASE_TWO
 	always @(*)
 	if (i_tap_wr)
 		assume(i_reset);
 	always @(posedge i_clk)
 	if ((f_past_valid)&&($past(i_tap_wr)))
 		assume(i_reset);
 `endif // FORMAL
 endmodule
	////////////////////////////////////////////////////////////////////////////////
	//
	// Filename: fastfir.v
	//
	// Project: DSP Filtering Example Project
	//
	// Purpose: Implement a high speed (1-output per clock), adjustable tap
	// FIR. Unlike our previous example in genericfir.v, this example
	// attempts to optimize the algorithm via the use of a better delay
	// structure for the input samples.
	//
	// Creator: Dan Gisselquist, Ph.D.
	// Gisselquist Technology, LLC
	//
	////////////////////////////////////////////////////////////////////////////////
	//
	// Copyright (C) 2017-2019, Gisselquist Technology, LLC
	//
	// This file is part of the DSP filtering set of designs.
	//
	// The DSP filtering designs are free RTL designs: you can redistribute them
	// and/or modify any of them 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 DSP filtering designs are distributed in the hope that they 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 these designs. (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 fastfir(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_result);
	`ifdef FORMAL
	parameter NTAPS=16, IW=9, TW=IW, OW=2*IW+5;
	`else
	parameter NTAPS=128, IW=12, TW=IW, OW=2*IW+7;
	`endif
	parameter [0:0] FIXED_TAPS=0;
	input wire i_clk, i_reset;
	//
	input wire i_tap_wr; // Ignored if FIXED_TAPS
	input wire [(TW-1):0] i_tap; // Ignored if FIXED_TAPS
	//
	input wire i_ce;
	input wire [(IW-1):0] i_sample;
	output wire [(OW-1):0] o_result;

	wire [(TW-1):0] tap [NTAPS:0];
	wire [(TW-1):0] tapout [NTAPS:0];
	wire [(IW-1):0] sample [NTAPS:0];
	wire [(OW-1):0] result [NTAPS:0];
	wire tap_wr;

	// The first sample in our sample chain is the sample we are given
	assign sample[0] = i_sample;
	// Initialize the partial summing accumulator with zero
	assign result[0] = 0;

	genvar k;
	generate
	if(FIXED_TAPS)
	begin
	initial $readmemh("taps.hex", tap);

	assign tap_wr = 1'b0;
	end else begin
	assign tap_wr = i_tap_wr;
	assign tap[0] = i_tap;
	end

	assign tapout[0] = 0;

	for(k=0; k<NTAPS; k=k+1)
	begin: FILTER

	firtap #(.FIXED_TAPS(FIXED_TAPS),
	.IW(IW), .OW(OW), .TW(TW),
	.INITIAL_VALUE(0))
	tapk(i_clk, i_reset,
	// Tap update circuitry
	tap_wr, tap[k], tapout[k+1],
	// Sample delay line
	// We'll let the optimizer trim away sample[k+1]
	i_ce, sample[0], sample[k+1],
	// The output accumulator
	result[k], result[k+1]);

	if (!FIXED_TAPS)
	assign tap[k+1] = tapout[k+1];

	// Make verilator happy
	// verilator lint_off UNUSED
	wire [(TW-1):0] unused_tap;
	if (FIXED_TAPS)
	assign unused_tap = tapout[k+1];
	// verilator lint_on UNUSED
	end endgenerate

	assign o_result = result[NTAPS];

	// Make verilator happy
	// verilator lint_off UNUSED
	wire [(TW):0] unused;
	assign unused = { i_tap_wr, i_tap };
	// verilator lint_on UNUSED

	`ifdef FORMAL
	`define PHASE_ONE_ASSERT assert
	`define PHASE_TWO_ASSERT assert

	`ifdef PHASE_TWO
	`undef PHASE_ONE_ASSERT
	`define PHASE_ONE_ASSERT assume
	`endif

	reg f_past_valid;
	initial f_past_valid = 1'b0;
	always @(posedge i_clk)
	f_past_valid <= 1'b1;


	///////////////////////////
	//
	// Assumptions
	//
	///////////////////////////

	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_ce))
	//&&($past(f_past_valid))&&(!$past(i_ce,2))
	)
	assume(i_ce);
	// always @(*) if (!i_reset) assume(i_ce);

	always @(posedge i_clk)
	if ((!f_past_valid)\|\|(i_reset)\|\|($past(i_reset)))
	assume(i_sample == 0);

	////////////////////////////////////////////////////////////////////////////////
	//
	// The Contract
	//
	// 1. Given an impulse, either +/- 2^k, return an impulse response
	// 2. No overflowing
	//
	////////////////////////////////////////////////////////////////////////////////


	wire [IW-1:0] f_impulse;
	assign f_impulse = $anyconst;
	wire f_is_impulse, f_sign;
	wire [4:0] f_zeros;

	integer m;
	always @(*)
	begin
	f_is_impulse = 1'b0;
	f_zeros = 5'h0;
	if (f_impulse == { 1'b1, {(IW-1){1'b0}}})
	begin
	f_is_impulse = 1'b1;
	f_zeros = IW-1;
	end else if (f_impulse == {(IW){1'b1}})
	begin
	f_is_impulse = 1'b1;
	f_zeros = 0;
	end else if (f_impulse[IW-1])
	begin
	// Signed impulse
	for(m=0; m<IW-1; m=m+1)
	begin
	if (f_impulse == (-1 << m))
	begin
	f_is_impulse = 1'b1;
	f_zeros = m;
	end
	end
	end else begin
	// Unsigned impulse
	for(m=0; m<IW-1; m=m+1)
	begin
	if (f_impulse == (1 << m))
	begin
	f_is_impulse = 1'b1;
	f_zeros = m;
	end
	end
	end

	f_sign = f_impulse[IW-1];
	assume(f_is_impulse);
	end

	reg [9:0] f_counts_to_clear, f_counts_since_impulse;
	initial f_counts_to_clear = 0;
	always @(posedge i_clk)
	if (i_reset)
	f_counts_to_clear <= 0;
	else if (i_tap_wr)
	f_counts_to_clear <= NTAPS;
	else if (i_ce)
	begin
	if ((i_sample != 0)\|\|(i_tap_wr))
	f_counts_to_clear <= NTAPS;
	else // if (i_sample == 0)
	f_counts_to_clear <= f_counts_to_clear - 1'b1;
	end

	always @(*)
	if (f_counts_to_clear == 0)
	`PHASE_ONE_ASSERT((f_counts_since_impulse == 0)
	\|\|(f_counts_since_impulse>NTAPS));

	initial f_counts_since_impulse = 0;
	always @(posedge i_clk)
	if ((i_reset)\|\|(!f_past_valid)\|\|($past(i_reset))\|\|(i_tap_wr))
	f_counts_since_impulse <= 0;
	else if (f_counts_since_impulse > NTAPS)
	f_counts_since_impulse <= 0;
	else if (i_ce)
	begin
	if ((i_sample != 0)&&(i_sample != f_impulse))
	f_counts_since_impulse <= 0;
	else if (i_sample == f_impulse)
	f_counts_since_impulse <= (f_counts_to_clear == 0);
	else if (f_counts_since_impulse > 0) // &&(i_sample == 0)
	f_counts_since_impulse <= f_counts_since_impulse + 1'b1;
	end


	///////////////////////////////////////
	//
	// Verify no overflow
	//
	///////////////////////////////////////
	always @(*)
	begin
	for(m=0; m<NTAPS; m=m+1)
	begin
	`PHASE_ONE_ASSERT((result[m][OW-1:OW-2] == 2'b00)
	\|\|(result[m][OW-1:OW-2] == 2'b11));
	end
	`PHASE_ONE_ASSERT((o_result[OW-1:OW-2] == 2'b00)
	\|\|(o_result[OW-1:OW-2] == 2'b11));
	end

	///////////////////////////////////////
	//
	// Verify the reset
	//
	///////////////////////////////////////
	always @(posedge i_clk)
	if ((!f_past_valid)\|\|($past(i_reset)))
	begin
	for(m=1; m<NTAPS; m=m+1)
	`PHASE_ONE_ASSERT(sample[m] == 0);

	for(m=0; m<NTAPS; m=m+1)
	`PHASE_ONE_ASSERT(result[m] == 0);

	`PHASE_ONE_ASSERT(result[NTAPS] == 0);
	end

	always @(*)
	begin
	for(m=0; m<NTAPS; m=m+1)
	`PHASE_ONE_ASSERT((f_counts_to_clear > m)\|\|(result[NTAPS-1-m] == 0));
	end

	//////////////////////////////////////////////
	always @(*)
	if (f_counts_since_impulse > 0)
	`PHASE_ONE_ASSERT(f_counts_to_clear == NTAPS + 1 - f_counts_since_impulse);


	`ifdef PHASE_TWO
	///////////////////////////////////////
	//
	// Verify the impulse response
	//
	///////////////////////////////////////
	always @(posedge i_clk)
	if ((!f_past_valid)\|\|($past(i_reset)))
	`PHASE_TWO_ASSERT(o_result == 0);
	else if (!$past(i_ce))
	`PHASE_TWO_ASSERT($stable(o_result));
	else if ((f_counts_since_impulse > 1)&&(f_counts_since_impulse <= NTAPS))
	begin
	if (f_sign)
	`PHASE_TWO_ASSERT(o_result == (-tapout[NTAPS-(f_counts_since_impulse-2)]<<f_zeros));
	else
	`PHASE_TWO_ASSERT(o_result == ( tapout[NTAPS-(f_counts_since_impulse-2)]<<f_zeros));
	end


	wire [IW+TW-1:0] widetaps [0:NTAPS];
	wire [IW+TW-1:0] staps [0:NTAPS];
	genvar gk;

	generate begin for(gk=0; gk <= NTAPS; gk=gk+1)
	begin

	assign widetaps[gk] = { {(IW){tapout[gk][TW-1]}}, tapout[gk][TW-1:0] };
	assign staps[gk] = widetaps[gk] << f_zeros;

	end end endgenerate

	//
	// Insure that our internal variables are properly set between the
	// impulse and its output
	//
	always @(*)
	begin
	if ((f_counts_since_impulse >= 2)&&(f_counts_since_impulse < 2+NTAPS))
	begin
	for(m=0; m<NTAPS; m=m+1)
	if ((m >= (f_counts_since_impulse-2))&&(f_sign))
	`PHASE_TWO_ASSERT(result[m+1]
	== (-staps[m-(f_counts_since_impulse-2)+1]));
	else if (m >= (f_counts_since_impulse-2))
	`PHASE_TWO_ASSERT(result[m+1]
	== (staps[m-(f_counts_since_impulse-2)+1]));
	else
	`PHASE_TWO_ASSERT(result[m+1] == 0);
	end
	`endif // PHASE_TWO
	always @(*)
	if (i_tap_wr)
	assume(i_reset);
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_tap_wr)))
	assume(i_reset);
	`endif // FORMAL
	endmodule