////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	aximrd2wbsp.v
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	Bridge an AXI read channel pair to a single wishbone read
//		channel.
//
// Rules:
// 	1. Any read channel error *must* be returned to the correct
//		read channel ID.  In other words, we can't pipeline between IDs
//	2. A FIFO must be used on getting a WB return, to make certain that
//		the AXI return channel is able to stall with no loss
//	3. No request can be accepted unless there is room in the return
//		channel for it
//
// Status:	Passes a formal bounded model check at 15 steps.  Should be
//		ready for a hardware check.
//
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2019-2020, Gisselquist Technology, LLC
//
// This file is part of the WB2AXIP project.
//
// The WB2AXIP project contains free software and gateware, licensed under the
// Apache License, Version 2.0 (the "License").  You may not use this project,
// or this file, except in compliance with the License.  You may obtain a copy
// of the License at
//
//	http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  See the
// License for the specific language governing permissions and limitations
// under the License.
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype	none
//
module	aximrd2wbsp #(
	parameter C_AXI_ID_WIDTH	= 6, // The AXI id width used for R&W
                                             // This is an int between 1-16
	parameter C_AXI_DATA_WIDTH	= 32,// Width of the AXI R&W data
	parameter C_AXI_ADDR_WIDTH	= 28,	// AXI Address width
	parameter AW			= 26,	// AXI Address width
	parameter LGFIFO                =  3,
	parameter [0:0] OPT_SWAP_ENDIANNESS = 0
	// parameter	WBMODE		= "B4PIPELINE"
		// Could also be "BLOCK"
	) (
	input	wire			S_AXI_ACLK,	// Bus clock
	input	wire			S_AXI_ARESETN,	// Bus reset

// AXI read address channel signals
	input	wire			S_AXI_ARVALID,	// Read address valid
	output	wire			S_AXI_ARREADY,	// Read address ready
	input wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_ARID,	// Read ID
	input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_ARADDR,	// Read address
	input	wire	[7:0]		S_AXI_ARLEN,	// Read Burst Length
	input	wire	[2:0]		S_AXI_ARSIZE,	// Read Burst size
	input	wire	[1:0]		S_AXI_ARBURST,	// Read Burst type
	input	wire	[0:0]		S_AXI_ARLOCK,	// Read lock type
	input	wire	[3:0]		S_AXI_ARCACHE,	// Read Cache type
	input	wire	[2:0]		S_AXI_ARPROT,	// Read Protection type
	input	wire	[3:0]		S_AXI_ARQOS,	// Read Protection type
  
// AXI read data channel signals   
	output	reg			S_AXI_RVALID,  // Read reponse valid
	input	wire			S_AXI_RREADY,  // Read Response ready
	output	wire [C_AXI_ID_WIDTH-1:0] S_AXI_RID,     // Response ID
	output	wire [C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA,    // Read data
	output	wire 			S_AXI_RLAST,    // Read last
	output	reg [1:0]		S_AXI_RRESP,   // Read response

	// We'll share the clock and the reset
	output	reg				o_wb_cyc,
	output	reg				o_wb_stb,
	output	reg [(AW-1):0]			o_wb_addr,
	input	wire				i_wb_stall,
	input	wire				i_wb_ack,
	input	wire [(C_AXI_DATA_WIDTH-1):0]	i_wb_data,
	input	wire				i_wb_err
	);

	localparam	DW = C_AXI_DATA_WIDTH;

	wire	w_reset;
	assign	w_reset = (S_AXI_ARESETN == 1'b0);


	wire	lastid_fifo_full, lastid_fifo_empty,
		resp_fifo_full, resp_fifo_empty;
	wire	[LGFIFO:0]	lastid_fifo_fill, resp_fifo_fill;


	reg				last_stb, last_ack, err_state;
	reg	[C_AXI_ID_WIDTH-1:0]	axi_id;
	reg	[7:0]			stblen;

	wire				skid_arvalid;
	wire	[C_AXI_ID_WIDTH-1:0]	skid_arid;//    r_id;
	wire	[C_AXI_ADDR_WIDTH-1:0]	skid_araddr;//  r_addr;
	wire	[7:0]			skid_arlen;//   r_len;
	wire	[2:0]			skid_arsize;//  r_size;
	wire	[1:0]			skid_arburst;// r_burst;
	reg				fifo_nearfull;
	wire				accept_request;

	reg	[1:0]	axi_burst;
	reg	[2:0]	axi_size;
	reg	[7:0]	axi_len;
	reg	[C_AXI_ADDR_WIDTH-1:0]	axi_addr;
	wire	[C_AXI_ADDR_WIDTH-1:0]	next_addr;
	wire	response_err;
	wire	lastid_fifo_wr;
	reg	midissue, wb_empty;
	reg	[LGFIFO+7:0]	acks_expected;

	skidbuffer #(
		.OPT_OUTREG(0),
		.DW(C_AXI_ID_WIDTH + C_AXI_ADDR_WIDTH + 8 + 3 + 2)
	) axirqbuf(S_AXI_ACLK, !S_AXI_ARESETN,
		S_AXI_ARVALID, S_AXI_ARREADY,
			{ S_AXI_ARID, S_AXI_ARADDR, S_AXI_ARLEN,
			  S_AXI_ARSIZE, S_AXI_ARBURST },
		skid_arvalid, accept_request,
			{ skid_arid, skid_araddr, skid_arlen,
			  skid_arsize, skid_arburst });

	assign	accept_request = (!err_state)
			&&((!o_wb_cyc)||(!i_wb_err))
			// &&(!lastid_fifo_full)
			&&(!midissue
				||(o_wb_stb && last_stb && !i_wb_stall))
			&&(skid_arvalid)
			// One ID at a time, lest we return a bus error
			// to the wrong AXI master
			&&(wb_empty ||(skid_arid == axi_id));


	initial o_wb_cyc        = 0;
	initial o_wb_stb        = 0;
	initial stblen          = 0;
	initial last_stb        = 0;
	always @(posedge S_AXI_ACLK)
	if (w_reset)
	begin
		o_wb_stb <= 1'b0;
		o_wb_cyc <= 1'b0;
	end else if (err_state || (o_wb_cyc && i_wb_err))
	begin
		o_wb_cyc <= 1'b0;
		o_wb_stb <= 1'b0;
	end else if ((!o_wb_stb)||(!i_wb_stall))
	begin
		if (accept_request)
		begin
			// Process the new request
			o_wb_cyc <= 1'b1;
			if (lastid_fifo_full && (!S_AXI_RVALID||!S_AXI_RREADY))
				o_wb_stb <= 1'b0;
			else if (fifo_nearfull && midissue
				&& (!S_AXI_RVALID||!S_AXI_RREADY))
				o_wb_stb <= 1'b0;
			else
				o_wb_stb <= 1'b1;
		end else if (!o_wb_stb && midissue)
		begin
			// Restart a transfer once the FIFO clears
			if (S_AXI_RVALID)
				o_wb_stb <= S_AXI_RREADY;
		// end else if ((o_wb_cyc)&&(i_wb_err)||(err_state))
		end else if (o_wb_stb && !last_stb)
		begin
			if (fifo_nearfull
				&& (!S_AXI_RVALID||!S_AXI_RREADY))
				o_wb_stb <= 1'b0;
		end else if (!o_wb_stb || last_stb)
		begin
			// End the request
			o_wb_stb <= 1'b0;

			// Check for the last acknowledgment
			if ((i_wb_ack)&&(last_ack))
				o_wb_cyc <= 1'b0;
			if (i_wb_err)
				o_wb_cyc <= 1'b0;
		end
	end

	initial	stblen   = 0;
	initial	last_stb = 0;
	initial	midissue = 0;
	always @(posedge S_AXI_ACLK)
	if (w_reset)
	begin
		stblen   <= 0;
		last_stb <= 0;
		midissue <= 0;
	end else if (accept_request)
	begin
		stblen   <= skid_arlen;
		last_stb <= (skid_arlen == 0);
		midissue <= 1'b1;
	end else if (lastid_fifo_wr)
	begin
		if (stblen > 0)
			stblen <= stblen - 1;
		last_stb <= (stblen == 1);
		midissue <= (stblen > 0);
	end

	always @(posedge S_AXI_ACLK)
	if (accept_request)
	begin
		axi_id    <= skid_arid;
		axi_burst <= skid_arburst;
		axi_size  <= skid_arsize;
		axi_len   <= skid_arlen;
	end

	axi_addr #(.AW(C_AXI_ADDR_WIDTH), .DW(C_AXI_DATA_WIDTH))
	next_read_addr(axi_addr, axi_size, axi_burst, axi_len, next_addr);

	always @(posedge S_AXI_ACLK)
	if (accept_request)
		axi_addr <= skid_araddr;
	else if (!i_wb_stall)
		axi_addr <= next_addr;

	always @(*)
		o_wb_addr = axi_addr[(C_AXI_ADDR_WIDTH-1):C_AXI_ADDR_WIDTH-AW];

	assign	lastid_fifo_wr = (o_wb_stb && (i_wb_err || !i_wb_stall))
			||(err_state && midissue && !lastid_fifo_full);

	sfifo #(.BW(C_AXI_ID_WIDTH+1), .LGFLEN(LGFIFO))
	lastid_fifo(S_AXI_ACLK, w_reset,
		lastid_fifo_wr,
		{ axi_id, last_stb },
		lastid_fifo_full, lastid_fifo_fill,
		S_AXI_RVALID && S_AXI_RREADY,
		{ S_AXI_RID, S_AXI_RLAST },
		lastid_fifo_empty);

	reg	[C_AXI_DATA_WIDTH-1:0]	read_data;

	generate if (OPT_SWAP_ENDIANNESS)
	begin : SWAP_ENDIANNESS
		integer	ik;

		// AXI is little endian.  WB can be either.  Most of my WB
		// work is big-endian.
		//
		// This will convert byte ordering between the two
		always @(*)
		for(ik=0; ik<C_AXI_DATA_WIDTH/8; ik=ik+1)
			read_data[ik*8 +: 8]
				= i_wb_data[(C_AXI_DATA_WIDTH-(ik+1)*8) +: 8];

	end else begin : KEEP_ENDIANNESS

		always @(*)
			read_data = i_wb_data;

	end endgenerate

	sfifo #(.BW(C_AXI_DATA_WIDTH+1), .LGFLEN(LGFIFO))
	resp_fifo(S_AXI_ACLK, w_reset,
		o_wb_cyc && (i_wb_ack || i_wb_err), { read_data, i_wb_err },
		resp_fifo_full, resp_fifo_fill,
		S_AXI_RVALID && S_AXI_RREADY,
		{ S_AXI_RDATA, response_err },
		resp_fifo_empty);

	// Count the number of acknowledgements we are still expecting.  This
	// is to support the last_ack calculation in the next process
	initial	acks_expected = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || err_state)
		acks_expected <= 0;
	else case({ accept_request, o_wb_cyc && i_wb_ack })
	2'b01:	acks_expected <= acks_expected -1;
	2'b10:	acks_expected <= acks_expected+({{(LGFIFO){1'b0}},skid_arlen} + 1);
	2'b11:	acks_expected <= acks_expected+{{(LGFIFO){1'b0}},skid_arlen};
	default: begin end
	endcase

	// last_ack should be true if the next acknowledgment will end the bus
	// cycle
	initial	last_ack = 1;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || err_state)
		last_ack <= 1;
	else case({ accept_request, i_wb_ack })
	2'b01:	last_ack <= (acks_expected <= 2);
	2'b10:	last_ack <= (acks_expected == 0)&&(skid_arlen == 0);
	2'b11:	last_ack <= (acks_expected < 2)&&(skid_arlen < 2)
				&&(!acks_expected[0]||!skid_arlen[0]);
	default: begin end
	endcase

	initial	fifo_nearfull = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		fifo_nearfull <= 1'b0;
	else case({ lastid_fifo_wr, S_AXI_RVALID && S_AXI_RREADY })
	2'b10: fifo_nearfull <= (lastid_fifo_fill >= (1<<LGFIFO)-2);
	2'b01: fifo_nearfull <= lastid_fifo_full;
	default: begin end
	endcase

	initial	wb_empty = 1'b1;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !o_wb_cyc)
		wb_empty <= 1'b1;
	else case({ lastid_fifo_wr, (i_wb_ack || i_wb_err) })
	2'b10: wb_empty <= 1'b0;
	2'b01: wb_empty <= (lastid_fifo_fill == resp_fifo_fill + 1);
	default: begin end
	endcase

	always @(*)
	begin
		S_AXI_RRESP[0] = 1'b0;
		S_AXI_RRESP[1] = response_err || (resp_fifo_empty && err_state);


		S_AXI_RVALID = !resp_fifo_empty
			|| (err_state && !lastid_fifo_empty);
	end

	initial	err_state = 0;
	always @(posedge S_AXI_ACLK)
	if (w_reset)
		err_state <= 1'b0;
	else if ((o_wb_cyc)&&(i_wb_err))
		err_state <= 1'b1;
	else if (lastid_fifo_empty && !midissue)
		err_state <= 1'b0;


	// Make Verilator happy
	// verilator lint_off UNUSED
	wire	unused;
	assign	unused = &{ 1'b0, S_AXI_ARLOCK, S_AXI_ARCACHE,
			S_AXI_ARPROT, S_AXI_ARQOS, resp_fifo_full };
	// verilator lint_on  UNUSED

`ifdef	FORMAL
	////////////////////////////////////////////////////////////////////////
	//
	// The following are a subset of the properties used to verify this
	// core.
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	reg	f_past_valid;
	initial f_past_valid = 1'b0;
	always @(posedge S_AXI_ACLK)
		f_past_valid <= 1'b1;

	////////////////////////////////////////////////////////////////////////
	//
	// Assumptions
	//
	//
	always @(*)
	if (!f_past_valid)
		assume(w_reset);

	////////////////////////////////////////////////////////////////////////
	//
	// Ad-hoc assertions
	//
	//

	////////////////////////////////////////////////////////////////////////
	//
	// Error state
	//
	//
	always @(*)
	if (err_state)
		assert(!o_wb_stb && !o_wb_cyc);

	////////////////////////////////////////////////////////////////////////
	//
	// Bus properties
	//
	//

	localparam	F_LGDEPTH = (LGFIFO>8) ? LGFIFO+1 : 10, F_LGRDFIFO = 72; // 9*F_LGFIFO;
	//
	// ...
	//
	wire	[(F_LGDEPTH-1):0]
			fwb_nreqs, fwb_nacks, fwb_outstanding;

	fwb_master #(.AW(AW), .DW(C_AXI_DATA_WIDTH), .F_MAX_STALL(2),
		.F_MAX_ACK_DELAY(3), .F_LGDEPTH(F_LGDEPTH),
		.F_OPT_DISCONTINUOUS(1))
		fwb(S_AXI_ACLK, w_reset,
			o_wb_cyc, o_wb_stb, 1'b0, o_wb_addr, {(DW){1'b0}}, 4'hf,
			i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
			fwb_nreqs, fwb_nacks, fwb_outstanding);

	always @(*)
	if (err_state)
		assert(fwb_outstanding == 0);


	faxi_slave	#(.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
			.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
			.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
			.F_LGDEPTH(F_LGDEPTH),
			.F_AXI_MAXSTALL(0),
			.F_AXI_MAXDELAY(0))
		faxi(.i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
			.i_axi_awready(1'b0),
			.i_axi_awaddr(0),
			.i_axi_awlen(8'h0),
			.i_axi_awsize(3'h0),
			.i_axi_awburst(2'h0),
			.i_axi_awlock(1'b0),
			.i_axi_awcache(4'h0),
			.i_axi_awprot(3'h0),
			.i_axi_awqos(4'h0),
			.i_axi_awvalid(1'b0),
			//
			.i_axi_wready(1'b0),
			.i_axi_wdata(0),
			.i_axi_wstrb(0),
			.i_axi_wlast(0),
			.i_axi_wvalid(1'b0),
			//
			.i_axi_bid(0),
			.i_axi_bresp(0),
			.i_axi_bvalid(1'b0),
			.i_axi_bready(1'b0),
			//
			.i_axi_arready(S_AXI_ARREADY),
			.i_axi_arid(S_AXI_ARID),
			.i_axi_araddr(S_AXI_ARADDR),
			.i_axi_arlen(S_AXI_ARLEN),
			.i_axi_arsize(S_AXI_ARSIZE),
			.i_axi_arburst(S_AXI_ARBURST),
			.i_axi_arlock(S_AXI_ARLOCK),
			.i_axi_arcache(S_AXI_ARCACHE),
			.i_axi_arprot(S_AXI_ARPROT),
			.i_axi_arqos(S_AXI_ARQOS),
			.i_axi_arvalid(S_AXI_ARVALID),
			//
			.i_axi_rresp(S_AXI_RRESP),
			.i_axi_rid(S_AXI_RID),
			.i_axi_rvalid(S_AXI_RVALID),
			.i_axi_rdata(S_AXI_RDATA),
			.i_axi_rlast(S_AXI_RLAST),
			.i_axi_rready(S_AXI_RREADY)
			//
			// ...
			//
			);

	//
	// ...
	//

	always @(*)
	if (!resp_fifo_empty && response_err)
		assert(resp_fifo_fill == 1);

	always @(*)
		assert(midissue == ((stblen > 0)||(last_stb)));

	always @(*)
	if (last_stb && !err_state)
		assert(o_wb_stb || lastid_fifo_full);

	always @(*)
	if (last_stb)
		assert(stblen == 0);

	always @(*)
	if (lastid_fifo_full)
	begin
		assert(!o_wb_stb);
		assert(!lastid_fifo_wr);
	end

	always @(*)
	if (!err_state)
	begin
		if (midissue && !last_stb)
			assert(!last_ack);

		assert(lastid_fifo_fill - resp_fifo_fill
			== fwb_outstanding);

		if (fwb_outstanding > 1)
			assert(!last_ack);
		else if (fwb_outstanding == 1)
			assert(midissue || last_ack);
		else if (o_wb_cyc) // && (fwb_outstanding ==0)
			assert(last_ack == last_stb);

		if (midissue)
			assert(o_wb_cyc);
	end

	always @(*)
	if (o_wb_cyc)
		assert(wb_empty == (lastid_fifo_fill == resp_fifo_fill));

	always @(*)
	if ((fwb_nacks == fwb_nreqs)&&(!midissue))
		assert(!o_wb_cyc);

	always @(*)
		assert(fwb_outstanding <= (1<<LGFIFO));

	always @(*)
		assert(fifo_nearfull == (lastid_fifo_fill >= (1<<LGFIFO)-1));

	always @(*)
	if (o_wb_stb)
		assert(last_ack == (last_stb&& wb_empty));//&&(!i_wb_stall);
	else if (o_wb_cyc && !midissue)
		assert(last_ack == (resp_fifo_fill + 1 >= lastid_fifo_fill));

	////////////////////////////////////////////////////////////////////////
	//
	// Cover checks
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	reg [3:0]	cvr_reads, cvr_read_bursts, cvr_rdid_bursts;
	reg [C_AXI_ID_WIDTH-1:0]	cvr_read_id;

	initial	cvr_reads = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_reads <= 1;
	else if (i_wb_err)
		cvr_reads <= 0;
	else if (S_AXI_RVALID && S_AXI_RREADY && !cvr_reads[3]
			&& cvr_reads > 0)
		cvr_reads <= cvr_reads + 1;

	initial	cvr_read_bursts = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_read_bursts <= 1;
	else if (S_AXI_ARVALID && S_AXI_ARLEN < 1)
		cvr_read_bursts <= 0;
	else if (i_wb_err)
		cvr_read_bursts <= 0;
	else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST
			&& !cvr_read_bursts[3] && cvr_read_bursts > 0)
		cvr_read_bursts <= cvr_read_bursts + 1;

	initial	cvr_read_id = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_read_id <= 1;
	else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST)
		cvr_read_id <= cvr_read_id + 1;

	initial	cvr_rdid_bursts = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_rdid_bursts <= 1;
	else if (S_AXI_ARVALID && S_AXI_ARLEN < 1)
		cvr_rdid_bursts <= 0;
	else if (i_wb_err)
		cvr_rdid_bursts <= 0;
	else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST
			&& S_AXI_RID == cvr_read_id
			&& !cvr_rdid_bursts[3] && cvr_rdid_bursts > 0)
		cvr_rdid_bursts <= cvr_rdid_bursts + 1;

	always @(*)
		cover(cvr_reads == 4);

	always @(*)
		cover(cvr_read_bursts == 4);

	always @(*)
		cover(cvr_rdid_bursts == 4);

`endif
endmodule