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

 ////////////////////////////////////////////////////////////////////////////////
 //
 // Filename: 	axi3reorder.v
 // {{{
 // Project:	WB2AXIPSP: bus bridges and other odds and ends
 //
 // Purpose:	One of the challenges of working with AXI3 are the (potentially)
 //		out of order writes.  This modules is designed to re-order write
 //	beats back into the proper order given by the AW* channel.  Once done,
 //	write beats will always be contiguous--only changing ID's after WLAST.
 //	Indeed, once done, the WID field can be properly removed and ignored.
 //	it's left within for forms sake, but isn't required.
 //
 // Algorithms:
 //	The design currently contains one of three reordering algorithms.
 //
 //	MTHD_NONE	Is a basic pass-through.  This would be appropriate
 //			for AXI3 streams that are known to be in order already.
 //
 //	MTHD_SHIFT_REGISTER	Uses a shift-register based "FIFO".  (Not block
 //				RAM)  All write data goes into this FIFO.  Items
 //			are read from this FIFO out of order as required for
 //			the given ID.  When any item is read from the middle,
 //			the shift register back around the item read.
 //
 //			This is a compromise implementation that uses less
 //			logic than the PER/ID FIFOS, while still allowing some
 //			amount of reordering to take place.
 //
 //	MTHD_PERID_FIFOS	Uses an explicit FIFO for each ID.  Data come
 //				into the core and go directly into the FIFO's.
 //			Data are read out of the FIFOs in write-address order
 //			until WLAST, where the write address may (potentially)
 //			change.
 //
 //			For a small number of IDs, this solution should be
 //			*complete*, and lacking nothing.  (Unless you fill the
 //			write data FIFO's while needing data from another ID ..)
 //
 // Implementation notes:
 //	This module is intended to be used side by side with other AW* channel
 //	processing, and following an (external) AW* skidbuffer.  For this
 //	reason, it doesn't use an AW skid buffer, nor does it output AW*
 //	information.  External AWREADY handling should therefore be:
 //
 //		master_awskid_read = reorder_awready && any_other_awready;
 //
 //	going into a skid buffer, with the proper AWREADY being the upstream
 //	skidbuffer's AWREADY output.
 //
 // Expected performance:
 //	One beat per clock, all methods.
 //
 // Status:
 //	This module passes both a Verilator lint check and a 15-20 step formal
 //	bounded model check.
 //
 // Creator:	Dan Gisselquist, Ph.D.
 //		Gisselquist Technology, LLC
 //
 ////////////////////////////////////////////////////////////////////////////////
 // }}}
 // Copyright (C) 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	axi3reorder #(
 		// {{{
 		parameter	C_AXI_ID_WIDTH = 4,
 		parameter	C_AXI_DATA_WIDTH = 32,
 		parameter	LGAWFIFO = 3,	// # packets we can handle
 		parameter	LGWFIFO = 4,	// Full size of an AXI burst
 		parameter	OPT_METHOD = 0,
 		parameter [0:0]	OPT_LOWPOWER = 0,
 		parameter [0:0]	OPT_LOW_LATENCY = 0,
 		localparam	MTHD_NONE = 0,
 		localparam	MTHD_SHIFT_REGISTER = 1,
 		localparam	MTHD_PERID_FIFOS = 2,
 		localparam	IW = C_AXI_ID_WIDTH,
 		localparam	DW = C_AXI_DATA_WIDTH,
 		parameter	NUM_FIFOS = (1<<IW)
 		// }}}
 	) (
 		// {{{
 		input	wire	S_AXI_ACLK,
 		input	wire	S_AXI_ARESETN,
 		// AXI3 (partial) slave interface
 		// {{{
 		input	wire			S_AXI3_AWVALID,
 		output	wire			S_AXI3_AWREADY,
 		input	wire	[IW-1:0]	S_AXI3_AWID,
 		// input	wire [AW-1:0]	S_AXI3_AWADDR,
 		// input	wire	[3:0]	S_AXI3_AWLEN,
 		// input	wire	[2:0]	S_AXI3_AWSIZE,
 		// input	wire	[1:0]	S_AXI3_AWBURST,
 		// input	wire	[1:0]	S_AXI3_AWLOCK,
 		// input	wire	[3:0]	S_AXI3_AWCACHE,
 		// input	wire	[2:0]	S_AXI3_AWPROT,
 		// input	wire	[3:0]	S_AXI3_AWQOS,
 		//
 		input	wire			S_AXI3_WVALID,
 		output	wire			S_AXI3_WREADY,
 		input	wire	[IW-1:0]	S_AXI3_WID,
 		input	wire	[DW-1:0]	S_AXI3_WDATA,
 		input	wire	[DW/8-1:0]	S_AXI3_WSTRB,
 		input	wire			S_AXI3_WLAST,
 		// }}}
 		// Reordered write data port.  WID may now be discarded.
 		// {{{
 		output	reg			M_AXI_WVALID,
 		input	wire			M_AXI_WREADY,
 		output	reg	[IW-1:0]	M_AXI_WID,
 		output	reg	[DW-1:0]	M_AXI_WDATA,
 		output	reg	[DW/8-1:0]	M_AXI_WSTRB,
 		output	reg			M_AXI_WLAST
 		// }}}
 		// }}}
 	);

 	// Register declarations
 	// {{{
 	wire			awfifo_full, awfifo_empty;
 	reg			read_awid_fifo;
 	wire	[IW-1:0]	awfifo_id;
 	wire	[LGAWFIFO:0]	awfifo_fill;

 	genvar	gk;
 	reg			read_beat_fifo;

 	reg			cid_valid;
 	reg	[IW-1:0]	current_id;

 	// }}}
 	////////////////////////////////////////////////////////////////////////
 	//
 	// Write address ID's go to an address ID FIFO
 	// {{{
 	////////////////////////////////////////////////////////////////////////
 	//
 	generate if (OPT_METHOD == MTHD_NONE)
 	begin : IGNORE_AW_CHANNEL
 		// No write address ID's to keep track of
 		// {{{
 		// These values are irrelevant.  They are placeholders, put here
 		// to keep the linter from complaining.

 		assign	awfifo_id = S_AXI3_AWID;
 		assign	S_AXI3_AWREADY = 1'b1;
 		assign	awfifo_full  = 0;
 		assign	awfifo_fill  = 0;
 		assign	awfifo_empty = !S_AXI3_AWVALID;
 		assign	cid_valid = S_AXI3_AWVALID;
 		always @(*)
 			cid_valid = S_AXI3_AWVALID;
 		always @(*)
 			current_id= S_AXI3_AWID;
 		always @(*)
 			read_awid_fifo = 0;

 		// Verilator lint_off UNUSED
 		wire	none_aw_unused;
 		assign	none_aw_unused = &{ 1'b0, awfifo_full, awfifo_fill,
 				awfifo_empty, read_awid_fifo, awfifo_id };
 		// }}}
 	end else begin : AWFIFO
 		////////////////////////////////////////////////////////////////
 		//
 		// Write address ID FIFO
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		//
 		sfifo #(
 			// {{{
 			.BW(IW),
 			.LGFLEN(LGAWFIFO),
 			.OPT_READ_ON_EMPTY(OPT_LOW_LATENCY)
 			// }}}
 		) awidfifo(
 			// {{{
 			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
 			.i_wr(S_AXI3_AWVALID && S_AXI3_AWREADY),
 				.i_data(S_AXI3_AWID),
 				.o_full(awfifo_full),
 				.o_fill(awfifo_fill),
 				.i_rd(read_awid_fifo),
 				.o_data( awfifo_id ),
 				.o_empty(awfifo_empty)
 			// }}}
 		);

 		assign	S_AXI3_AWREADY = !awfifo_full;
 		// }}}
 		////////////////////////////////////////////////////////////////
 		//
 		// Current ID -- what ID shall we output next?
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		// The current ID is given by the write address channel

 		initial	cid_valid = 0;
 		always @(posedge S_AXI_ACLK)
 		if (!S_AXI_ARESETN)
 			cid_valid <= 1'b0;
 		else if (read_awid_fifo)
 			cid_valid  <= !awfifo_empty;

 		// The current ID is given by the write address channel
 		always @(posedge S_AXI_ACLK)
 		if (read_awid_fifo)
 			current_id <= awfifo_id;

 		// }}}
 	end endgenerate
 	// }}}
 	////////////////////////////////////////////////////////////////////////
 	//
 	// Write data channel processing and reordering
 	// {{{
 	////////////////////////////////////////////////////////////////////////
 	//
 	//
 	generate if (OPT_METHOD == MTHD_NONE)
 	begin : COPY_SW_TO_MW // Copy S_AXI3_W* values to M_AXIW*
 		// {{{
 		// {{{
 		always @(*)
 		begin
 			M_AXI_WVALID = S_AXI3_WVALID;
 			M_AXI_WID    = S_AXI3_WID;
 			M_AXI_WDATA  = S_AXI3_WDATA;
 			M_AXI_WSTRB  = S_AXI3_WSTRB;
 			M_AXI_WLAST  = S_AXI3_WLAST;

 			read_beat_fifo = 0;
 		end
 		// }}}

 		assign	S_AXI3_WREADY = M_AXI_WREADY;

 		// Keep Verilator happy
 		// Verilator lint_off UNUSED
 		wire	none_unused;
 		assign	none_unused = &{ 1'b0, S_AXI_ACLK, S_AXI_ARESETN,
 				current_id, cid_valid, read_beat_fifo };
 		// Verilator lint_on  UNUSED
 		// }}}
 	end else if (OPT_METHOD == MTHD_SHIFT_REGISTER)
 	begin : SHIFT_REGISTER
 		// {{{

 		////////////////////////////////////////////////////////////////
 		//
 		// Local declarations
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		//
 		localparam	NSREG = (1<<LGWFIFO);
 		reg	[NSREG-1:0]	sr_advance;
 		reg	[NSREG-1:0]	sr_write;
 		reg	[NSREG-1:0]	sr_valid;
 		reg	[IW-1:0]	sr_id	[0:NSREG];
 		reg	[DW-1:0]	sr_data	[0:NSREG];
 		reg	[DW/8-1:0]	sr_strb	[0:NSREG];
 		reg	[NSREG-1:0]	sr_last;

 		integer	ik;
 		// }}}
 		////////////////////////////////////////////////////////////////
 		//
 		// Per-register-station logic
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		//

 		for (gk = 0; gk<NSREG; gk=gk+1)
 		begin

 			// sr_advance
 			// {{{
 			// Do we copy from the next station into this one or no?
 			always @(*)
 			begin
 				sr_advance[gk] = 0;
 				if ((gk > 0)&&(sr_advance[gk-1]))
 					sr_advance[gk] = 1;
 				if ((!M_AXI_WVALID || M_AXI_WREADY)
 					&& cid_valid && current_id == sr_id[gk])
 					sr_advance[gk] = 1;
 				if (!sr_valid[gk])
 					sr_advance[gk] = 0;
 			end
 			// }}}

 			// sw_write
 			// {{{
 			// Do we write new data into this station?
 			always @(*)
 			begin
 				sr_write[gk] = S_AXI3_WVALID && S_AXI3_WREADY;
 				if (sr_valid[gk] && (!sr_advance[gk]
 						||(gk < NSREG-1 && sr_valid[gk+1])))
 					sr_write[gk] = 0;
 				if (gk > 0 && (!sr_valid[gk-1]
 					|| (sr_advance[gk-1] && !sr_valid[gk])))
 					sr_write[gk] = 0;
 			end
 			// }}}

 			// sr_valid
 			// {{{
 			initial	sr_valid[gk] = 0;
 			always @(posedge S_AXI_ACLK)
 			if (!S_AXI_ARESETN)
 				sr_valid[gk] <= 0;
 			else if (sr_write[gk])
 				sr_valid[gk] <= 1;
 			else if (sr_advance[gk] && gk<NSREG-1)
 				sr_valid[gk] <= sr_valid[gk+1];
 			else if (sr_advance[gk])
 				sr_valid[gk] <= 0;
 			// }}}

 			// sr_id, sr_data, sr_strb, sr_last
 			// {{{
 			always @(posedge S_AXI_ACLK)
 			if (OPT_LOWPOWER && !S_AXI_ARESETN)
 			begin
 				sr_id[gk]   <= 0;
 				sr_data[gk] <= 0;
 				sr_strb[gk] <= 0;
 				sr_last[gk] <= 0;
 			end else if (sr_write[gk])
 			begin
 				sr_id[gk]   <= S_AXI3_WID;
 				sr_data[gk] <= S_AXI3_WDATA;
 				sr_strb[gk] <= S_AXI3_WSTRB;
 				sr_last[gk] <= S_AXI3_WLAST;
 			end else if ((gk < NSREG-1) && sr_advance[gk])
 			begin
 				sr_id[gk]   <= sr_id[gk+1];
 				sr_data[gk] <= sr_data[gk+1];
 				sr_strb[gk] <= sr_strb[gk+1];
 				sr_last[gk] <= sr_last[gk+1];

 				if (OPT_LOWPOWER && gk < NSREG-1 && !sr_valid[gk+1])
 				begin
 					// If we are running in low power,
 					// Keep every unused register == 0
 					sr_id[gk]   <= 0;
 					sr_data[gk] <= 0;
 					sr_strb[gk] <= 0;
 					sr_last[gk] <= 0;
 				end
 			end else if ((!OPT_LOWPOWER && !sr_valid[gk])
 				|| sr_write[gk])
 			begin
 				sr_id[gk]   <= S_AXI3_WID;
 				sr_data[gk] <= S_AXI3_WDATA;
 				sr_strb[gk] <= S_AXI3_WSTRB;
 				sr_last[gk] <= S_AXI3_WLAST;
 			end
 			// }}}
 		end
 		// }}}
 		////////////////////////////////////////////////////////////////
 		//
 		// Pick a register location to output
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		reg			known_next;
 		reg	[LGWFIFO-1:0]	sr_next;
 		always @(*)
 		begin
 			known_next = 0;
 			sr_next = -1;
 			for(ik=0; ik<NSREG; ik=ik+1)
 			if (!known_next && current_id == sr_id[ik])
 			begin
 				sr_next = ik[LGWFIFO-1:0];
 				known_next = sr_valid[ik];
 			end

 			if (!cid_valid)
 				known_next = 0;
 		end

 		assign	S_AXI3_WREADY = !sr_valid[NSREG-1];
 		// }}}
 		////////////////////////////////////////////////////////////////
 		//
 		//
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		//
 		always @(*)
 			read_awid_fifo = (!M_AXI_WVALID || M_AXI_WREADY)
 				&& (!cid_valid
 				|| (known_next && sr_last[sr_next]));

 		always @(*)
 			read_beat_fifo = (!M_AXI_WVALID || M_AXI_WREADY)
 				&&(known_next);

 		initial	M_AXI_WVALID = 0;
 		always @(posedge S_AXI_ACLK)
 		if (!S_AXI_ARESETN)
 			M_AXI_WVALID <= 0;
 		else if (!M_AXI_WVALID || M_AXI_WREADY)
 			M_AXI_WVALID <= known_next;

 		initial	M_AXI_WID   = 0;
 		initial	M_AXI_WDATA = 0;
 		initial	M_AXI_WSTRB = 0;
 		initial	M_AXI_WLAST = 0;
 		always @(posedge S_AXI_ACLK)
 		if (OPT_LOWPOWER && !S_AXI_ARESETN)
 		begin
 			// {{{
 			M_AXI_WID   <= 0;
 			M_AXI_WDATA <= 0;
 			M_AXI_WSTRB <= 0;
 			M_AXI_WLAST <= 0;
 			// }}}
 		end else if (!M_AXI_WVALID || M_AXI_WREADY)
 		begin
 			if (OPT_LOWPOWER && !known_next)
 			begin
 				// {{{
 				M_AXI_WID <= 0;
 				M_AXI_WDATA <= 0;
 				M_AXI_WSTRB <= 0;
 				M_AXI_WLAST <= 0;
 				// }}}
 			end else begin
 				// {{{
 				M_AXI_WID <= current_id;
 				// Verilator lint_off WIDTH
 				M_AXI_WDATA <= sr_data[sr_next];
 				M_AXI_WSTRB <= sr_strb[sr_next];
 				M_AXI_WLAST <= sr_last[sr_next];
 				// Verilator lint_on  WIDTH
 				// }}}
 			end
 		end
 		// }}}
 		// Verilator lint_off UNUSED
 		wire	unused_sreg;
 		assign	unused_sreg = &{ 1'b0, read_beat_fifo };
 		// Verilator lint_on  UNUSED
 `ifdef	FORMAL
 		always @(*)
 		if (S_AXI3_WVALID && S_AXI3_WREADY)
 			assert($onehot(sr_write));
 		else if (S_AXI_ARESETN)
 			assert(sr_write == 0);

 		always @(*)
 			assert(((sr_write << 1) & sr_valid) == 0);

 		reg	cvr_sreg_full;

 		initial	cvr_sreg_full = 0;
 		always @(posedge S_AXI_ACLK)
 		if (!S_AXI_ARESETN)
 			cvr_sreg_full <= 0;
 		else if (!S_AXI3_WREADY)
 			cvr_sreg_full <= 1;

 		always @(*)
 			cover(cvr_sreg_full && sr_valid == 0);

 `endif
 		// }}}
 	end else if (OPT_METHOD == MTHD_PERID_FIFOS)
 	begin : MULTIPLE_FIFOS
 		// {{{
 		wire	[NUM_FIFOS-1:0]	wbfifo_full, wbfifo_empty, wbfifo_last;
 		// wire	[IW-1:0]	wbfifo_id	[0:NUM_FIFOS-1];
 		wire	[DW-1:0]	wbfifo_data	[0:NUM_FIFOS-1];
 		wire	[DW/8-1:0]	wbfifo_strb	[0:NUM_FIFOS-1];

 		////////////////////////////////////////////////////////////////
 		//
 		// The write beat FIFO
 		////////////////////////////////////////////////////////////////
 		// {{{
 		//
 		// Every write beat goes into a separate FIFO based on its ID
 		//
 		for (gk=0; gk < NUM_FIFOS; gk=gk+1)
 		begin
 		// {{{
 			wire	[LGWFIFO:0]	wbfifo_fill;

 			sfifo #(
 				.BW(DW+(DW/8)+1),
 				.LGFLEN(LGWFIFO),
 				.OPT_READ_ON_EMPTY(OPT_LOW_LATENCY)
 			) write_beat_fifo (
 				.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
 				.i_wr(S_AXI3_WVALID && S_AXI3_WREADY && S_AXI3_WID == gk),
 				.i_data({ S_AXI3_WDATA, S_AXI3_WSTRB,
 					S_AXI3_WLAST }),
 				.o_full(wbfifo_full[gk]), .o_fill(wbfifo_fill),
 				.i_rd(read_beat_fifo && current_id == gk),
 				.o_data({ wbfifo_data[gk],
 					wbfifo_strb[gk], wbfifo_last[gk] }),
 				.o_empty(wbfifo_empty[gk])
 			);

 			// Verilator lint_off UNUSED
 			wire	unused;
 			assign	unused = &{ 1'b0, wbfifo_fill };
 			// Verilator lint_on  UNUSED
 			// }}}
 		end

 		assign	S_AXI3_WREADY = !wbfifo_full[S_AXI3_WID];
 		// }}}
 		////////////////////////////////////////////////////////////////
 		//
 		// Outgoing write data channel
 		// {{{
 		////////////////////////////////////////////////////////////////
 		//
 		//

 		always @(*)
 			read_awid_fifo = (!M_AXI_WVALID || M_AXI_WREADY)
 				&& (!cid_valid
 				|| (read_beat_fifo && wbfifo_last[current_id]));
 		// Write packets associated with the current ID can move forward
 		always @(*)
 			read_beat_fifo = (!M_AXI_WVALID || M_AXI_WREADY)
 				&&(cid_valid)&&(!wbfifo_empty[current_id]);

 		initial	M_AXI_WVALID = 0;
 		always @(posedge S_AXI_ACLK)
 		if (!S_AXI_ARESETN)
 			M_AXI_WVALID <= 0;
 		else if (!M_AXI_WVALID || M_AXI_WREADY)
 			M_AXI_WVALID <= read_beat_fifo;

 		initial	M_AXI_WID   = 0;
 		initial	M_AXI_WDATA = 0;
 		initial	M_AXI_WSTRB = 0;
 		initial	M_AXI_WLAST = 0;
 		always @(posedge S_AXI_ACLK)
 		if (OPT_LOWPOWER && !S_AXI_ARESETN)
 		begin
 			// {{{
 			M_AXI_WID   <= 0;
 			M_AXI_WDATA <= 0;
 			M_AXI_WSTRB <= 0;
 			M_AXI_WLAST <= 0;
 			// }}}
 		end else if (!M_AXI_WVALID || M_AXI_WREADY)
 		begin
 			// {{{
 			M_AXI_WID <= current_id;
 			M_AXI_WDATA <= wbfifo_data[current_id];
 			M_AXI_WSTRB <= wbfifo_strb[current_id];
 			M_AXI_WLAST <= wbfifo_last[current_id];

 			if (OPT_LOWPOWER && !read_beat_fifo)
 			begin
 				// {{{
 				M_AXI_WID   <= 0;
 				M_AXI_WDATA <= 0;
 				M_AXI_WSTRB <= 0;
 				M_AXI_WLAST <= 0;
 				// }}}
 			end
 			// }}}
 		end
 		// }}}
 		// }}}
 	end endgenerate
 	// }}}
 	// Make Verilator happy
 	// {{{
 	// Verilator lint_off UNUSED
 	wire	unused;
 	assign	unused = &{ 1'b0, awfifo_fill };
 	// Verilator lint_on  UNUSED
 	// }}}
 ////////////////////////////////////////////////////////////////////////////////
 ////////////////////////////////////////////////////////////////////////////////
 ////////////////////////////////////////////////////////////////////////////////
 //
 // Formal properties
 // {{{
 ////////////////////////////////////////////////////////////////////////////////
 ////////////////////////////////////////////////////////////////////////////////
 ////////////////////////////////////////////////////////////////////////////////
 `ifdef	FORMAL
 	reg				f_past_valid;
 	reg	[LGAWFIFO+LGWFIFO-1:0]	f_awid_count;
 	(* anyconst *) reg	[IW-1:0]	f_const_id;

 	initial	f_past_valid = 0;
 	always @(posedge S_AXI_ACLK)
 		f_past_valid <= 1;

 	always @(*)
 	if (!f_past_valid)
 		assume(!S_AXI_ARESETN);

 	always @(posedge S_AXI_ACLK)
 	if (!f_past_valid || $past(!S_AXI_ARESETN))
 	begin
 		assume(!S_AXI3_AWVALID);
 		assume(!S_AXI3_WVALID);

 		assume(!M_AXI_WVALID);
 	end else begin
 		if ($past(S_AXI3_AWVALID && !S_AXI3_AWREADY))
 		begin
 			assume(S_AXI3_AWVALID);
 			assume($stable(S_AXI3_AWID));
 		end

 		if ($past(S_AXI3_WVALID && !S_AXI3_WREADY))
 		begin
 			assume(S_AXI3_WVALID);
 			assume($stable(S_AXI3_WID));
 			assume($stable(S_AXI3_WDATA));
 			assume($stable(S_AXI3_WSTRB));
 			assume($stable(S_AXI3_WLAST));
 		end

 		if ($past(M_AXI_WVALID && !M_AXI_WREADY))
 		begin
 			assert(M_AXI_WVALID);
 			assert($stable(M_AXI_WID));
 			assert($stable(M_AXI_WDATA));
 			assert($stable(M_AXI_WSTRB));
 			assert($stable(M_AXI_WLAST));
 		end
 	end

 	generate if (OPT_METHOD != MTHD_NONE)
 	begin : F_FIFO_CHECK
 		wire	[LGWFIFO:0]	f_ckfifo_fill;
 		wire	[LGWFIFO:0]	f_ckfifo_full, f_ckfifo_empty;
 		wire	[IW-1:0]	f_ckfifo_id;
 		wire	[DW-1:0]	f_ckfifo_data;
 		wire	[DW/8-1:0]	f_ckfifo_strb;
 		wire			f_ckfifo_last;

 		sfifo #(
 			.BW(IW + DW + (DW/8) + 1),
 			.LGFLEN(LGWFIFO),
 			.OPT_READ_ON_EMPTY(OPT_LOW_LATENCY)
 		) f_checkfifo (
 			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
 			.i_wr(S_AXI3_WVALID && S_AXI3_WREADY
 							&& S_AXI3_WID == f_const_id),
 			.i_data({ S_AXI3_WID, S_AXI3_WDATA, S_AXI3_WSTRB, S_AXI3_WLAST }),
 			.o_full(f_ckfifo_full), .o_fill(f_ckfifo_fill),
 			.i_rd(M_AXI_WVALID && M_AXI_WREADY
 						&& M_AXI_WID == f_const_id),
 			.o_data({ f_ckfifo_id, f_ckfifo_data, f_ckfifo_strb,
 					f_ckfifo_last }),
 			.o_empty(f_ckfifo_empty)
 		);

 		always @(*)
 		if (S_AXI_ARESETN && M_AXI_WVALID && M_AXI_WID == f_const_id)
 		begin
 			assert(!f_ckfifo_empty);
 			assert(f_ckfifo_id   == M_AXI_WID);
 			assert(f_ckfifo_data == M_AXI_WDATA);
 			assert(f_ckfifo_strb == M_AXI_WSTRB);
 			assert(f_ckfifo_last == M_AXI_WLAST);
 		end
 	end endgenerate

 	always @(posedge S_AXI_ACLK)
 	if (!S_AXI_ARESETN)
 		f_awid_count = 0;
 	else case({S_AXI3_AWVALID&& S_AXI3_AWREADY && S_AXI3_AWID == f_const_id,
 			M_AXI_WVALID && M_AXI_WREADY && M_AXI_WLAST
 			&& M_AXI_WID == f_const_id })
 	2'b01: f_awid_count <= f_awid_count - 1;
 	2'b10: f_awid_count <= f_awid_count + 1;
 	default begin end
 	endcase

 	always @(*)
 	if (M_AXI_WVALID && M_AXI_WID == f_const_id)
 		assert(f_awid_count > 0);

 	generate if (OPT_LOWPOWER)
 	begin : F_LOWPOWER_CHECK
 		always @(*)
 		if (!S_AXI3_AWVALID)
 			assume(S_AXI3_AWID == 0);

 		always @(*)
 		if (!S_AXI3_WVALID)
 		begin
 			assume(S_AXI3_WID   == 0);
 			assume(S_AXI3_WDATA == 0);
 			assume(S_AXI3_WSTRB == 0);
 			assume(S_AXI3_WLAST == 0);
 		end

 		always @(*)
 		if (!M_AXI_WVALID)
 		begin
 			assert(M_AXI_WID   == 0);
 			assert(M_AXI_WDATA == 0);
 			assert(M_AXI_WSTRB == 0);
 			assert(M_AXI_WLAST == 0);
 		end

 	end endgenerate

 `endif
 	// }}}
 endmodule
	////////////////////////////////////////////////////////////////////////////////
	//
	// Filename: axi3reorder.v
	// {{{
	// Project: WB2AXIPSP: bus bridges and other odds and ends
	//
	// Purpose: One of the challenges of working with AXI3 are the (potentially)
	// out of order writes. This modules is designed to re-order write
	// beats back into the proper order given by the AW* channel. Once done,
	// write beats will always be contiguous--only changing ID's after WLAST.
	// Indeed, once done, the WID field can be properly removed and ignored.
	// it's left within for forms sake, but isn't required.
	//
	// Algorithms:
	// The design currently contains one of three reordering algorithms.
	//
	// MTHD_NONE Is a basic pass-through. This would be appropriate
	// for AXI3 streams that are known to be in order already.
	//
	// MTHD_SHIFT_REGISTER Uses a shift-register based "FIFO". (Not block
	// RAM) All write data goes into this FIFO. Items
	// are read from this FIFO out of order as required for
	// the given ID. When any item is read from the middle,
	// the shift register back around the item read.
	//
	// This is a compromise implementation that uses less
	// logic than the PER/ID FIFOS, while still allowing some
	// amount of reordering to take place.
	//
	// MTHD_PERID_FIFOS Uses an explicit FIFO for each ID. Data come
	// into the core and go directly into the FIFO's.
	// Data are read out of the FIFOs in write-address order
	// until WLAST, where the write address may (potentially)
	// change.
	//
	// For a small number of IDs, this solution should be
	// complete, and lacking nothing. (Unless you fill the
	// write data FIFO's while needing data from another ID ..)
	//
	// Implementation notes:
	// This module is intended to be used side by side with other AW* channel
	// processing, and following an (external) AW* skidbuffer. For this
	// reason, it doesn't use an AW skid buffer, nor does it output AW*
	// information. External AWREADY handling should therefore be:
	//
	// master_awskid_read = reorder_awready && any_other_awready;
	//
	// going into a skid buffer, with the proper AWREADY being the upstream
	// skidbuffer's AWREADY output.
	//
	// Expected performance:
	// One beat per clock, all methods.
	//
	// Status:
	// This module passes both a Verilator lint check and a 15-20 step formal
	// bounded model check.
	//
	// Creator: Dan Gisselquist, Ph.D.
	// Gisselquist Technology, LLC
	//
	////////////////////////////////////////////////////////////////////////////////
	// }}}
	// Copyright (C) 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 axi3reorder #(
	// {{{
	parameter C_AXI_ID_WIDTH = 4,
	parameter C_AXI_DATA_WIDTH = 32,
	parameter LGAWFIFO = 3, // # packets we can handle
	parameter LGWFIFO = 4, // Full size of an AXI burst
	parameter OPT_METHOD = 0,
	parameter [0:0] OPT_LOWPOWER = 0,
	parameter [0:0] OPT_LOW_LATENCY = 0,
	localparam MTHD_NONE = 0,
	localparam MTHD_SHIFT_REGISTER = 1,
	localparam MTHD_PERID_FIFOS = 2,
	localparam IW = C_AXI_ID_WIDTH,
	localparam DW = C_AXI_DATA_WIDTH,
	parameter NUM_FIFOS = (1<<IW)
	// }}}
	) (
	// {{{
	input wire S_AXI_ACLK,
	input wire S_AXI_ARESETN,
	// AXI3 (partial) slave interface
	// {{{
	input wire S_AXI3_AWVALID,
	output wire S_AXI3_AWREADY,
	input wire [IW-1:0] S_AXI3_AWID,
	// input wire [AW-1:0] S_AXI3_AWADDR,
	// input wire [3:0] S_AXI3_AWLEN,
	// input wire [2:0] S_AXI3_AWSIZE,
	// input wire [1:0] S_AXI3_AWBURST,
	// input wire [1:0] S_AXI3_AWLOCK,
	// input wire [3:0] S_AXI3_AWCACHE,
	// input wire [2:0] S_AXI3_AWPROT,
	// input wire [3:0] S_AXI3_AWQOS,
	//
	input wire S_AXI3_WVALID,
	output wire S_AXI3_WREADY,
	input wire [IW-1:0] S_AXI3_WID,
	input wire [DW-1:0] S_AXI3_WDATA,
	input wire [DW/8-1:0] S_AXI3_WSTRB,
	input wire S_AXI3_WLAST,
	// }}}
	// Reordered write data port. WID may now be discarded.
	// {{{
	output reg M_AXI_WVALID,
	input wire M_AXI_WREADY,
	output reg [IW-1:0] M_AXI_WID,
	output reg [DW-1:0] M_AXI_WDATA,
	output reg [DW/8-1:0] M_AXI_WSTRB,
	output reg M_AXI_WLAST
	// }}}
	// }}}
	);

	// Register declarations
	// {{{
	wire awfifo_full, awfifo_empty;
	reg read_awid_fifo;
	wire [IW-1:0] awfifo_id;
	wire [LGAWFIFO:0] awfifo_fill;

	genvar gk;
	reg read_beat_fifo;

	reg cid_valid;
	reg [IW-1:0] current_id;

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Write address ID's go to an address ID FIFO
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	generate if (OPT_METHOD == MTHD_NONE)
	begin : IGNORE_AW_CHANNEL
	// No write address ID's to keep track of
	// {{{
	// These values are irrelevant. They are placeholders, put here
	// to keep the linter from complaining.

	assign awfifo_id = S_AXI3_AWID;
	assign S_AXI3_AWREADY = 1'b1;
	assign awfifo_full = 0;
	assign awfifo_fill = 0;
	assign awfifo_empty = !S_AXI3_AWVALID;
	assign cid_valid = S_AXI3_AWVALID;
	always @(*)
	cid_valid = S_AXI3_AWVALID;
	always @(*)
	current_id= S_AXI3_AWID;
	always @(*)
	read_awid_fifo = 0;

	// Verilator lint_off UNUSED
	wire none_aw_unused;
	assign none_aw_unused = &{ 1'b0, awfifo_full, awfifo_fill,
	awfifo_empty, read_awid_fifo, awfifo_id };
	// }}}
	end else begin : AWFIFO
	////////////////////////////////////////////////////////////////
	//
	// Write address ID FIFO
	// {{{
	////////////////////////////////////////////////////////////////
	//
	//
	sfifo #(
	// {{{
	.BW(IW),
	.LGFLEN(LGAWFIFO),
	.OPT_READ_ON_EMPTY(OPT_LOW_LATENCY)
	// }}}
	) awidfifo(
	// {{{
	.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
	.i_wr(S_AXI3_AWVALID && S_AXI3_AWREADY),
	.i_data(S_AXI3_AWID),
	.o_full(awfifo_full),
	.o_fill(awfifo_fill),
	.i_rd(read_awid_fifo),
	.o_data( awfifo_id ),
	.o_empty(awfifo_empty)
	// }}}
	);

	assign S_AXI3_AWREADY = !awfifo_full;
	// }}}
	////////////////////////////////////////////////////////////////
	//
	// Current ID -- what ID shall we output next?
	// {{{
	////////////////////////////////////////////////////////////////
	//
	// The current ID is given by the write address channel

	initial cid_valid = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	cid_valid <= 1'b0;
	else if (read_awid_fifo)
	cid_valid <= !awfifo_empty;

	// The current ID is given by the write address channel
	always @(posedge S_AXI_ACLK)
	if (read_awid_fifo)
	current_id <= awfifo_id;

	// }}}
	end endgenerate
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Write data channel processing and reordering
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//
	generate if (OPT_METHOD == MTHD_NONE)
	begin : COPY_SW_TO_MW // Copy S_AXI3_W* values to M_AXIW*
	// {{{
	// {{{
	always @(*)
	begin
	M_AXI_WVALID = S_AXI3_WVALID;
	M_AXI_WID = S_AXI3_WID;
	M_AXI_WDATA = S_AXI3_WDATA;
	M_AXI_WSTRB = S_AXI3_WSTRB;
	M_AXI_WLAST = S_AXI3_WLAST;

	read_beat_fifo = 0;
	end
	// }}}

	assign S_AXI3_WREADY = M_AXI_WREADY;

	// Keep Verilator happy
	// Verilator lint_off UNUSED
	wire none_unused;
	assign none_unused = &{ 1'b0, S_AXI_ACLK, S_AXI_ARESETN,
	current_id, cid_valid, read_beat_fifo };
	// Verilator lint_on UNUSED
	// }}}
	end else if (OPT_METHOD == MTHD_SHIFT_REGISTER)
	begin : SHIFT_REGISTER
	// {{{

	////////////////////////////////////////////////////////////////
	//
	// Local declarations
	// {{{
	////////////////////////////////////////////////////////////////
	//
	//
	localparam NSREG = (1<<LGWFIFO);
	reg [NSREG-1:0] sr_advance;
	reg [NSREG-1:0] sr_write;
	reg [NSREG-1:0] sr_valid;
	reg [IW-1:0] sr_id [0:NSREG];
	reg [DW-1:0] sr_data [0:NSREG];
	reg [DW/8-1:0] sr_strb [0:NSREG];
	reg [NSREG-1:0] sr_last;

	integer ik;
	// }}}
	////////////////////////////////////////////////////////////////
	//
	// Per-register-station logic
	// {{{
	////////////////////////////////////////////////////////////////
	//
	//

	for (gk = 0; gk<NSREG; gk=gk+1)
	begin

	// sr_advance
	// {{{
	// Do we copy from the next station into this one or no?
	always @(*)
	begin
	sr_advance[gk] = 0;
	if ((gk > 0)&&(sr_advance[gk-1]))
	sr_advance[gk] = 1;
	if ((!M_AXI_WVALID \|\| M_AXI_WREADY)
	&& cid_valid && current_id == sr_id[gk])
	sr_advance[gk] = 1;
	if (!sr_valid[gk])
	sr_advance[gk] = 0;
	end
	// }}}

	// sw_write
	// {{{
	// Do we write new data into this station?
	always @(*)
	begin
	sr_write[gk] = S_AXI3_WVALID && S_AXI3_WREADY;
	if (sr_valid[gk] && (!sr_advance[gk]
	\|\|(gk < NSREG-1 && sr_valid[gk+1])))
	sr_write[gk] = 0;
	if (gk > 0 && (!sr_valid[gk-1]
	\|\| (sr_advance[gk-1] && !sr_valid[gk])))
	sr_write[gk] = 0;
	end
	// }}}

	// sr_valid
	// {{{
	initial sr_valid[gk] = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	sr_valid[gk] <= 0;
	else if (sr_write[gk])
	sr_valid[gk] <= 1;
	else if (sr_advance[gk] && gk<NSREG-1)
	sr_valid[gk] <= sr_valid[gk+1];
	else if (sr_advance[gk])
	sr_valid[gk] <= 0;
	// }}}

	// sr_id, sr_data, sr_strb, sr_last
	// {{{
	always @(posedge S_AXI_ACLK)
	if (OPT_LOWPOWER && !S_AXI_ARESETN)
	begin
	sr_id[gk] <= 0;
	sr_data[gk] <= 0;
	sr_strb[gk] <= 0;
	sr_last[gk] <= 0;
	end else if (sr_write[gk])
	begin
	sr_id[gk] <= S_AXI3_WID;
	sr_data[gk] <= S_AXI3_WDATA;
	sr_strb[gk] <= S_AXI3_WSTRB;
	sr_last[gk] <= S_AXI3_WLAST;
	end else if ((gk < NSREG-1) && sr_advance[gk])
	begin
	sr_id[gk] <= sr_id[gk+1];
	sr_data[gk] <= sr_data[gk+1];
	sr_strb[gk] <= sr_strb[gk+1];
	sr_last[gk] <= sr_last[gk+1];

	if (OPT_LOWPOWER && gk < NSREG-1 && !sr_valid[gk+1])
	begin
	// If we are running in low power,
	// Keep every unused register == 0
	sr_id[gk] <= 0;
	sr_data[gk] <= 0;
	sr_strb[gk] <= 0;
	sr_last[gk] <= 0;
	end
	end else if ((!OPT_LOWPOWER && !sr_valid[gk])
	\|\| sr_write[gk])
	begin
	sr_id[gk] <= S_AXI3_WID;
	sr_data[gk] <= S_AXI3_WDATA;
	sr_strb[gk] <= S_AXI3_WSTRB;
	sr_last[gk] <= S_AXI3_WLAST;
	end
	// }}}
	end
	// }}}
	////////////////////////////////////////////////////////////////
	//
	// Pick a register location to output
	// {{{
	////////////////////////////////////////////////////////////////
	//
	reg known_next;
	reg [LGWFIFO-1:0] sr_next;
	always @(*)
	begin
	known_next = 0;
	sr_next = -1;
	for(ik=0; ik<NSREG; ik=ik+1)
	if (!known_next && current_id == sr_id[ik])
	begin
	sr_next = ik[LGWFIFO-1:0];
	known_next = sr_valid[ik];
	end

	if (!cid_valid)
	known_next = 0;
	end

	assign S_AXI3_WREADY = !sr_valid[NSREG-1];
	// }}}
	////////////////////////////////////////////////////////////////
	//
	//
	// {{{
	////////////////////////////////////////////////////////////////
	//
	//
	always @(*)
	read_awid_fifo = (!M_AXI_WVALID \|\| M_AXI_WREADY)
	&& (!cid_valid
	\|\| (known_next && sr_last[sr_next]));

	always @(*)
	read_beat_fifo = (!M_AXI_WVALID \|\| M_AXI_WREADY)
	&&(known_next);

	initial M_AXI_WVALID = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	M_AXI_WVALID <= 0;
	else if (!M_AXI_WVALID \|\| M_AXI_WREADY)
	M_AXI_WVALID <= known_next;

	initial M_AXI_WID = 0;
	initial M_AXI_WDATA = 0;
	initial M_AXI_WSTRB = 0;
	initial M_AXI_WLAST = 0;
	always @(posedge S_AXI_ACLK)
	if (OPT_LOWPOWER && !S_AXI_ARESETN)
	begin
	// {{{
	M_AXI_WID <= 0;
	M_AXI_WDATA <= 0;
	M_AXI_WSTRB <= 0;
	M_AXI_WLAST <= 0;
	// }}}
	end else if (!M_AXI_WVALID \|\| M_AXI_WREADY)
	begin
	if (OPT_LOWPOWER && !known_next)
	begin
	// {{{
	M_AXI_WID <= 0;
	M_AXI_WDATA <= 0;
	M_AXI_WSTRB <= 0;
	M_AXI_WLAST <= 0;
	// }}}
	end else begin
	// {{{
	M_AXI_WID <= current_id;
	// Verilator lint_off WIDTH
	M_AXI_WDATA <= sr_data[sr_next];
	M_AXI_WSTRB <= sr_strb[sr_next];
	M_AXI_WLAST <= sr_last[sr_next];
	// Verilator lint_on WIDTH
	// }}}
	end
	end
	// }}}
	// Verilator lint_off UNUSED
	wire unused_sreg;
	assign unused_sreg = &{ 1'b0, read_beat_fifo };
	// Verilator lint_on UNUSED
	`ifdef FORMAL
	always @(*)
	if (S_AXI3_WVALID && S_AXI3_WREADY)
	assert($onehot(sr_write));
	else if (S_AXI_ARESETN)
	assert(sr_write == 0);

	always @(*)
	assert(((sr_write << 1) & sr_valid) == 0);

	reg cvr_sreg_full;

	initial cvr_sreg_full = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	cvr_sreg_full <= 0;
	else if (!S_AXI3_WREADY)
	cvr_sreg_full <= 1;

	always @(*)
	cover(cvr_sreg_full && sr_valid == 0);

	`endif
	// }}}
	end else if (OPT_METHOD == MTHD_PERID_FIFOS)
	begin : MULTIPLE_FIFOS
	// {{{
	wire [NUM_FIFOS-1:0] wbfifo_full, wbfifo_empty, wbfifo_last;
	// wire [IW-1:0] wbfifo_id [0:NUM_FIFOS-1];
	wire [DW-1:0] wbfifo_data [0:NUM_FIFOS-1];
	wire [DW/8-1:0] wbfifo_strb [0:NUM_FIFOS-1];

	////////////////////////////////////////////////////////////////
	//
	// The write beat FIFO
	////////////////////////////////////////////////////////////////
	// {{{
	//
	// Every write beat goes into a separate FIFO based on its ID
	//
	for (gk=0; gk < NUM_FIFOS; gk=gk+1)
	begin
	// {{{
	wire [LGWFIFO:0] wbfifo_fill;

	sfifo #(
	.BW(DW+(DW/8)+1),
	.LGFLEN(LGWFIFO),
	.OPT_READ_ON_EMPTY(OPT_LOW_LATENCY)
	) write_beat_fifo (
	.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
	.i_wr(S_AXI3_WVALID && S_AXI3_WREADY && S_AXI3_WID == gk),
	.i_data({ S_AXI3_WDATA, S_AXI3_WSTRB,
	S_AXI3_WLAST }),
	.o_full(wbfifo_full[gk]), .o_fill(wbfifo_fill),
	.i_rd(read_beat_fifo && current_id == gk),
	.o_data({ wbfifo_data[gk],
	wbfifo_strb[gk], wbfifo_last[gk] }),
	.o_empty(wbfifo_empty[gk])
	);

	// Verilator lint_off UNUSED
	wire unused;
	assign unused = &{ 1'b0, wbfifo_fill };
	// Verilator lint_on UNUSED
	// }}}
	end

	assign S_AXI3_WREADY = !wbfifo_full[S_AXI3_WID];
	// }}}
	////////////////////////////////////////////////////////////////
	//
	// Outgoing write data channel
	// {{{
	////////////////////////////////////////////////////////////////
	//
	//

	always @(*)
	read_awid_fifo = (!M_AXI_WVALID \|\| M_AXI_WREADY)
	&& (!cid_valid
	\|\| (read_beat_fifo && wbfifo_last[current_id]));
	// Write packets associated with the current ID can move forward
	always @(*)
	read_beat_fifo = (!M_AXI_WVALID \|\| M_AXI_WREADY)
	&&(cid_valid)&&(!wbfifo_empty[current_id]);

	initial M_AXI_WVALID = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	M_AXI_WVALID <= 0;
	else if (!M_AXI_WVALID \|\| M_AXI_WREADY)
	M_AXI_WVALID <= read_beat_fifo;

	initial M_AXI_WID = 0;
	initial M_AXI_WDATA = 0;
	initial M_AXI_WSTRB = 0;
	initial M_AXI_WLAST = 0;
	always @(posedge S_AXI_ACLK)
	if (OPT_LOWPOWER && !S_AXI_ARESETN)
	begin
	// {{{
	M_AXI_WID <= 0;
	M_AXI_WDATA <= 0;
	M_AXI_WSTRB <= 0;
	M_AXI_WLAST <= 0;
	// }}}
	end else if (!M_AXI_WVALID \|\| M_AXI_WREADY)
	begin
	// {{{
	M_AXI_WID <= current_id;
	M_AXI_WDATA <= wbfifo_data[current_id];
	M_AXI_WSTRB <= wbfifo_strb[current_id];
	M_AXI_WLAST <= wbfifo_last[current_id];

	if (OPT_LOWPOWER && !read_beat_fifo)
	begin
	// {{{
	M_AXI_WID <= 0;
	M_AXI_WDATA <= 0;
	M_AXI_WSTRB <= 0;
	M_AXI_WLAST <= 0;
	// }}}
	end
	// }}}
	end
	// }}}
	// }}}
	end endgenerate
	// }}}
	// Make Verilator happy
	// {{{
	// Verilator lint_off UNUSED
	wire unused;
	assign unused = &{ 1'b0, awfifo_fill };
	// Verilator lint_on UNUSED
	// }}}
	////////////////////////////////////////////////////////////////////////////////
	////////////////////////////////////////////////////////////////////////////////
	////////////////////////////////////////////////////////////////////////////////
	//
	// Formal properties
	// {{{
	////////////////////////////////////////////////////////////////////////////////
	////////////////////////////////////////////////////////////////////////////////
	////////////////////////////////////////////////////////////////////////////////
	`ifdef FORMAL
	reg f_past_valid;
	reg [LGAWFIFO+LGWFIFO-1:0] f_awid_count;
	(* anyconst *) reg [IW-1:0] f_const_id;

	initial f_past_valid = 0;
	always @(posedge S_AXI_ACLK)
	f_past_valid <= 1;

	always @(*)
	if (!f_past_valid)
	assume(!S_AXI_ARESETN);

	always @(posedge S_AXI_ACLK)
	if (!f_past_valid \|\| $past(!S_AXI_ARESETN))
	begin
	assume(!S_AXI3_AWVALID);
	assume(!S_AXI3_WVALID);

	assume(!M_AXI_WVALID);
	end else begin
	if ($past(S_AXI3_AWVALID && !S_AXI3_AWREADY))
	begin
	assume(S_AXI3_AWVALID);
	assume($stable(S_AXI3_AWID));
	end

	if ($past(S_AXI3_WVALID && !S_AXI3_WREADY))
	begin
	assume(S_AXI3_WVALID);
	assume($stable(S_AXI3_WID));
	assume($stable(S_AXI3_WDATA));
	assume($stable(S_AXI3_WSTRB));
	assume($stable(S_AXI3_WLAST));
	end

	if ($past(M_AXI_WVALID && !M_AXI_WREADY))
	begin
	assert(M_AXI_WVALID);
	assert($stable(M_AXI_WID));
	assert($stable(M_AXI_WDATA));
	assert($stable(M_AXI_WSTRB));
	assert($stable(M_AXI_WLAST));
	end
	end

	generate if (OPT_METHOD != MTHD_NONE)
	begin : F_FIFO_CHECK
	wire [LGWFIFO:0] f_ckfifo_fill;
	wire [LGWFIFO:0] f_ckfifo_full, f_ckfifo_empty;
	wire [IW-1:0] f_ckfifo_id;
	wire [DW-1:0] f_ckfifo_data;
	wire [DW/8-1:0] f_ckfifo_strb;
	wire f_ckfifo_last;

	sfifo #(
	.BW(IW + DW + (DW/8) + 1),
	.LGFLEN(LGWFIFO),
	.OPT_READ_ON_EMPTY(OPT_LOW_LATENCY)
	) f_checkfifo (
	.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
	.i_wr(S_AXI3_WVALID && S_AXI3_WREADY
	&& S_AXI3_WID == f_const_id),
	.i_data({ S_AXI3_WID, S_AXI3_WDATA, S_AXI3_WSTRB, S_AXI3_WLAST }),
	.o_full(f_ckfifo_full), .o_fill(f_ckfifo_fill),
	.i_rd(M_AXI_WVALID && M_AXI_WREADY
	&& M_AXI_WID == f_const_id),
	.o_data({ f_ckfifo_id, f_ckfifo_data, f_ckfifo_strb,
	f_ckfifo_last }),
	.o_empty(f_ckfifo_empty)
	);

	always @(*)
	if (S_AXI_ARESETN && M_AXI_WVALID && M_AXI_WID == f_const_id)
	begin
	assert(!f_ckfifo_empty);
	assert(f_ckfifo_id == M_AXI_WID);
	assert(f_ckfifo_data == M_AXI_WDATA);
	assert(f_ckfifo_strb == M_AXI_WSTRB);
	assert(f_ckfifo_last == M_AXI_WLAST);
	end
	end endgenerate

	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	f_awid_count = 0;
	else case({S_AXI3_AWVALID&& S_AXI3_AWREADY && S_AXI3_AWID == f_const_id,
	M_AXI_WVALID && M_AXI_WREADY && M_AXI_WLAST
	&& M_AXI_WID == f_const_id })
	2'b01: f_awid_count <= f_awid_count - 1;
	2'b10: f_awid_count <= f_awid_count + 1;
	default begin end
	endcase

	always @(*)
	if (M_AXI_WVALID && M_AXI_WID == f_const_id)
	assert(f_awid_count > 0);

	generate if (OPT_LOWPOWER)
	begin : F_LOWPOWER_CHECK
	always @(*)
	if (!S_AXI3_AWVALID)
	assume(S_AXI3_AWID == 0);

	always @(*)
	if (!S_AXI3_WVALID)
	begin
	assume(S_AXI3_WID == 0);
	assume(S_AXI3_WDATA == 0);
	assume(S_AXI3_WSTRB == 0);
	assume(S_AXI3_WLAST == 0);
	end

	always @(*)
	if (!M_AXI_WVALID)
	begin
	assert(M_AXI_WID == 0);
	assert(M_AXI_WDATA == 0);
	assert(M_AXI_WSTRB == 0);
	assert(M_AXI_WLAST == 0);
	end

	end endgenerate

	`endif
	// }}}
	endmodule