verilog/rtl/softshell/third_party/wb2axip/rtl/aximrd2wbsp.v - third_party/shuttle/sky130/mpw-001/slot-003 - Git at Google

 ////////////////////////////////////////////////////////////////////////////////
 //
 // 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
	////////////////////////////////////////////////////////////////////////////////
	//
	// 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