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

 ////////////////////////////////////////////////////////////////////////////////
 //
 // Filename: 	boxcar.v
 //
 // Project:	DSP Filtering Example Project
 //
 // Purpose:	This filter expands upon the capabilities of the simplest.v
 //		non-trivial filter.  Like simplest.v, this filter only averages
 //	samples together.  Unlike the simplest.v filter, this filter will
 //	average more than two samples together.  Indeed, the number of samples
 //	that can be averaged together is programmable from 1 to
 //	(1<<LGMEM)-1.  To change the number of averages, raise the reset signal,
 //	i_reset, and set i_navg while i_reset is set.  Upon clearing i_reset,
 //	the right number of taps will be set.
 //
 // Algorithm:
 //
 //	y[n] = SUM_{k=0}^{navg-1} x[n-k]
 //		= y[n-1] + x[n] - x[n-navg]
 //
 //	We'll use block RAM to hold the x[n-navg] value.
 //
 // Pipeline scheduling: The following variables are set on the given pipeline
 // 		stages:
 //
 //	(PRE)	navg (set on reset)
 //
 //	0	rdaddr
 //	1	mem[rdaddr]
 //	2	memval
 //		ival
 //		full
 //		wraddr
 //	3	sub
 //		mem[wraddr]
 //	4	acc
 //	5	rounded, and thence o_result
 //
 // The overall delay of this algorithm is four samples.  One to clock in
 // the input, and three more to get to where the input has an effect.
 //
 // 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	boxcar(i_clk, i_reset, i_navg, i_ce, i_sample, o_result);
 	parameter	IW=16,		// Input bit-width
 			LGMEM=6,	// Size of the memory.
 			OW=(IW+LGMEM);	// Output bit-width
 	parameter [0:0]	FIXED_NAVG=1'b0; // True if number of averages is fixed
 	parameter [0:0]	OPT_SIGNED=1'b1; // True for averaging signed numbers
 	// Always assume we'll be averaging by the maximum amount, unless told
 	// otherwise.  Minus one, in two's complement, will become this number
 	// when interpreted as an unsigned number.
 	parameter	[(LGMEM-1):0]	INITIAL_NAVG= -1; // Initial avglen
 	input	wire			i_clk,	// Data clock
 					i_reset;// Positive synchronous reset
 	input	wire	[(LGMEM-1):0]	i_navg;	// Requested number of averages
 	//
 	input	wire			i_ce;	// True if i_sample is valid
 	input	wire	[(IW-1):0]	i_sample;// Input value to be filtered
 	output	reg	[(OW-1):0]	o_result;// Output filter value

 	reg			full;
 	reg	[(LGMEM-1):0]	rdaddr, wraddr;
 	reg	[(IW-1):0]	mem [0:((1<<LGMEM)-1)];
 	reg	[(IW-1):0]	preval, memval;
 	reg	[IW:0]	sub;
 	reg	[(IW+LGMEM-1):0] acc;

 	// The write address.  We'll write into our memory using this address.
 	// It starts at zero, and increments on every valid sample.
 	initial	wraddr = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		wraddr <= 0;
 	else if (i_ce)
 		wraddr <= wraddr + 1'b1;

 	// Calculate the requested number of averages.  If this value is
 	// fixed, these will be INITIAL_NAVG and the input i_navg will be
 	// ignored, else the requested number will be the number given on
 	// the input.
 	wire	[(LGMEM-1):0]	w_requested_navg;
 	assign w_requested_navg = (FIXED_NAVG) ? INITIAL_NAVG : i_navg;

 	// The read address.  We'll keep a running sum of values, and then need
 	// to subtract the value dropping off of the end of the summation.
 	// We'll get this value from memory, using our read address to get
 	// there.
 	//
 	// One trick in this code is that we don't want to waste the logic to
 	// to initialize memory.  For this reason, we'll declare all memory
 	// values to be zero on reset, and only start using the memory once
 	// all values have been set.
 	initial	rdaddr = -INITIAL_NAVG;
 	always @(posedge i_clk)
 	if (i_reset)
 		rdaddr <= -w_requested_navg;
 	else if (i_ce)
 		// rdaddr <= wraddr - navg + 1'b1;
 		rdaddr <= rdaddr + 1'b1;

 	//
 	// Clock stage one
 	//
 	//
 	// "preval" just moves things down one stage in time, to give us
 	// a clock to read from our memory
 	initial	preval = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		preval <= 0;
 	else if (i_ce)
 		preval <= i_sample;

 	always @(posedge i_clk)
 	if (i_ce)
 		mem[wraddr] <= i_sample;

 	initial	memval = 0;
 	always @(posedge i_clk)
 	if (i_ce)
 		memval <= mem[rdaddr];

 	initial	full   = 1'b0;
 	always @(posedge i_clk)
 	if (i_reset)
 		full <= 0;
 	else if (i_ce)
 		full <= (full)||(rdaddr==0);

 	// Clock stage two
 	//
 	// This stage uses the results of stage one.  Note the sign extension
 	// below.  (One of my simulators required me to do that ...)
 	//
 	initial	sub = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		sub <= 0;
 	else if (i_ce)
 	begin
 		if (full)
 			sub <= { OPT_SIGNED&preval[(IW-1)], preval }
 					- { OPT_SIGNED&memval[(IW-1)], memval };
 		else
 			sub <= { OPT_SIGNED&preval[(IW-1)], preval };
 	end

 	// Clock stage three
 	//
 	// Using the difference from stage two, calculate the overall block
 	// average summation.
 	initial	acc = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		acc <= 0;
 	else if (i_ce)
 		acc <= acc + { {(LGMEM-1){OPT_SIGNED&sub[IW]}}, sub };

 	//
 	// Clock stage four
 	//
 	//
 	// Round the result from IW+LGMEM bits down to OW bits.  Also, deal
 	// with all the various cases of relationships between IW+LGLEN and OW
 	wire	[(IW+LGMEM-1):0]	rounded;
 	generate
 	// if (IW+LGMEM < OW)
 		// CANNOT BE: rounded is only IW+LGLEN bits long
 		// Besides, artificially increasing the number of bits doesn't
 		// really make sense
 	if (IW+LGMEM == OW)
 		// No rounding required, output is the acc(umulator)
 		assign	rounded = acc;
 	else if (IW+LGMEM == OW + 1)
 		// Need to drop one bit, round towards even
 		assign	rounded = acc + { {(OW){1'b0}}, acc[1] };
 	else // if (IW+LGMEM > OW)
 		// Drop more than one bit, rounding towards even
 		assign	rounded = acc + {
 				{(OW){1'b0}},
 				acc[(IW+LGMEM-OW)],
 				{(IW+LGMEM-OW-1){!acc[(IW+LGMEM-OW)]}}
 				};
 	endgenerate

 	// (Still stage four)
 	// rounded is set with combinatorial logic.  It's also set to
 	// IW+LGMEM bits.  So, let's take a clock and drop from IW+LGMEM bits
 	// to however many bits have been requested of us.
 	initial	o_result = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		o_result <= 0;
 	else if (i_ce)
 		o_result <= rounded[(IW+LGMEM-1):(IW+LGMEM-OW)];

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

 	reg	[(LGMEM-1):0]	f_navg;

 	always @(*)
 	if ((!FIXED_NAVG)&&(!f_past_valid))
 		assume(i_reset);

 	always @(posedge i_clk)
 	if ((f_past_valid)&&(!$past(i_ce)))
 		assume(i_ce);

 	always @(*)
 	if ((!FIXED_NAVG)&&(i_reset))
 		assume(i_navg > 3);

 	always @(posedge i_clk)
 	if ((f_test[3])&&(f_navg < (1<<LGMEM)-3))
 		assert(f_sum == acc);

 	always @(*)
 		assert(f_navg > 3);

 	always @(posedge i_clk)
 		cover($rose(full));

 	initial	f_navg = INITIAL_NAVG;
 	always @(posedge i_clk)
 	if (FIXED_NAVG)
 		f_navg <= INITIAL_NAVG;
 	else if (i_reset)
 		f_navg <= i_navg;


 	wire	[LGMEM-1:0]	f_rdaddr;
 	assign	f_rdaddr = wraddr - f_navg;
 	always @(posedge i_clk)
 	if (!i_reset)
 		assert(f_rdaddr == rdaddr);

 	integer	k;
 	reg	[LGMEM+IW-1:0]	f_sum;
 	always @(*)
 	begin
 		f_sum = 0;
 		for(k=0; k<(1<<LGMEM); k=k+1)
 		begin
 			if (((full)&&(k<f_navg)) || ((!full)&&(wraddr>=3)&&(k < wraddr-2)))
 				f_sum = f_sum
 				+ {{(LGMEM){OPT_SIGNED&mem[wraddr-k-3][IW-1]}},
 				    mem[wraddr-k-3] };
 		end
 	end

 	wire	[LGMEM-1:0]	f_full_addr;
 	assign	f_full_addr = - f_navg;

 	always @(*)
 	if ((rdaddr < f_full_addr)&&(rdaddr != 0))
 		assert(full);

 	reg	[3:0]	f_test;
 	initial	f_test = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		f_test <= 0;
 	else if ((full)&&(i_ce))
 		f_test <= { f_test[2:0], 1'b1 };

 	always @(posedge i_clk)
 	if ((f_test[3])&&(f_navg < (1<<LGMEM)-4))
 		assert(f_sum == acc);
 	else if ((wraddr > 1)&&(!full))
 		assert(f_sum == acc);
 `endif
 endmodule
	////////////////////////////////////////////////////////////////////////////////
	//
	// Filename: boxcar.v
	//
	// Project: DSP Filtering Example Project
	//
	// Purpose: This filter expands upon the capabilities of the simplest.v
	// non-trivial filter. Like simplest.v, this filter only averages
	// samples together. Unlike the simplest.v filter, this filter will
	// average more than two samples together. Indeed, the number of samples
	// that can be averaged together is programmable from 1 to
	// (1<<LGMEM)-1. To change the number of averages, raise the reset signal,
	// i_reset, and set i_navg while i_reset is set. Upon clearing i_reset,
	// the right number of taps will be set.
	//
	// Algorithm:
	//
	// y[n] = SUM_{k=0}^{navg-1} x[n-k]
	// = y[n-1] + x[n] - x[n-navg]
	//
	// We'll use block RAM to hold the x[n-navg] value.
	//
	// Pipeline scheduling: The following variables are set on the given pipeline
	// stages:
	//
	// (PRE) navg (set on reset)
	//
	// 0 rdaddr
	// 1 mem[rdaddr]
	// 2 memval
	// ival
	// full
	// wraddr
	// 3 sub
	// mem[wraddr]
	// 4 acc
	// 5 rounded, and thence o_result
	//
	// The overall delay of this algorithm is four samples. One to clock in
	// the input, and three more to get to where the input has an effect.
	//
	// 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 boxcar(i_clk, i_reset, i_navg, i_ce, i_sample, o_result);
	parameter IW=16, // Input bit-width
	LGMEM=6, // Size of the memory.
	OW=(IW+LGMEM); // Output bit-width
	parameter [0:0] FIXED_NAVG=1'b0; // True if number of averages is fixed
	parameter [0:0] OPT_SIGNED=1'b1; // True for averaging signed numbers
	// Always assume we'll be averaging by the maximum amount, unless told
	// otherwise. Minus one, in two's complement, will become this number
	// when interpreted as an unsigned number.
	parameter [(LGMEM-1):0] INITIAL_NAVG= -1; // Initial avglen
	input wire i_clk, // Data clock
	i_reset;// Positive synchronous reset
	input wire [(LGMEM-1):0] i_navg; // Requested number of averages
	//
	input wire i_ce; // True if i_sample is valid
	input wire [(IW-1):0] i_sample;// Input value to be filtered
	output reg [(OW-1):0] o_result;// Output filter value

	reg full;
	reg [(LGMEM-1):0] rdaddr, wraddr;
	reg [(IW-1):0] mem [0:((1<<LGMEM)-1)];
	reg [(IW-1):0] preval, memval;
	reg [IW:0] sub;
	reg [(IW+LGMEM-1):0] acc;

	// The write address. We'll write into our memory using this address.
	// It starts at zero, and increments on every valid sample.
	initial wraddr = 0;
	always @(posedge i_clk)
	if (i_reset)
	wraddr <= 0;
	else if (i_ce)
	wraddr <= wraddr + 1'b1;

	// Calculate the requested number of averages. If this value is
	// fixed, these will be INITIAL_NAVG and the input i_navg will be
	// ignored, else the requested number will be the number given on
	// the input.
	wire [(LGMEM-1):0] w_requested_navg;
	assign w_requested_navg = (FIXED_NAVG) ? INITIAL_NAVG : i_navg;

	// The read address. We'll keep a running sum of values, and then need
	// to subtract the value dropping off of the end of the summation.
	// We'll get this value from memory, using our read address to get
	// there.
	//
	// One trick in this code is that we don't want to waste the logic to
	// to initialize memory. For this reason, we'll declare all memory
	// values to be zero on reset, and only start using the memory once
	// all values have been set.
	initial rdaddr = -INITIAL_NAVG;
	always @(posedge i_clk)
	if (i_reset)
	rdaddr <= -w_requested_navg;
	else if (i_ce)
	// rdaddr <= wraddr - navg + 1'b1;
	rdaddr <= rdaddr + 1'b1;

	//
	// Clock stage one
	//
	//
	// "preval" just moves things down one stage in time, to give us
	// a clock to read from our memory
	initial preval = 0;
	always @(posedge i_clk)
	if (i_reset)
	preval <= 0;
	else if (i_ce)
	preval <= i_sample;

	always @(posedge i_clk)
	if (i_ce)
	mem[wraddr] <= i_sample;

	initial memval = 0;
	always @(posedge i_clk)
	if (i_ce)
	memval <= mem[rdaddr];

	initial full = 1'b0;
	always @(posedge i_clk)
	if (i_reset)
	full <= 0;
	else if (i_ce)
	full <= (full)\|\|(rdaddr==0);

	// Clock stage two
	//
	// This stage uses the results of stage one. Note the sign extension
	// below. (One of my simulators required me to do that ...)
	//
	initial sub = 0;
	always @(posedge i_clk)
	if (i_reset)
	sub <= 0;
	else if (i_ce)
	begin
	if (full)
	sub <= { OPT_SIGNED&preval[(IW-1)], preval }
	- { OPT_SIGNED&memval[(IW-1)], memval };
	else
	sub <= { OPT_SIGNED&preval[(IW-1)], preval };
	end

	// Clock stage three
	//
	// Using the difference from stage two, calculate the overall block
	// average summation.
	initial acc = 0;
	always @(posedge i_clk)
	if (i_reset)
	acc <= 0;
	else if (i_ce)
	acc <= acc + { {(LGMEM-1){OPT_SIGNED&sub[IW]}}, sub };

	//
	// Clock stage four
	//
	//
	// Round the result from IW+LGMEM bits down to OW bits. Also, deal
	// with all the various cases of relationships between IW+LGLEN and OW
	wire [(IW+LGMEM-1):0] rounded;
	generate
	// if (IW+LGMEM < OW)
	// CANNOT BE: rounded is only IW+LGLEN bits long
	// Besides, artificially increasing the number of bits doesn't
	// really make sense
	if (IW+LGMEM == OW)
	// No rounding required, output is the acc(umulator)
	assign rounded = acc;
	else if (IW+LGMEM == OW + 1)
	// Need to drop one bit, round towards even
	assign rounded = acc + { {(OW){1'b0}}, acc[1] };
	else // if (IW+LGMEM > OW)
	// Drop more than one bit, rounding towards even
	assign rounded = acc + {
	{(OW){1'b0}},
	acc[(IW+LGMEM-OW)],
	{(IW+LGMEM-OW-1){!acc[(IW+LGMEM-OW)]}}
	};
	endgenerate

	// (Still stage four)
	// rounded is set with combinatorial logic. It's also set to
	// IW+LGMEM bits. So, let's take a clock and drop from IW+LGMEM bits
	// to however many bits have been requested of us.
	initial o_result = 0;
	always @(posedge i_clk)
	if (i_reset)
	o_result <= 0;
	else if (i_ce)
	o_result <= rounded[(IW+LGMEM-1):(IW+LGMEM-OW)];

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

	reg [(LGMEM-1):0] f_navg;

	always @(*)
	if ((!FIXED_NAVG)&&(!f_past_valid))
	assume(i_reset);

	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_ce)))
	assume(i_ce);

	always @(*)
	if ((!FIXED_NAVG)&&(i_reset))
	assume(i_navg > 3);

	always @(posedge i_clk)
	if ((f_test[3])&&(f_navg < (1<<LGMEM)-3))
	assert(f_sum == acc);

	always @(*)
	assert(f_navg > 3);

	always @(posedge i_clk)
	cover($rose(full));

	initial f_navg = INITIAL_NAVG;
	always @(posedge i_clk)
	if (FIXED_NAVG)
	f_navg <= INITIAL_NAVG;
	else if (i_reset)
	f_navg <= i_navg;


	wire [LGMEM-1:0] f_rdaddr;
	assign f_rdaddr = wraddr - f_navg;
	always @(posedge i_clk)
	if (!i_reset)
	assert(f_rdaddr == rdaddr);

	integer k;
	reg [LGMEM+IW-1:0] f_sum;
	always @(*)
	begin
	f_sum = 0;
	for(k=0; k<(1<<LGMEM); k=k+1)
	begin
	if (((full)&&(k<f_navg)) \|\| ((!full)&&(wraddr>=3)&&(k < wraddr-2)))
	f_sum = f_sum
	+ {{(LGMEM){OPT_SIGNED&mem[wraddr-k-3][IW-1]}},
	mem[wraddr-k-3] };
	end
	end

	wire [LGMEM-1:0] f_full_addr;
	assign f_full_addr = - f_navg;

	always @(*)
	if ((rdaddr < f_full_addr)&&(rdaddr != 0))
	assert(full);

	reg [3:0] f_test;
	initial f_test = 0;
	always @(posedge i_clk)
	if (i_reset)
	f_test <= 0;
	else if ((full)&&(i_ce))
	f_test <= { f_test[2:0], 1'b1 };

	always @(posedge i_clk)
	if ((f_test[3])&&(f_navg < (1<<LGMEM)-4))
	assert(f_sum == acc);
	else if ((wraddr > 1)&&(!full))
	assert(f_sum == acc);
	`endif
	endmodule