rtl/wb2axip: add to version control

1 files changed, 1285 insertions, 0 deletions

diff --git a/rtl/wb2axip/demofull.v b/rtl/wb2axip/demofull.v
new file mode 100644
index 0000000..5d0c604
--- /dev/null
+++ b/rtl/wb2axip/demofull.v
@@ -0,0 +1,1285 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: 	demofull.v
+// {{{
+// Project:	WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose:	Demonstrate a formally verified AXI4 core with a (basic)
+//		interface.  This interface is explained below.
+//
+// Performance: This core has been designed for a total throughput of one beat
+//		per clock cycle.  Both read and write channels can achieve
+//	this.  The write channel will also introduce two clocks of latency,
+//	assuming no other latency from the master.  This means it will take
+//	a minimum of 3+AWLEN clock cycles per transaction of (1+AWLEN) beats,
+//	including both address and acknowledgment cycles.  The read channel
+//	will introduce a single clock of latency, requiring 2+ARLEN cycles
+//	per transaction of 1+ARLEN beats.
+//
+// Creator:	Dan Gisselquist, Ph.D.
+//		Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2019-2024, 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 demofull #(
+		// {{{
+		parameter integer C_S_AXI_ID_WIDTH	= 2,
+		parameter integer C_S_AXI_DATA_WIDTH	= 32,
+		parameter integer C_S_AXI_ADDR_WIDTH	= 6,
+		parameter	[0:0]	OPT_LOCK     = 1'b0,
+		parameter	[0:0]	OPT_LOCKID   = 1'b1,
+		parameter	[0:0]	OPT_LOWPOWER = 1'b0,
+		// Some useful short-hand definitions
+		localparam	LSB = $clog2(C_S_AXI_DATA_WIDTH)-3
+		// }}}
+	) (
+		// {{{
+		// User ports
+		// {{{
+		// A very basic protocol-independent peripheral interface
+		// 1. A value will be written any time o_we is true
+		// 2. A value will be read any time o_rd is true
+		// 3. Such a slave might just as easily be written as:
+		//
+		//	always @(posedge S_AXI_ACLK)
+		//	if (o_we)
+		//	begin
+		//	    for(k=0; k<C_S_AXI_DATA_WIDTH/8; k=k+1)
+		//	    begin
+		//		if (o_wstrb[k])
+		//		mem[o_waddr[AW-1:LSB]][k*8+:8] <= o_wdata[k*8+:8]
+		//	    end
+		//	end
+		//
+		//	always @(posedge S_AXI_ACLK)
+		//	if (o_rd)
+		//		i_rdata <= mem[o_raddr[AW-1:LSB]];
+		//
+		// 4. The rule on the input is that i_rdata must be registered,
+		//    and that it must only change if o_rd is true.  Violating
+		//    this rule will cause this core to violate the AXI
+		//    protocol standard, as this value is not registered within
+		//    this core
+		output	reg					o_we,
+		output	reg	[C_S_AXI_ADDR_WIDTH-LSB-1:0]	o_waddr,
+		output	reg	[C_S_AXI_DATA_WIDTH-1:0]	o_wdata,
+		output	reg	[C_S_AXI_DATA_WIDTH/8-1:0]	o_wstrb,
+		//
+		output	reg					o_rd,
+		output	reg	[C_S_AXI_ADDR_WIDTH-LSB-1:0]	o_raddr,
+		input	wire	[C_S_AXI_DATA_WIDTH-1:0]	i_rdata,
+		//
+		// User ports ends
+		// }}}
+		// Do not modify the ports beyond this line
+		// AXI signals
+		// {{{
+		// Global Clock Signal
+		input wire  S_AXI_ACLK,
+		// Global Reset Signal. This Signal is Active LOW
+		input wire  S_AXI_ARESETN,
+
+		// Write address channel
+		// {{{
+		// Write Address ID
+		input wire [C_S_AXI_ID_WIDTH-1 : 0] S_AXI_AWID,
+		// Write address
+		input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_AWADDR,
+		// Burst length. The burst length gives the exact number of
+		// transfers in a burst
+		input wire [7 : 0] S_AXI_AWLEN,
+		// Burst size. This signal indicates the size of each transfer
+		// in the burst
+		input wire [2 : 0] S_AXI_AWSIZE,
+		// Burst type. The burst type and the size information,
+		// determine how the address for each transfer within the burst
+		// is calculated.
+		input wire [1 : 0] S_AXI_AWBURST,
+		// Lock type. Provides additional information about the
+		// atomic characteristics of the transfer.
+		input wire  S_AXI_AWLOCK,
+		// Memory type. This signal indicates how transactions
+		// are required to progress through a system.
+		input wire [3 : 0] S_AXI_AWCACHE,
+		// Protection type. This signal indicates the privilege
+		// and security level of the transaction, and whether
+		// the transaction is a data access or an instruction access.
+		input wire [2 : 0] S_AXI_AWPROT,
+		// Quality of Service, QoS identifier sent for each
+		// write transaction.
+		input wire [3 : 0] S_AXI_AWQOS,
+		// Region identifier. Permits a single physical interface
+		// on a slave to be used for multiple logical interfaces.
+		// Write address valid. This signal indicates that
+		// the channel is signaling valid write address and
+		// control information.
+		input wire  S_AXI_AWVALID,
+		// Write address ready. This signal indicates that
+		// the slave is ready to accept an address and associated
+		// control signals.
+		output wire  S_AXI_AWREADY,
+		// }}}
+		// Write data channel
+		// {{{
+		// Write Data
+		input wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_WDATA,
+		// Write strobes. This signal indicates which byte
+		// lanes hold valid data. There is one write strobe
+		// bit for each eight bits of the write data bus.
+		input wire [(C_S_AXI_DATA_WIDTH/8)-1 : 0] S_AXI_WSTRB,
+		// Write last. This signal indicates the last transfer
+		// in a write burst.
+		input wire  S_AXI_WLAST,
+		// Optional User-defined signal in the write data channel.
+		// Write valid. This signal indicates that valid write
+		// data and strobes are available.
+		input wire  S_AXI_WVALID,
+		// Write ready. This signal indicates that the slave
+		// can accept the write data.
+		output wire  S_AXI_WREADY,
+		// }}}
+		// Write response channel
+		// {{{
+		// Response ID tag. This signal is the ID tag of the
+		// write response.
+		output wire [C_S_AXI_ID_WIDTH-1 : 0] S_AXI_BID,
+		// Write response. This signal indicates the status
+		// of the write transaction.
+		output wire [1 : 0] S_AXI_BRESP,
+		// Optional User-defined signal in the write response channel.
+		// Write response valid. This signal indicates that the
+		// channel is signaling a valid write response.
+		output wire  S_AXI_BVALID,
+		// Response ready. This signal indicates that the master
+		// can accept a write response.
+		input wire  S_AXI_BREADY,
+		// }}}
+		// Read address channel
+		// {{{
+		// Read address ID. This signal is the identification
+		// tag for the read address group of signals.
+		input wire [C_S_AXI_ID_WIDTH-1 : 0] S_AXI_ARID,
+		// Read address. This signal indicates the initial
+		// address of a read burst transaction.
+		input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_ARADDR,
+		// Burst length. The burst length gives the exact number of
+		// transfers in a burst
+		input wire [7 : 0] S_AXI_ARLEN,
+		// Burst size. This signal indicates the size of each transfer
+		// in the burst
+		input wire [2 : 0] S_AXI_ARSIZE,
+		// Burst type. The burst type and the size information,
+		// determine how the address for each transfer within the
+		// burst is calculated.
+		input wire [1 : 0] S_AXI_ARBURST,
+		// Lock type. Provides additional information about the
+		// atomic characteristics of the transfer.
+		input wire  S_AXI_ARLOCK,
+		// Memory type. This signal indicates how transactions
+		// are required to progress through a system.
+		input wire [3 : 0] S_AXI_ARCACHE,
+		// Protection type. This signal indicates the privilege
+		// and security level of the transaction, and whether
+		// the transaction is a data access or an instruction access.
+		input wire [2 : 0] S_AXI_ARPROT,
+		// Quality of Service, QoS identifier sent for each
+		// read transaction.
+		input wire [3 : 0] S_AXI_ARQOS,
+		// Region identifier. Permits a single physical interface
+		// on a slave to be used for multiple logical interfaces.
+		// Optional User-defined signal in the read address channel.
+		// Write address valid. This signal indicates that
+		// the channel is signaling valid read address and
+		// control information.
+		input wire  S_AXI_ARVALID,
+		// Read address ready. This signal indicates that
+		// the slave is ready to accept an address and associated
+		// control signals.
+		output wire  S_AXI_ARREADY,
+		// }}}
+		// Read data (return) channel
+		// {{{
+		// Read ID tag. This signal is the identification tag
+		// for the read data group of signals generated by the slave.
+		output wire [C_S_AXI_ID_WIDTH-1 : 0] S_AXI_RID,
+		// Read Data
+		output wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_RDATA,
+		// Read response. This signal indicates the status of
+		// the read transfer.
+		output wire [1 : 0] S_AXI_RRESP,
+		// Read last. This signal indicates the last transfer
+		// in a read burst.
+		output wire  S_AXI_RLAST,
+		// Optional User-defined signal in the read address channel.
+		// Read valid. This signal indicates that the channel
+		// is signaling the required read data.
+		output wire  S_AXI_RVALID,
+		// Read ready. This signal indicates that the master can
+		// accept the read data and response information.
+		input wire  S_AXI_RREADY
+		// }}}
+		// }}}
+		// }}}
+	);
+
+	// Local declarations
+	// {{{
+	// More useful shorthand definitions
+	localparam	AW = C_S_AXI_ADDR_WIDTH;
+	localparam	DW = C_S_AXI_DATA_WIDTH;
+	localparam	IW = C_S_AXI_ID_WIDTH;
+	// Double buffer the write response channel only
+	reg	[IW-1 : 0]	r_bid;
+	reg			r_bvalid;
+	reg	[IW-1 : 0]	axi_bid;
+	reg			axi_bvalid;
+
+	reg			axi_awready, axi_wready;
+	reg	[AW-1:0]	waddr;
+	wire	[AW-1:0]	next_wr_addr;
+
+	// Vivado will warn about wlen only using 4-bits.  This is
+	// to be expected, since the axi_addr module only needs to use
+	// the bottom four bits of wlen to determine address increments
+	reg	[7:0]		wlen;
+	// Vivado will also warn about the top bit of wsize being unused.
+	// This is also to be expected for a DATA_WIDTH of 32-bits.
+	reg	[2:0]		wsize;
+	reg	[1:0]		wburst;
+
+	wire			m_awvalid, m_awlock;
+	reg			m_awready;
+	wire	[AW-1:0]	m_awaddr;
+	wire	[1:0]		m_awburst;
+	wire	[2:0]		m_awsize;
+	wire	[7:0]		m_awlen;
+	wire	[IW-1:0]	m_awid;
+
+	wire	[AW-1:0]	next_rd_addr;
+
+	// Vivado will warn about rlen only using 4-bits.  This is
+	// to be expected, since for a DATA_WIDTH of 32-bits, the axi_addr
+	// module only uses the bottom four bits of rlen to determine
+	// address increments
+	reg	[7:0]		rlen;
+	// Vivado will also warn about the top bit of wsize being unused.
+	// This is also to be expected for a DATA_WIDTH of 32-bits.
+	reg	[2:0]		rsize;
+	reg	[1:0]		rburst;
+	reg	[IW-1:0]	rid;
+	reg			rlock;
+	reg			axi_arready;
+	reg	[8:0]		axi_rlen;
+	reg	[AW-1:0]	raddr;
+
+	// Read skid buffer
+	reg			rskd_valid, rskd_last, rskd_lock;
+	wire			rskd_ready;
+	reg	[IW-1:0]	rskd_id;
+
+	// Exclusive address register checking
+	reg			exclusive_write, block_write;
+	wire			write_lock_valid;
+	reg			axi_exclusive_write;
+
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// AW Skid buffer
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	skidbuffer #(
+		// {{{
+		.DW(AW+2+3+1+8+IW),
+		.OPT_LOWPOWER(OPT_LOWPOWER),
+		.OPT_OUTREG(1'b0)
+		// }}}
+	) awbuf(
+		// {{{
+		.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+		.i_valid(S_AXI_AWVALID), .o_ready(S_AXI_AWREADY),
+			.i_data({ S_AXI_AWADDR, S_AXI_AWBURST, S_AXI_AWSIZE,
+				S_AXI_AWLOCK, S_AXI_AWLEN, S_AXI_AWID }),
+		.o_valid(m_awvalid), .i_ready(m_awready),
+			.o_data({ m_awaddr, m_awburst, m_awsize,
+				m_awlock, m_awlen, m_awid })
+		// }}}
+	);
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Write processing
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// axi_awready, axi_wready
+	// {{{
+	initial	axi_awready = 1;
+	initial	axi_wready  = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+	begin
+		axi_awready  <= 1;
+		axi_wready   <= 0;
+	end else if (m_awvalid && m_awready)
+	begin
+		axi_awready <= 0;
+		axi_wready  <= 1;
+	end else if (S_AXI_WVALID && S_AXI_WREADY)
+	begin
+		axi_awready <= (S_AXI_WLAST)&&(!S_AXI_BVALID || S_AXI_BREADY);
+		axi_wready  <= (!S_AXI_WLAST);
+	end else if (!axi_awready)
+	begin
+		if (S_AXI_WREADY)
+			axi_awready <= 1'b0;
+		else if (r_bvalid && !S_AXI_BREADY)
+			axi_awready <= 1'b0;
+		else
+			axi_awready <= 1'b1;
+	end
+	// }}}
+
+	// Exclusive write calculation
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || !OPT_LOCK)
+	begin
+		exclusive_write <= 0;
+		block_write <= 0;
+	end else if (m_awvalid && m_awready)
+	begin
+		exclusive_write <= 1'b0;
+		block_write     <= 1'b0;
+		if (write_lock_valid)
+			exclusive_write <= 1'b1;
+		else if (m_awlock)
+			block_write <= 1'b1;
+	end else if (m_awready)
+	begin
+		exclusive_write <= 1'b0;
+		block_write     <= 1'b0;
+	end
+
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || !OPT_LOCK)
+		axi_exclusive_write <= 0;
+	else if (!S_AXI_BVALID || S_AXI_BREADY)
+	begin
+		axi_exclusive_write <= exclusive_write;
+		if (OPT_LOWPOWER && (!S_AXI_WVALID || !S_AXI_WREADY || !S_AXI_WLAST)
+				&& !r_bvalid)
+			axi_exclusive_write <= 0;
+	end
+	// }}}
+
+	// Next write address calculation
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (m_awready)
+	begin
+		waddr    <= m_awaddr;
+		wburst   <= m_awburst;
+		wsize    <= m_awsize;
+		wlen     <= m_awlen;
+	end else if (S_AXI_WVALID)
+		waddr <= next_wr_addr;
+
+	axi_addr #(
+		// {{{
+		.AW(AW), .DW(DW)
+		// }}}
+	) get_next_wr_addr(
+		// {{{
+		waddr, wsize, wburst, wlen,
+			next_wr_addr
+		// }}}
+	);
+	// }}}
+
+	// o_w*
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	begin
+		o_we    <= (S_AXI_WVALID && S_AXI_WREADY);
+		o_waddr <= waddr[AW-1:LSB];
+		o_wdata <= S_AXI_WDATA;
+		if (block_write)
+			o_wstrb <= 0;
+		else
+			o_wstrb <= S_AXI_WSTRB;
+
+		if (!S_AXI_ARESETN)
+			o_we <= 0;
+		if (OPT_LOWPOWER && (!S_AXI_ARESETN || !S_AXI_WVALID
+					|| !S_AXI_WREADY))
+		begin
+			o_waddr <= 0;
+			o_wdata <= 0;
+			o_wstrb <= 0;
+		end
+	end
+	// }}}
+
+	//
+	// Write return path
+	// {{{
+	// r_bvalid
+	// {{{
+	initial	r_bvalid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		r_bvalid <= 1'b0;
+	else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST
+			&&(S_AXI_BVALID && !S_AXI_BREADY))
+		r_bvalid <= 1'b1;
+	else if (S_AXI_BREADY)
+		r_bvalid <= 1'b0;
+	// }}}
+
+	// r_bid, axi_bid
+	// {{{
+	initial	r_bid = 0;
+	initial	axi_bid = 0;
+	always @(posedge S_AXI_ACLK)
+	begin
+		if (m_awready && (!OPT_LOWPOWER || m_awvalid))
+			r_bid    <= m_awid;
+
+		if (!S_AXI_BVALID || S_AXI_BREADY)
+			axi_bid <= r_bid;
+
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+		begin
+			r_bid <= 0;
+			axi_bid <= 0;
+		end
+	end
+	// }}}
+
+	// axi_bvalid
+	// {{{
+	initial	axi_bvalid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		axi_bvalid <= 0;
+	else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST)
+		axi_bvalid <= 1;
+	else if (S_AXI_BREADY)
+		axi_bvalid <= r_bvalid;
+	// }}}
+
+	// m_awready
+	// {{{
+	always @(*)
+	begin
+		m_awready = axi_awready;
+		if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST
+			&& (!S_AXI_BVALID || S_AXI_BREADY))
+			m_awready = 1;
+	end
+	// }}}
+
+	// At one time, axi_awready was the same as S_AXI_AWREADY.  Now, though,
+	// with the extra write address skid buffer, this is no longer the case.
+	// S_AXI_AWREADY is handled/created/managed by the skid buffer.
+	//
+	// assign S_AXI_AWREADY = axi_awready;
+	//
+	// The rest of these signals can be set according to their registered
+	// values above.
+	assign	S_AXI_WREADY  = axi_wready;
+	assign	S_AXI_BVALID  = axi_bvalid;
+	assign	S_AXI_BID     = axi_bid;
+	//
+	// This core does not produce any bus errors, nor does it support
+	// exclusive access, so 2'b00 will always be the correct response.
+	assign	S_AXI_BRESP = { 1'b0, axi_exclusive_write };
+	// }}}
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Read processing
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// axi_arready
+	// {{{
+	initial axi_arready = 1;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		axi_arready <= 1;
+	else if (S_AXI_ARVALID && S_AXI_ARREADY)
+		axi_arready <= (S_AXI_ARLEN==0)&&(o_rd);
+	else if (o_rd)
+		axi_arready <= (axi_rlen <= 1);
+	// }}}
+
+	// axi_rlen
+	// {{{
+	initial	axi_rlen = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		axi_rlen <= 0;
+	else if (S_AXI_ARVALID && S_AXI_ARREADY)
+		axi_rlen <= S_AXI_ARLEN + (o_rd ? 0:1);
+	else if (o_rd)
+		axi_rlen <= axi_rlen - 1;
+	// }}}
+
+	// Next read address calculation
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (o_rd)
+		raddr <= next_rd_addr;
+	else if (S_AXI_ARREADY)
+	begin
+		raddr <= S_AXI_ARADDR;
+		if (OPT_LOWPOWER && !S_AXI_ARVALID)
+			raddr <= 0;
+	end
+
+	// r*
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (S_AXI_ARREADY)
+	begin
+		rburst   <= S_AXI_ARBURST;
+		rsize    <= S_AXI_ARSIZE;
+		rlen     <= S_AXI_ARLEN;
+		rid      <= S_AXI_ARID;
+		rlock    <= S_AXI_ARLOCK && S_AXI_ARVALID && OPT_LOCK;
+
+		if (OPT_LOWPOWER && !S_AXI_ARVALID)
+		begin
+			rburst   <= 0;
+			rsize    <= 0;
+			rlen     <= 0;
+			rid      <= 0;
+			rlock    <= 0;
+		end
+	end
+	// }}}
+
+	axi_addr #(
+		// {{{
+		.AW(AW), .DW(DW)
+		// }}}
+	) get_next_rd_addr(
+		// {{{
+		(S_AXI_ARREADY ? S_AXI_ARADDR : raddr),
+		(S_AXI_ARREADY  ? S_AXI_ARSIZE : rsize),
+		(S_AXI_ARREADY  ? S_AXI_ARBURST: rburst),
+		(S_AXI_ARREADY  ? S_AXI_ARLEN  : rlen),
+		next_rd_addr
+		// }}}
+	);
+	// }}}
+
+	// o_rd, o_raddr
+	// {{{
+	always @(*)
+	begin
+		o_rd = (S_AXI_ARVALID || !S_AXI_ARREADY);
+		if (S_AXI_RVALID && !S_AXI_RREADY)
+			o_rd = 0;
+		if (rskd_valid && !rskd_ready)
+			o_rd = 0;
+		o_raddr = (S_AXI_ARREADY ? S_AXI_ARADDR[AW-1:LSB] : raddr[AW-1:LSB]);
+	end
+	// }}}
+
+	// rskd_valid
+	// {{{
+	initial	rskd_valid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		rskd_valid <= 0;
+	else if (o_rd)
+		rskd_valid <= 1;
+	else if (rskd_ready)
+		rskd_valid <= 0;
+	// }}}
+
+	// rskd_id
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (!rskd_valid || rskd_ready)
+	begin
+		if (S_AXI_ARVALID && S_AXI_ARREADY)
+			rskd_id <= S_AXI_ARID;
+		else
+			rskd_id <= rid;
+	end
+	// }}}
+
+	// rskd_last
+	// {{{
+	initial rskd_last   = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!rskd_valid || rskd_ready)
+	begin
+		rskd_last <= 0;
+		if (o_rd && axi_rlen == 1)
+			rskd_last <= 1;
+		if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN == 0)
+			rskd_last <= 1;
+	end
+	// }}}
+
+	// rskd_lock
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || !OPT_LOCK)
+		rskd_lock <= 1'b0;
+	else if (!rskd_valid || rskd_ready)
+	begin
+		rskd_lock <= 0;
+		if (!OPT_LOWPOWER || o_rd)
+		begin
+			if (S_AXI_ARVALID && S_AXI_ARREADY)
+				rskd_lock <= S_AXI_ARLOCK;
+			else
+				rskd_lock <= rlock;
+		end
+	end
+	// }}}
+
+
+	// Outgoing read skidbuffer
+	// {{{
+	skidbuffer #(
+		// {{{
+		.OPT_LOWPOWER(OPT_LOWPOWER),
+		.OPT_OUTREG(1),
+		.DW(IW+2+DW)
+		// }}}
+	) rskid (
+		// {{{
+		.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+		.i_valid(rskd_valid), .o_ready(rskd_ready),
+		.i_data({ rskd_id, rskd_lock, rskd_last, i_rdata }),
+		.o_valid(S_AXI_RVALID), .i_ready(S_AXI_RREADY),
+			.o_data({ S_AXI_RID, S_AXI_RRESP[0], S_AXI_RLAST,
+					S_AXI_RDATA })
+		// }}}
+	);
+	// }}}
+
+	assign	S_AXI_RRESP[1] = 1'b0;
+	assign	S_AXI_ARREADY = axi_arready;
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Exclusive address caching
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	generate if (OPT_LOCK && !OPT_LOCKID)
+	begin : EXCLUSIVE_ACCESS_BLOCK
+		// {{{
+		// The AXI4 specification requires that we check one address
+		// per ID.  This isn't that.  This algorithm checks one ID,
+		// whichever the last ID was.  It's designed to be lighter on
+		// the logic requirements, and (unnoticably) not (fully) spec
+		// compliant.  (The difference, if noticed at all, will be in
+		// performance when multiple masters try to perform an exclusive
+		// transaction at once.)
+
+		// Local declarations
+		// {{{
+		reg			w_valid_lock_request, w_cancel_lock,
+					w_lock_request,
+					lock_valid, returned_lock_valid;
+		reg	[AW-LSB-1:0]	lock_start, lock_end;
+		reg	[3:0]		lock_len;
+		reg	[1:0]		lock_burst;
+		reg	[2:0]		lock_size;
+		reg	[IW-1:0]	lock_id;
+		reg			w_write_lock_valid;
+		// }}}
+
+		// w_lock_request
+		// {{{
+		always @(*)
+		begin
+			w_lock_request = 0;
+			if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLOCK)
+				w_lock_request = 1;
+		end
+		// }}}
+
+		// w_valid_lock_request
+		// {{{
+		always @(*)
+		begin
+			w_valid_lock_request = 0;
+			if (w_lock_request)
+				w_valid_lock_request = 1;
+			if (o_we && o_waddr == S_AXI_ARADDR[AW-1:LSB])
+				w_valid_lock_request = 0;
+		end
+		// }}}
+
+		// returned_lock_valid
+		// {{{
+		initial	returned_lock_valid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			returned_lock_valid <= 0;
+		else if (S_AXI_ARVALID && S_AXI_ARREADY
+					&& S_AXI_ARLOCK && S_AXI_ARID== lock_id)
+			returned_lock_valid <= 0;
+		else if (w_cancel_lock)
+			returned_lock_valid <= 0;
+		else if (rskd_valid && rskd_lock && rskd_ready)
+			returned_lock_valid <= lock_valid;
+		// }}}
+
+		// w_cancel_lock
+		// {{{
+		always @(*)
+			w_cancel_lock = (lock_valid && w_lock_request)
+				|| (lock_valid && o_we
+					&& o_waddr >= lock_start
+					&& o_waddr <= lock_end
+					&& o_wstrb != 0);
+		// }}}
+
+		// lock_valid
+		// {{{
+		initial	lock_valid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN || !OPT_LOCK)
+			lock_valid <= 0;
+		else begin
+			if (S_AXI_ARVALID && S_AXI_ARREADY
+					&& S_AXI_ARLOCK && S_AXI_ARID== lock_id)
+				lock_valid <= 0;
+			if (w_cancel_lock)
+				lock_valid <= 0;
+			if (w_valid_lock_request)
+				lock_valid <= 1;
+		end
+		// }}}
+
+		// lock_start, lock_end, lock_len, lock_size, lock_id
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (w_valid_lock_request)
+		begin
+			lock_start <= S_AXI_ARADDR[C_S_AXI_ADDR_WIDTH-1:LSB];
+			lock_end <= S_AXI_ARADDR[C_S_AXI_ADDR_WIDTH-1:LSB]
+					+ ((S_AXI_ARBURST == 2'b00) ? 0 : S_AXI_ARLEN[3:0]);
+			lock_len   <= S_AXI_ARLEN[3:0];
+			lock_burst <= S_AXI_ARBURST;
+			lock_size  <= S_AXI_ARSIZE;
+			lock_id    <= S_AXI_ARID;
+		end
+		// }}}
+
+		// w_write_lock_valid
+		// {{{
+		always @(*)
+		begin
+			w_write_lock_valid = returned_lock_valid;
+			if (!m_awvalid || !m_awready || !m_awlock || !lock_valid)
+				w_write_lock_valid = 0;
+			if (m_awaddr[C_S_AXI_ADDR_WIDTH-1:LSB] != lock_start)
+				w_write_lock_valid = 0;
+			if (m_awid != lock_id)
+				w_write_lock_valid = 0;
+			if (m_awlen[3:0] != lock_len)	// MAX transfer size is 16 beats
+				w_write_lock_valid = 0;
+			if (m_awburst != 2'b01 && lock_len != 0)
+				w_write_lock_valid = 0;
+			if (m_awsize != lock_size)
+				w_write_lock_valid = 0;
+		end
+		// }}}
+
+		assign	write_lock_valid = w_write_lock_valid;
+		// }}}
+	end else if (OPT_LOCK) // && OPT_LOCKID
+	begin : EXCLUSIVE_ACCESS_PER_ID
+		// {{{
+
+		genvar	gk;
+		wire	[(1<<IW)-1:0]	write_lock_valid_per_id;
+
+		for(gk=0; gk<(1<<IW); gk=gk+1)
+		begin : PER_ID_LOGIC
+		// {{{
+			// Local declarations
+			// {{{
+			reg			w_valid_lock_request,
+						w_cancel_lock,
+						lock_valid, returned_lock_valid;
+			reg	[1:0]		lock_burst;
+			reg	[2:0]		lock_size;
+			reg	[3:0]		lock_len;
+			reg	[AW-LSB-1:0]	lock_start, lock_end;
+			reg			w_write_lock_valid;
+			// }}}
+
+			// valid_lock_request
+			// {{{
+			always @(*)
+			begin
+				w_valid_lock_request = 0;
+				if (S_AXI_ARVALID && S_AXI_ARREADY
+						&& S_AXI_ARID == gk[IW-1:0]
+						&& S_AXI_ARLOCK)
+					w_valid_lock_request = 1;
+				if (o_we && o_waddr == S_AXI_ARADDR[AW-1:LSB])
+					w_valid_lock_request = 0;
+			end
+			// }}}
+
+			// returned_lock_valid
+			// {{{
+			initial	returned_lock_valid = 0;
+			always @(posedge S_AXI_ACLK)
+			if (!S_AXI_ARESETN)
+				returned_lock_valid <= 0;
+			else if (S_AXI_ARVALID && S_AXI_ARREADY
+					&&S_AXI_ARLOCK&&S_AXI_ARID== gk[IW-1:0])
+				returned_lock_valid <= 0;
+			else if (w_cancel_lock)
+				returned_lock_valid <= 0;
+			else if (rskd_valid && rskd_lock && rskd_ready
+					&& rskd_id == gk[IW-1:0])
+				returned_lock_valid <= lock_valid;
+			// }}}
+
+			// w_cancel_lock
+			// {{{
+			always @(*)
+				w_cancel_lock=(lock_valid&&w_valid_lock_request)
+					|| (lock_valid && o_we
+						&& o_waddr >= lock_start
+						&& o_waddr <= lock_end
+						&& o_wstrb != 0);
+			// }}}
+
+			// lock_valid
+			// {{{
+			initial	lock_valid = 0;
+			always @(posedge S_AXI_ACLK)
+			if (!S_AXI_ARESETN || !OPT_LOCK)
+				lock_valid <= 0;
+			else begin
+				if (S_AXI_ARVALID && S_AXI_ARREADY
+						&& S_AXI_ARLOCK
+						&& S_AXI_ARID == gk[IW-1:0])
+					lock_valid <= 0;
+				if (w_cancel_lock)
+					lock_valid <= 0;
+				if (w_valid_lock_request)
+					lock_valid <= 1;
+			end
+			// }}}
+
+			// lock_start, lock_end, lock_len, lock_size
+			// {{{
+			always @(posedge S_AXI_ACLK)
+			if (w_valid_lock_request)
+			begin
+				lock_start <= S_AXI_ARADDR[C_S_AXI_ADDR_WIDTH-1:LSB];
+				// Verilator lint_off WIDTH
+				lock_end <= S_AXI_ARADDR[C_S_AXI_ADDR_WIDTH-1:LSB]
+					+ ((S_AXI_ARBURST == 2'b00) ? 4'h0 : S_AXI_ARLEN[3:0]);
+				// Verilator lint_on  WIDTH
+				lock_len   <= S_AXI_ARLEN[3:0];
+				lock_size  <= S_AXI_ARSIZE;
+				lock_burst <= S_AXI_ARBURST;
+			end
+			// }}}
+
+			// w_write_lock_valid
+			// {{{
+			always @(*)
+			begin
+				w_write_lock_valid = returned_lock_valid;
+				if (!m_awvalid || !m_awready || !m_awlock || !lock_valid)
+					w_write_lock_valid = 0;
+				if (m_awaddr[C_S_AXI_ADDR_WIDTH-1:LSB] != lock_start)
+					w_write_lock_valid = 0;
+				if (m_awid[IW-1:0] != gk[IW-1:0])
+					w_write_lock_valid = 0;
+				if (m_awlen[3:0] != lock_len)	// MAX transfer size is 16 beats
+					w_write_lock_valid = 0;
+				if (m_awburst != 2'b01 && lock_len != 0)
+					w_write_lock_valid = 0;
+				if (m_awsize != lock_size)
+					w_write_lock_valid = 0;
+			end
+			// }}}
+
+			assign	write_lock_valid_per_id[gk]= w_write_lock_valid;
+		// }}}
+		end
+
+		assign	write_lock_valid = |write_lock_valid_per_id;
+		// }}}
+	end else begin : NO_LOCKING
+		// {{{
+
+		assign	write_lock_valid = 1'b0;
+		// Verilator lint_off UNUSED
+		wire	unused_lock;
+		assign	unused_lock = &{ 1'b0, S_AXI_ARLOCK, S_AXI_AWLOCK };
+		// Verilator lint_on  UNUSED
+		// }}}
+	end endgenerate
+	// }}}
+
+	// Make Verilator happy
+	// {{{
+	// Verilator lint_off UNUSED
+	wire	unused;
+	assign	unused = &{ 1'b0, S_AXI_AWCACHE, S_AXI_AWPROT, S_AXI_AWQOS,
+		S_AXI_ARCACHE, S_AXI_ARPROT, S_AXI_ARQOS };
+	// Verilator lint_on  UNUSED
+	// }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal properties
+// {{{
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+	//
+	// The following properties are only some of the properties used
+	// to verify this core
+	//	
+	// Local (formal) register declarations
+	// {{{
+	reg	f_past_valid;
+	initial	f_past_valid = 0;
+	always @(posedge S_AXI_ACLK)
+		f_past_valid <= 1;
+
+	always @(*)
+	if (!f_past_valid)
+		assume(!S_AXI_ARESETN);
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// AXI slave properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	faxi_slave	#(
+		// {{{
+		.C_AXI_ID_WIDTH(C_S_AXI_ID_WIDTH),
+		.C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH),
+		.C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH))
+		// ...
+		// }}}
+	f_slave(
+		// {{{
+		.i_clk(S_AXI_ACLK),
+		.i_axi_reset_n(S_AXI_ARESETN),
+		//
+		// Address write channel
+		// {{{
+		.i_axi_awvalid(m_awvalid),
+		.i_axi_awready(m_awready),
+		.i_axi_awid(   m_awid),
+		.i_axi_awaddr( m_awaddr),
+		.i_axi_awlen(  m_awlen),
+		.i_axi_awsize( m_awsize),
+		.i_axi_awburst(m_awburst),
+		.i_axi_awlock( m_awlock),
+		.i_axi_awcache(4'h0),
+		.i_axi_awprot( 3'h0),
+		.i_axi_awqos(  4'h0),
+		// }}}
+		// Write Data Channel
+		// {{{
+		// Write Data
+		.i_axi_wdata(S_AXI_WDATA),
+		.i_axi_wstrb(S_AXI_WSTRB),
+		.i_axi_wlast(S_AXI_WLAST),
+		.i_axi_wvalid(S_AXI_WVALID),
+		.i_axi_wready(S_AXI_WREADY),
+		// }}}
+		// Write response
+		// {{{
+		.i_axi_bvalid(S_AXI_BVALID),
+		.i_axi_bready(S_AXI_BREADY),
+		.i_axi_bid(   S_AXI_BID),
+		.i_axi_bresp( S_AXI_BRESP),
+		// }}}
+		// Read address channel
+		// {{{
+		.i_axi_arvalid(S_AXI_ARVALID),
+		.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),
+		// }}}
+		// Read data return channel
+		// {{{
+		.i_axi_rvalid(S_AXI_RVALID),
+		.i_axi_rready(S_AXI_RREADY),
+		.i_axi_rid(S_AXI_RID),
+		.i_axi_rdata(S_AXI_RDATA),
+		.i_axi_rresp(S_AXI_RRESP),
+		.i_axi_rlast(S_AXI_RLAST),
+		// }}}
+		//
+		// ...
+		// }}}
+	);
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Write induction properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+
+	//
+	// ...
+	//
+
+	always @(*)
+	if (r_bvalid)
+		assert(S_AXI_BVALID);
+
+	always @(*)
+		assert(axi_awready == (!S_AXI_WREADY&& !r_bvalid));
+
+	always @(*)
+	if (axi_awready)
+		assert(!S_AXI_WREADY);
+
+
+	//
+	// ...
+	//
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Read induction properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+
+	//
+	// ...
+	//
+
+
+	always @(posedge S_AXI_ACLK)
+	if (f_past_valid && axi_rlen == 0)
+		assert(S_AXI_ARREADY);
+
+	always @(posedge S_AXI_ACLK)
+		assert(axi_rlen <= 256);
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Lowpower checking
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	always @(*)
+	if (OPT_LOWPOWER && S_AXI_ARESETN)
+	begin
+		if (!rskd_valid)
+			assert(!rskd_lock);
+		if (faxi_awr_nbursts == 0)
+		begin
+			assert(S_AXI_BRESP == 2'b00);
+			// assert(S_AXI_BID == 0);
+		end
+
+		if (!S_AXI_RVALID)
+		begin
+			assert(S_AXI_RID   == 0);
+			assert(S_AXI_RDATA == 0);
+			assert(S_AXI_RRESP == 2'b00);
+		end
+
+		if (!o_we)
+		begin
+			assert(o_waddr == 0);
+			assert(o_wdata == 0);
+			assert(o_wstrb == 0);
+		end
+	end
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Contract checking
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	// ...
+	//
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Cover properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	reg	f_wr_cvr_valid, f_rd_cvr_valid;
+	reg	[4:0]	f_dbl_rd_count, f_dbl_wr_count;
+
+	initial	f_wr_cvr_valid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		f_wr_cvr_valid <= 0;
+	else if (S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN > 4)
+		f_wr_cvr_valid <= 1;
+
+	always @(*)
+		cover(!S_AXI_BVALID && axi_awready && !m_awvalid
+			&& f_wr_cvr_valid /* && ... */));
+
+	initial	f_rd_cvr_valid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		f_rd_cvr_valid <= 0;
+	else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN > 4)
+		f_rd_cvr_valid <= 1;
+
+	always @(*)
+		cover(S_AXI_ARREADY && f_rd_cvr_valid /* && ... */);
+
+	//
+	// Generate cover statements associated with multiple successive bursts
+	//
+	// These will be useful for demonstrating the throughput of the core.
+	//
+
+	initial	f_dbl_wr_count = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		f_dbl_wr_count = 0;
+	else if (S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN == 3)
+	begin
+		if (!(&f_dbl_wr_count))
+			f_dbl_wr_count <= f_dbl_wr_count + 1;
+	end
+
+	always @(*)
+		cover(S_AXI_ARESETN && (f_dbl_wr_count > 1));	//!
+
+	always @(*)
+		cover(S_AXI_ARESETN && (f_dbl_wr_count > 3));	//!
+
+	always @(*)
+		cover(S_AXI_ARESETN && (f_dbl_wr_count > 3) && !m_awvalid
+			&&(!S_AXI_AWVALID && !S_AXI_WVALID && !S_AXI_BVALID)
+			&& (faxi_awr_nbursts == 0)
+			&& (faxi_wr_pending == 0));
+
+	initial	f_dbl_rd_count = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		f_dbl_rd_count = 0;
+	else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN == 3)
+	begin
+		if (!(&f_dbl_rd_count))
+			f_dbl_rd_count <= f_dbl_rd_count + 1;
+	end
+
+	always @(*)
+		cover(!S_AXI_ARESETN && (f_dbl_rd_count > 3)
+			/* && ... */
+			&& !S_AXI_ARVALID && !S_AXI_RVALID);
+
+	generate if (OPT_LOCK)
+	begin
+		always @(*)
+			cover(S_AXI_ARESETN && S_AXI_BVALID && S_AXI_BREADY
+				&& S_AXI_BRESP == 2'b01);
+	end endgenerate
+
+`ifdef	VERIFIC
+	cover property (@(posedge S_AXI_ACLK)
+		disable iff (!S_AXI_ARESETN)
+		// Accept a burst request for 4 beats
+		(S_AXI_ARVALID && S_AXI_ARREADY && (S_AXI_ARLEN == 3)
+			##1 S_AXI_ARVALID [*3]) [*3]
+		##1 1 [*0:12]
+		// The return to idle
+		##1 (!S_AXI_ARVALID && !o_rd && !rskd_valid && !S_AXI_RVALID)
+		);
+`endif
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// "Careless" assumptions
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// }}}
+`endif
+// }}}
+endmodule
+`ifndef	YOSYS
+`default_nettype wire
+`endif