////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	axilite2axi.v
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	
//
// 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 axilite2axi #(
	parameter	C_AXI_ID_WIDTH	= 4,
			C_AXI_ADDR_WIDTH= 32,
			C_AXI_DATA_WIDTH= 32,
	parameter [C_AXI_ID_WIDTH-1:0]	C_AXI_WRITE_ID = 0,
					C_AXI_READ_ID = 0,
	localparam	ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3
	) (
	input	wire				ACLK,
	input	wire				ARESETN,
	// Slave write signals
	input	wire				S_AXI_AWVALID,
	output	wire				S_AXI_AWREADY,
	input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_AWADDR,
	input	wire	[3-1:0]			S_AXI_AWPROT,
	// Slave write data signals
	input	wire				S_AXI_WVALID,
	output	wire				S_AXI_WREADY,
	input	wire	[C_AXI_DATA_WIDTH-1:0]	S_AXI_WDATA,
	input	wire	[C_AXI_DATA_WIDTH/8-1:0] S_AXI_WSTRB,
	// Slave return write response
	output	wire				S_AXI_BVALID,
	input	wire				S_AXI_BREADY,
	output	wire	[2-1:0]			S_AXI_BRESP,
	// Slave read signals
	input	wire				S_AXI_ARVALID,
	output	wire				S_AXI_ARREADY,
	input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_ARADDR,
	input	wire	[3-1:0]			S_AXI_ARPROT,
	// Slave read data signals
	output	wire				S_AXI_RVALID,
	input	wire				S_AXI_RREADY,
	output	wire	[C_AXI_DATA_WIDTH-1:0]	S_AXI_RDATA,
	output	wire	[2-1:0]			S_AXI_RRESP,
	//
	// Master interface write address
	output	wire				M_AXI_AWVALID,
	input	wire				M_AXI_AWREADY,
	output	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_AWID,
	output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_AWADDR,
	output	wire	[8-1:0]			M_AXI_AWLEN,
	output	wire	[3-1:0]			M_AXI_AWSIZE,
	output	wire	[2-1:0]			M_AXI_AWBURST,
	output	wire				M_AXI_AWLOCK,
	output	wire	[4-1:0]			M_AXI_AWCACHE,
	output	wire	[3-1:0]			M_AXI_AWPROT,
	output	wire	[4-1:0]			M_AXI_AWQOS,
	// Master write data
	output	wire				M_AXI_WVALID,
	input	wire				M_AXI_WREADY,
	output	wire	[C_AXI_DATA_WIDTH-1:0]	M_AXI_WDATA,
	output	wire	[C_AXI_DATA_WIDTH/8-1:0] M_AXI_WSTRB,
	output	wire				M_AXI_WLAST,
	// Master write response
	input	wire				M_AXI_BVALID,
	output	wire				M_AXI_BREADY,
	input	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_BID,
	input	wire	[1:0]			M_AXI_BRESP,
	// Master interface read address
	output	wire				M_AXI_ARVALID,
	input	wire				M_AXI_ARREADY,
	output	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_ARID,
	output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_ARADDR,
	output	wire	[8-1:0]			M_AXI_ARLEN,
	output	wire	[3-1:0]			M_AXI_ARSIZE,
	output	wire	[2-1:0]			M_AXI_ARBURST,
	output	wire				M_AXI_ARLOCK,
	output	wire	[4-1:0]			M_AXI_ARCACHE,
	output	wire	[3-1:0]			M_AXI_ARPROT,
	output	wire	[4-1:0]			M_AXI_ARQOS,
	// Master interface read data return
	input	wire				M_AXI_RVALID,
	output	wire				M_AXI_RREADY,
	input	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_RID,
	input	wire	[C_AXI_DATA_WIDTH-1:0]	M_AXI_RDATA,
	input	wire				M_AXI_RLAST,
	input	wire	[2-1:0]			M_AXI_RRESP
	);

	assign	M_AXI_AWID    = C_AXI_WRITE_ID;
	assign	M_AXI_AWADDR  = S_AXI_AWADDR;
	assign	M_AXI_AWLEN   = 0;
	assign	M_AXI_AWSIZE  = ADDRLSB[2:0];
	assign	M_AXI_AWBURST = 0;
	assign	M_AXI_AWLOCK  = 0;
	assign	M_AXI_AWCACHE = 4'b0011; // As recommended by Xilinx UG1037
	assign	M_AXI_AWPROT  = S_AXI_AWPROT;
	assign	M_AXI_AWQOS   = 0;
	assign	M_AXI_AWVALID = S_AXI_AWVALID;
	assign	S_AXI_AWREADY = M_AXI_AWREADY;
	// Master write data
	assign	M_AXI_WDATA   = S_AXI_WDATA;
	assign	M_AXI_WLAST   = 1;
	assign	M_AXI_WSTRB   = S_AXI_WSTRB;
	assign	M_AXI_WVALID  = S_AXI_WVALID;
	assign	S_AXI_WREADY  = M_AXI_WREADY;
	// Master write response
	assign	S_AXI_BRESP   = M_AXI_BRESP;
	assign	S_AXI_BVALID  = M_AXI_BVALID;
	assign	M_AXI_BREADY  = S_AXI_BREADY;
	//
	//
	assign	M_AXI_ARID    = C_AXI_READ_ID;
	assign	M_AXI_ARADDR  = S_AXI_ARADDR;
	assign	M_AXI_ARLEN   = 0;
	assign	M_AXI_ARSIZE  = ADDRLSB[2:0];
	assign	M_AXI_ARBURST = 0;
	assign	M_AXI_ARLOCK  = 0;
	assign	M_AXI_ARCACHE = 4'b0011; // As recommended by Xilinx UG1037
	assign	M_AXI_ARPROT  = S_AXI_ARPROT;
	assign	M_AXI_ARQOS   = 0;
	assign	M_AXI_ARVALID = S_AXI_ARVALID;
	assign	S_AXI_ARREADY = M_AXI_ARREADY;
	//
	assign	S_AXI_RDATA   = M_AXI_RDATA;
	assign	S_AXI_RRESP   = M_AXI_RRESP;
	assign	S_AXI_RVALID  = M_AXI_RVALID;
	assign	M_AXI_RREADY  = S_AXI_RREADY;

	// Make Verilator happy
	// Verilator lint_off UNUSED
	wire	unused;
	assign	unused = &{ 1'b0, ACLK, ARESETN, M_AXI_RLAST, M_AXI_RID, M_AXI_BID };
	// Verilator lint_on UNUSED

`ifdef	FORMAL
	//
	// The following are some of the properties used to verify this design
	//

	localparam	F_LGDEPTH = 10;

	wire	[F_LGDEPTH-1:0]	faxil_awr_outstanding,
				faxil_wr_outstanding, faxil_rd_outstanding;

	faxil_slave #(
			.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
			.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
			.F_LGDEPTH(10),
			.F_AXI_MAXRSTALL(4),
			.F_AXI_MAXWAIT(9),
			.F_AXI_MAXDELAY(0)
	) faxil(.i_clk(ACLK), .i_axi_reset_n(ARESETN),
		//
		.i_axi_awready(S_AXI_AWREADY),
		.i_axi_awaddr( S_AXI_AWADDR),
		.i_axi_awcache(4'h0),
		.i_axi_awprot( S_AXI_AWPROT),
		.i_axi_awvalid(S_AXI_AWVALID),
		//
		.i_axi_wready(S_AXI_WREADY),
		.i_axi_wdata( S_AXI_WDATA),
		.i_axi_wstrb( S_AXI_WSTRB),
		.i_axi_wvalid(S_AXI_WVALID),
		//
		.i_axi_bready(S_AXI_BREADY),
		.i_axi_bresp( S_AXI_BRESP),
		.i_axi_bvalid(S_AXI_BVALID),
		//
		.i_axi_arready(S_AXI_ARREADY),
		.i_axi_araddr( S_AXI_ARADDR),
		.i_axi_arcache(4'h0),
		.i_axi_arprot( S_AXI_ARPROT),
		.i_axi_arvalid(S_AXI_ARVALID),
		//
		//
		.i_axi_rready(S_AXI_RREADY),
		.i_axi_rresp( S_AXI_RRESP),
		.i_axi_rvalid(S_AXI_RVALID),
		.i_axi_rdata( S_AXI_RDATA),
		//
		.f_axi_awr_outstanding(faxil_awr_outstanding),
		.f_axi_wr_outstanding(faxil_wr_outstanding),
		.f_axi_rd_outstanding(faxil_rd_outstanding));

	//
	// ...
	//

	faxi_master #(
			.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
			.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
			.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
			.OPT_MAXBURST(0),
			.OPT_EXCLUSIVE(1'b0),
			.OPT_NARROW_BURST(1'b0),
			.F_OPT_NO_RESET(1'b1),
			.F_LGDEPTH(10),
			.F_AXI_MAXSTALL(4),
			.F_AXI_MAXRSTALL(0),
			.F_AXI_MAXDELAY(4)
	) faxi(.i_clk(ACLK), .i_axi_reset_n(ARESETN),
		//
		.i_axi_awready(M_AXI_AWREADY),
		.i_axi_awid(   M_AXI_AWID),
		.i_axi_awaddr( M_AXI_AWADDR),
		.i_axi_awlen(  M_AXI_AWLEN),
		.i_axi_awsize( M_AXI_AWSIZE),
		.i_axi_awburst(M_AXI_AWBURST),
		.i_axi_awlock( M_AXI_AWLOCK),
		.i_axi_awcache(M_AXI_AWCACHE),
		.i_axi_awprot( M_AXI_AWPROT),
		.i_axi_awqos(  M_AXI_AWQOS),
		.i_axi_awvalid(M_AXI_AWVALID),
		//
		.i_axi_wready(M_AXI_WREADY),
		.i_axi_wdata( M_AXI_WDATA),
		.i_axi_wstrb( M_AXI_WSTRB),
		.i_axi_wlast( M_AXI_WLAST),
		.i_axi_wvalid(M_AXI_WVALID),
		//
		.i_axi_bready(M_AXI_BREADY),
		.i_axi_bid(   M_AXI_BID),
		.i_axi_bresp( M_AXI_BRESP),
		.i_axi_bvalid(M_AXI_BVALID),
		//
		.i_axi_arready(M_AXI_ARREADY),
		.i_axi_arid(   M_AXI_ARID),
		.i_axi_araddr( M_AXI_ARADDR),
		.i_axi_arlen(  M_AXI_ARLEN),
		.i_axi_arsize( M_AXI_ARSIZE),
		.i_axi_arburst(M_AXI_ARBURST),
		.i_axi_arlock( M_AXI_ARLOCK),
		.i_axi_arcache(M_AXI_ARCACHE),
		.i_axi_arprot( M_AXI_ARPROT),
		.i_axi_arqos(  M_AXI_ARQOS),
		.i_axi_arvalid(M_AXI_ARVALID),
		//
		.i_axi_rid(   M_AXI_RID),
		.i_axi_rdata( M_AXI_RDATA),
		.i_axi_rready(M_AXI_RREADY),
		.i_axi_rresp( M_AXI_RRESP),
		.i_axi_rvalid(M_AXI_RVALID),
		//
		.f_axi_awr_nbursts(faxi_awr_nbursts),
		.f_axi_wr_pending(faxi_wr_pending),
		.f_axi_rd_nbursts(faxi_rd_nbursts),
		.f_axi_rd_outstanding(faxi_rd_outstanding)
		//
		// ...
		//
		);


	////////////////////////////////////////////////////////////////////////
	//
	// Induction rule checks
	//
	////////////////////////////////////////////////////////////////////////
	//
	//

	// First rule: the AXI solver isn't permitted to have any more write
	// bursts outstanding than the AXI-lite interface has.
	always @(*)
		assert(faxi_awr_nbursts == faxil_awr_outstanding);

	//
	// Second: Since our bursts are limited to one value each, and since
	// we can't send address bursts ahead of their data counterparts,
	// (AXI property limitation) faxi_wr_pending can only ever be one or
	// zero, and the counters must match
	always @(*)
	begin
		//
		// ...
		//

		if (faxil_awr_outstanding != 0)
		begin
			assert((faxil_awr_outstanding == faxil_wr_outstanding)
			||(faxil_awr_outstanding-1 == faxil_wr_outstanding));
		end

		if (faxil_awr_outstanding == 0)
			assert(faxil_wr_outstanding == 0);
	end

	//
	// ...
	//

	////////////////////////////////////////////////////////////////////////
	//
	// Known "bugs"
	//
	////////////////////////////////////////////////////////////////////////
	//
	// These are really more limitations in the AXI properties than
	// bugs in the code, but they need to be documented here.
	//
	generate if (C_AXI_DATA_WIDTH > 8)
	begin
		// The AXI-lite property checker doesn't validate WSTRB
		// values like it should.  If we don't force the AWADDR
		// LSBs to zero, the solver will pick an invalid WSTRB.
		//
		always @(*)
			assume(S_AXI_AWADDR[$clog2(C_AXI_DATA_WIDTH)-3:0] == 0);
		always @(*)
			assert(faxi_wr_addr[$clog2(C_AXI_DATA_WIDTH)-3:0] == 0);
	end endgenerate

	//
	// The AXI solver can't handle write transactions without either a
	// concurrent or proceeding write address burst.  Here we make that
	// plain.  It's not likely to cause any problems, but still worth
	// noting.
	always @(*)
	if (faxil_awr_outstanding == faxil_wr_outstanding)
		assume(S_AXI_AWVALID || !S_AXI_WVALID);
	else if (faxil_awr_outstanding > faxil_wr_outstanding)
		assume(!S_AXI_AWVALID);

	//
	// We need to make certain that our counters never overflow.  This is
	// an assertion within the property checkers, so we need an appropriate
	// matching assumption here.  In practice, F_LGDEPTH could be set
	// so arbitrarily large that this assumption would never get hit,
	// but the solver doesn't know that.
	always @(*)
	if (faxil_rd_outstanding >= {{(F_LGDEPTH-1){1'b1}}, 1'b0 })
		assume(!S_AXI_ARVALID);

	always @(*)
	if (faxil_awr_outstanding >= {{(F_LGDEPTH-1){1'b1}}, 1'b0 })
		assume(!S_AXI_AWVALID);

`endif
endmodule
`ifndef	YOSYS
`default_nettype wire
`endif