Subversion Repositories zipcpu

////////////////////////////////////////////////////////////////////////////////
//
// Filename:	wbwatchdog.v
//
// Project:	Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose:	A Zip timer, redesigned to be a bus watchdog
//
//	This is basically a timer, but there are some unique features to it.
//
//	1. There is no way to "write" the timeout to this watchdog.  It is
//		fixed with an input (that is assumed to be constant)
//	2. The counter returns to i_timer and the interrupt is cleared on any
//		reset.
//	3. Between resets, the counter counts down to zero.  Once (and if) it
//		hits zero, it will remain at zero until reset.
//	4. Any time the counter is at zero, and until the reset that resets
//		the counter, the output interrupt will be set.
//
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of  the GNU General Public License as published
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
//
// This program 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 General Public License
// for more details.
//
// You should have received a copy of the GNU 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:	GPL, v3, as defined and found on www.gnu.org,
//		http://www.gnu.org/licenses/gpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype	none
//
module	wbwatchdog(i_clk, i_reset, i_timeout, o_int);
	parameter	BW = 32;
	input	wire		i_clk, i_reset;
	// Inputs (these were at one time wishbone controlled ...)
	input	wire [(BW-1):0]	i_timeout;
	// Interrupt line
	output	reg		o_int;
 
	reg	[(BW-1):0]	r_value;
	initial	r_value = {(BW){1'b1}};
	always @(posedge i_clk)
		if (i_reset)
			r_value <= i_timeout[(BW-1):0];
		else if (!o_int)
			r_value <= r_value + {(BW){1'b1}}; // r_value - 1;
 
	// Set the interrupt on our last tick.
	initial	o_int   = 1'b0;
	always @(posedge i_clk)
		if (i_reset)
			o_int <= 1'b0;
		else if (!o_int)
			o_int <= (r_value == { {(BW-1){1'b0}}, 1'b1 });
 
`ifdef	FORMAL
	reg	f_past_valid;
 
	initial	f_past_valid = 1'b0;
	always @(posedge f_past_valid)
		f_past_valid <= 1'b1;
 
	///////////////////////////////////////////////
	//
	//
	// Assumptions about our inputs
	//
	//
	///////////////////////////////////////////////
	always @(*)
		assume(i_timeout > 1);
	always @(posedge i_clk)
	if (f_past_valid)
		assume(i_timeout == $past(i_timeout));
 
	//
	//
	///////////////////////////////////////////////
	//
	//
	// Assertions about our internal state and our outputs
	//
	//
	///////////////////////////////////////////////
	//
	//
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(o_int))&&(!$past(i_reset)))
		assert(o_int);
 
	always @(*)
		assert(o_int == (r_value == 0));
 
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_reset))&&(!$past(o_int)))
	begin
		assert(r_value == $past(r_value)-1'b1);
	end
 
	always @(posedge i_clk)
	if ((!f_past_valid)||($past(i_reset)))
	begin
		if (!f_past_valid)
			assert(r_value == {(BW){1'b1}});
		else // if ($past(i_reset))
			assert(r_value == $past(i_timeout));
		assert(!o_int);
	end
`endif
endmodule