`default_nettype none

// Direct Memory Access Channel
//
// This DMAC core is currently used to help bring the Kestrel-3 up.
// It started out as just a simple address generator, something
// which fetches a sequence of 32-bit words from the ROM address
// space.  Each word fetched will have bits 7-0 pushed out to a
// diagnostic LED array, allowing a human to manually verify that
// fetching from ROM is working.
//
// Later in its life, it will be amended to write fetched data
// back out to an address (range).  This will facilitate block
// memory moves to I/O peripherals without involving the host
// processor, for example.  It's hoped that both console I/O
// and external mass storage devices will make use of these
// DMACs to facilitate efficient yet high throughput I/O.
//
// Perhaps later still, these channels will evolve some intelligence
// of their own, further off-loading the burden from the host CPU.
// What that intelligence will look like will depend entirely on
// the problems faced at that time, however.


`include "tilelink.vh"


module dmac(
	i_clk,
	i_reset,

	// Data Request.  Asserted by the peripheral behind the DMAC whenever
	// it wants more data to be fed to it.  For diagnostic applications,
	// this signal serves as an 'enable'.  For example, to get one word
	// transferred per second, you'd pulse this signal once per second.
	i_drq,

	// Master Link
	// This link is used to fetch and/or write data from/to memory or I/O.
	//
	//   Channel A
	o_a_opcode,
	o_a_param,
	o_a_size,
	o_a_address,
	o_a_mask,
	o_a_valid,
	i_a_ready,
	//   Channel D
	i_d_opcode,
	i_d_param,
	i_d_size,
	i_d_data,
	i_d_error,
	i_d_valid,
	o_d_ready,

	o_leds
);
	input i_clk;
	input i_reset;

	input i_drq;

	output reg [2:0]	o_a_opcode = `A_OPC_GET;
	output reg [2:0]	o_a_param = 0;
	output reg [1:0]	o_a_size = `A_SIZ_WORD;
	output reg [63:0]	o_a_address = 0;
	output wire [7:0]	o_a_mask;
	output reg		o_a_valid = 0;
	input  			i_a_ready;

	input  [2:0]		i_d_opcode;
	input  [2:0]		i_d_param;
	input  [3:0]		i_d_size;
	input  [63:0]		i_d_data;
	input  			i_d_error;
	input  			i_d_valid;
	output reg		o_d_ready = 0;

	output reg [7:0]	o_leds = 0;


	// a_valid	d_ready
	// 0		0	No current transaction is in progress.
	// 			Ready for another.
	// 0		1	A-channel has had its transaction accepted.
	// 			Still waiting for data on D-channel.
	// 1		0	undefined behavior.
	// 1		1	Both A- and D-channels have yet to be serviced.
	//
	// With this (admittedly unoptimized) state machine of sorts,
	// i_clk/2 transfers per second are allowed, since overlapping
	// transactions are not allowed.  E.g., if i_clk runs at 100MHz,
	// you can get at most 50 MT/s with this engine.
	//
	// When a transfer is in progress, make sure we're ready to receive
	// any response that comes back.  Make sure to negate o_d_ready
	// when we're not looking for more data again.
	//
	// i_drq
	// | o_a_valid
	// | | o_d_ready
	// | | | i_a_ready
	// | | | | i_d_valid
	// | | | | |
	// | | | | |  next_a_valid
	// | | | | |  | next_d_ready
	// | | | | |  | |
	// 0 0 0 0 0  0 0
	// 0 0 0 0 1  0 0
	// 0 0 0 1 0  0 0
	// 0 0 0 1 1  0 0
	// 0 0 1 0 0  0 0
	// 0 0 1 0 1  0 0
	// 0 0 1 1 0  0 1
	// 0 0 1 1 1  0 0
	// 0 1 0 0 0  0 0
	// 0 1 0 0 1  0 0
	// 0 1 0 1 0  0 0
	// 0 1 0 1 1  0 0
	// 0 1 1 0 0  1 1
	// 0 1 1 0 1  1 1
	// 0 1 1 1 0  0 1
	// 0 1 1 1 1  0 0
	// 1 0 0 0 0  1 1
	// 1 0 0 0 1  0 0
	// 1 0 0 1 0  1 1
	// 1 0 0 1 1  0 0
	// 1 0 1 0 0  0 1
	// 1 0 1 0 1  0 0
	// 1 0 1 1 0  0 1
	// 1 0 1 1 1  0 0
	// 1 1 0 0 0  0 0
	// 1 1 0 0 1  0 0
	// 1 1 0 1 0  0 0
	// 1 1 0 1 1  0 0
	// 1 1 1 0 0  1 1
	// 1 1 1 0 1  1 1
	// 1 1 1 1 0  0 1
	// 1 1 1 1 1  0 0

	wire next_a_valid =
		  (i_drq & !o_a_valid & !o_d_ready & !i_d_valid)
		| (o_a_valid & o_d_ready & !i_a_ready);

	wire next_d_ready =
		  (!i_drq & o_d_ready & i_a_ready & !i_d_valid)
		| (!i_drq & o_a_valid & o_d_ready & !i_a_ready)
		| (i_drq & !o_a_valid & !i_d_valid)
		| (i_drq & o_a_valid & o_d_ready & !i_a_ready)
		| (i_drq & o_a_valid & o_d_ready & i_a_ready & !i_d_valid);

	always @(posedge i_clk) begin
		o_a_valid <= next_a_valid;
		o_d_ready <= next_d_ready;

		if (i_reset) begin
			o_a_valid <= 0;
			o_d_ready <= 0;
		end
	end

	// The fetch address must be incremented after each transfer.
	// Make sure the byte enable mask is updated appropriately.

	always @(posedge i_clk) begin
		o_a_address <= o_a_address;

		if (i_reset) begin
			o_a_address <= 0;
		end
		else if (o_d_ready && i_d_valid) begin
			o_a_address <= o_a_address + 4;
		end
	end

	assign o_a_mask = o_a_address[2] ? 8'hF0 : 8'h0F;

	// Set the LEDs to the data we received.
	
	always @(posedge i_clk) begin
		o_leds <= o_leds;

		if (i_reset) begin
			o_leds <= 0;
		end
		else if (o_d_ready && i_d_valid) begin
			if (o_a_address[2]) begin
//				o_leds <= i_d_data[63:56];
//				o_leds <= i_d_data[55:48];
//				o_leds <= i_d_data[47:40];
				o_leds <= i_d_data[39:32];
			end
			else begin
//				o_leds <= i_d_data[31:24];
//				o_leds <= i_d_data[23:16];
//				o_leds <= i_d_data[15:8];
				o_leds <= i_d_data[7:0];
			end
		end
	end

`ifdef FORMAL
	// f_past_valid will be 0 from the start of the simulation to the
	// first rising clock edge.  It'll forever be 1 thereafter.  This
	// allows the simulator to know whether or not certain assumptions
	// about our state holds.
	reg	f_past_valid = 0;
	always @(posedge i_clk) f_past_valid <= 1;

	// Assert initial conditions are actually held for the first time
	// step.  Without this, the formal solver runs the risk of failing
	// immediately.  And it likely will.
	always @(posedge i_clk)
	if((!f_past_valid) || ($past(i_reset))) begin
		assume(!i_drq);
		assert(o_leds == 0);
		assert(o_a_valid == 0);
		assert(o_d_ready == 0);
	end

	always @(posedge i_clk)
	if(!f_past_valid) begin
		assert(o_a_address == 0);
	end

	// No matter what, we should never have a situation where o_a_valid is
	// asserted without at least o_d_ready being asserted as well.  The
	// A-channel is used to send address information out, and D-channel
	// the response to that request.  It's OK for A-channel to clear
	// before (or concurrently with) D-channel, but never vice versa.
	always @(*) assert(!(o_a_valid && !o_d_ready));
`endif

endmodule
