Subversion Repositories zipcpu

////////////////////////////////////////////////////////////////////////////////
//
// Filename:	icontrol.v
//
// Project:	Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose:	An interrupt controller, for managing many interrupt sources.
//
//	This interrupt controller started from the question of how best to
//	design a simple interrupt controller.  As such, it has a few nice
//	qualities to it:
//		1. This is wishbone compliant
//		2. It sits on a 32-bit wishbone data bus
//		3. It only consumes one address on that wishbone bus.
//		4. There is no extra delays associated with reading this
//			device.
//		5. Common operations can all be done in one clock.
//
//	So, how shall this be used?  First, the 32-bit word is broken down as
//	follows:
//
//	Bit 31	- This is the global interrupt enable bit.  If set, interrupts
//		will be generated and passed on as they come in.
//	Bits 16-30	- These are specific interrupt enable lines.  If set,
//		interrupts from source (bit#-16) will be enabled.
//		To set this line and enable interrupts from this source, write
//		to the register with this bit set and the global enable set.
//		To disable this line, write to this register with global enable
//		bit not set, but this bit set.  (Writing a zero to any of these
//		bits has no effect, either setting or unsetting them.)
//	Bit 15 - This is the any interrupt pin.  If any interrupt is pending,
//		this bit will be set.
//	Bits 0-14	- These are interrupt bits.  When set, an interrupt is
//		pending from the corresponding source--regardless of whether
//		it was enabled.  (If not enabled, it won't generate an
//		interrupt, but it will still register here.)  To clear any
//		of these bits, write a '1' to the corresponding bit.  Writing
//		a zero to any of these bits has no effect.
//
//	The peripheral also sports a parameter, IUSED, which can be set
//	to any value between 1 and (buswidth/2-1, or) 15 inclusive.  This will
//	be the number of interrupts handled by this routine.  (Without the
//	parameter, Vivado was complaining about unused bits.  With it, we can
//	keep the complaints down and still use the routine).
//
//	To get access to more than 15 interrupts, chain these together, so
//	that one interrupt controller device feeds another.
//
//
// 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	icontrol(i_clk, i_reset, i_wr, i_data, o_data,
		i_brd_ints, o_interrupt);
	parameter	IUSED = 15, BW=32;
	input	wire		i_clk, i_reset;
	input	wire		i_wr;
	input	wire	[BW-1:0]	i_data;
	output	reg	[BW-1:0]	o_data;
	input	wire	[(IUSED-1):0]	i_brd_ints;
	output	wire		o_interrupt;
 
	reg	[(IUSED-1):0]	r_int_state;
	reg	[(IUSED-1):0]	r_int_enable;
	wire	[(IUSED-1):0]	nxt_int_state;
	reg		r_interrupt, r_gie;
	wire		w_any;
 
	assign	nxt_int_state = (r_int_state|i_brd_ints);
	initial	r_int_state = 0;
	always @(posedge i_clk)
		if (i_reset)
			r_int_state  <= 0;
		else if (i_wr)
			r_int_state <= i_brd_ints | (r_int_state & (~i_data[(IUSED-1):0]));
		else
			r_int_state <= nxt_int_state;
	initial	r_int_enable = 0;
	always @(posedge i_clk)
		if (i_reset)
			r_int_enable <= 0;
		else if ((i_wr)&&(i_data[BW-1]))
			r_int_enable <= r_int_enable | i_data[(16+IUSED-1):16];
		else if ((i_wr)&&(!i_data[BW-1]))
			r_int_enable <= r_int_enable & (~ i_data[(16+IUSED-1):16]);
 
	initial	r_gie = 1'b0;
	always @(posedge i_clk)
		if (i_reset)
			r_gie <= 1'b0;
		else if (i_wr)
			r_gie <= i_data[BW-1];
 
	assign	w_any = ((r_int_state & r_int_enable) != 0);
 
	initial	r_interrupt = 1'b0;
	always @(posedge i_clk)
	if (i_reset)
		r_interrupt <= 1'b0;
	else
		r_interrupt <= (r_gie)&&(w_any);
 
	generate
	if (IUSED < 15)
	begin
		always @(posedge i_clk)
			o_data <= {
				r_gie, { {(15-IUSED){1'b0}}, r_int_enable }, 
				w_any, { {(15-IUSED){1'b0}}, r_int_state  } };
	end else begin
		always @(posedge i_clk)
			o_data <= { r_gie, r_int_enable, w_any, r_int_state };
	end endgenerate
 
	assign	o_interrupt = r_interrupt;
 
	// Make verilator happy
	// verilator lint_off UNUSED
	wire	[30:0]	unused;
	assign	unused = i_data[30:0];
	// verilator lint_on  UNUSED
 
`ifdef	FORMAL
`ifdef	ICONTROL
`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 @(*)
	if (!f_past_valid)
		`ASSUME(i_reset);
 
	always @(posedge i_clk)
	if ((!f_past_valid)||($past(i_reset)))
	begin
		assert(w_any == 0);
		assert(r_interrupt == 0);
		assert(r_gie == 0);
		assert(r_int_enable == 0);
	end
 
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_reset)))
		assert((r_int_state & $past(i_brd_ints))==$past(i_brd_ints));
 
	always @(posedge i_clk)
	if (((f_past_valid)&&(!$past(i_reset)))
			&&($past(r_int_state) & $past(r_int_enable))
			&&($past(r_gie)) )
		assert(o_interrupt);
 
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(w_any))&&(!$past(i_wr))&&(!$past(i_reset)))
		assert(w_any);
 
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(r_gie)))
		assert(!o_interrupt);
 
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(w_any)))
		assert(!o_interrupt);
 
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr)))
	begin
		// Interrupts cannot be cleared, unless they are set
		assert(r_int_state == (($past(i_brd_ints))
			|(($past(r_int_state))&(~$past(i_data[IUSED-1:0])))));
		assert(r_gie == $past(i_data[BW-1]));
	end else if ((f_past_valid)&&(!$past(i_reset)))
	begin
		assert(r_int_state == ($past(r_int_state)|$past(i_brd_ints)));
		assert(r_gie == $past(r_gie));
	end
 
`endif
endmodule