////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	faxis_slave.v
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	Formal properties for verifying the proper functionality of an
//		AXI Stream slave.
//
// 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	faxis_slave #(
	parameter	F_MAX_PACKET = 0,
	parameter	F_MIN_PACKET = 0,
	parameter	F_MAX_STALL  = 0,
	parameter	C_S_AXI_DATA_WIDTH  = 32,
	parameter	C_S_AXI_ID_WIDTH = 1,
	parameter	C_S_AXI_ADDR_WIDTH = 1,
	parameter	C_S_AXI_USER_WIDTH = 1,
	parameter [0:0]	OPT_ASYNC_RESET = 1'b0,
	//
	// F_LGDEPTH is the number of bits necessary to represent a packets
	// length
	parameter	F_LGDEPTH = 32,
	//
	localparam	AW  = C_S_AXI_ADDR_WIDTH,
	localparam	DW  = C_S_AXI_DATA_WIDTH,
	localparam	IDW  = C_S_AXI_ID_WIDTH,
	localparam	UW  = C_S_AXI_USER_WIDTH
	//
	) (
	//
	input	wire			i_aclk, i_aresetn,
	input	wire			i_tvalid,
	input	wire			i_tready = 1,
	input	wire	[DW-1:0]	i_tdata,
	input	wire	[DW/8-1:0]	i_tstrb = {(DW/8){1'b1}},
	input	wire	[DW/8-1:0]	i_tkeep = {(DW/8){1'b1}},
	input	wire			i_tlast,
	input	wire	[(IDW>0?IDW:1)-1:0]	i_tid = {(IDW){1'b0}},
	input	wire	[(AW>0?AW:1)-1:0]	i_tdest = {(AW){1'b0}},
	input	wire	[(UW>0?UW:1)-1:0]	i_tuser = {(UW){1'b0}},
	//
	output	reg	[F_LGDEPTH-1:0]	f_bytecount,
	(* anyconst *) output	reg	[AW+IDW-1:0]	f_routecheck
	);

`define	SLAVE_ASSUME	assume
`define	SLAVE_ASSERT	assert

	localparam	F_STALLBITS	= (F_MAX_STALL <= 1)
						? 1 : $clog2(F_MAX_STALL+2);
	reg				f_past_valid;
	reg	[F_LGDEPTH-1:0]		f_vbytes;
	reg	[F_STALLBITS-1:0]	f_stall_count;
	integer	iB;
	genvar	k;

	//
	// f_past_valid is used to make certain that temporal assertions
	// depending upon past values depend upon *valid* past values.
	// It is true for all clocks other than the first clock.
	initial	f_past_valid = 1'b0;
	always @(posedge i_aclk)
		f_past_valid <= 1'b1;

	//
	// Reset should always be active (low) initially
	always @(posedge i_aclk)
	if (!f_past_valid)
		`SLAVE_ASSUME(!i_aresetn);

	//
	// During and following a reset, TVALID should be deasserted
	always @(posedge i_aclk)
	if ((!f_past_valid)||(!i_aresetn && OPT_ASYNC_RESET)||($past(!i_aresetn)))
		`SLAVE_ASSUME(!i_tvalid);

	//
	// If TVALID but not TREADY, then the master isn't allowed to change
	// anything until the slave asserts TREADY.
	always @(posedge i_aclk)
	if ((f_past_valid)&&($past(i_aresetn))&&(!OPT_ASYNC_RESET || i_aresetn)
		&&($past(i_tvalid))&&(!$past(i_tready)))
	begin
		`SLAVE_ASSUME(i_tvalid);
		`SLAVE_ASSUME($stable(i_tstrb));
		`SLAVE_ASSUME($stable(i_tkeep));
		`SLAVE_ASSUME($stable(i_tlast));
		`SLAVE_ASSUME($stable(i_tid));
		`SLAVE_ASSUME($stable(i_tdest));
		`SLAVE_ASSUME($stable(i_tuser));
	end

	generate for(k=0; k<DW/8; k=k+1)
	begin : CHECK_PARTIAL_DATA

		// If TVALID && !TREADY, only those TDATA values with TKEEP
		// high are required to maintain their values until TREADY
		// becomes true.
		always @(posedge i_aclk)
		if ((f_past_valid)&&($past(i_aresetn))
			&&(!OPT_ASYNC_RESET || i_aresetn)
			&&($past(i_tvalid))&&(!$past(i_tready)))
		begin
			if (i_tkeep[k])
				`SLAVE_ASSUME($stable(i_tdata[k*8 +: 8]));
			// else this is a null (don't care) byte, with
			// no data within it
			//
		end

	end endgenerate

	//
	// TKEEP == LOW and TSTRB == HIGH is reserved per the spec, and
	// must not be used
	always @(posedge i_aclk)
	if (i_tvalid)
		`SLAVE_ASSUME((~i_tkeep & i_tstrb)==0);

	//
	// f_vbytes is the number of valid bytes contained in the current beat
	// It is used for counting packet lengths below.
	always @(*)
	if (!i_tvalid)
		f_vbytes = 0;
	else begin
		f_vbytes = 0;
		for(iB=0; iB < DW/8; iB=iB+1)
		if (i_tkeep[iB] && i_tstrb[iB])
			f_vbytes = f_vbytes + 1;
	end

	//
	// f_bytecount is the number of bytes that have taken place so far in
	// the current packet transmission.  Note that we are *only* counting
	// our location within the stream if the TUSER and TDEST fields match
	// our (solver chosen) ROUTECHECK.  That way we don't have to check
	// *EVERY POSSIBLE* TUSER and TDEST combination.
	initial	f_bytecount = 0;
	always @(posedge i_aclk)
	if (!i_aresetn)
		f_bytecount <= 0;
	else if (i_tready && i_tvalid && ({ i_tuser, i_tdest } == f_routecheck))
	begin
		if (i_tlast)
			f_bytecount <= 0;
		else
			f_bytecount <= f_bytecount + f_vbytes;
	end

	//
	// Count the number of clock cycles between ready's.  We'll use this in
	// a bit to insist on an (optional) minimum transfer speed.
	initial	f_stall_count = 0;
	always @(posedge i_aclk)
	if (!i_aresetn || !i_tvalid || i_tready)
		f_stall_count <= 0;
	else if (!(&f_stall_count))
		f_stall_count <= f_stall_count + 1;

	//
	// F_MAX_PACKET
	//
	// An optional check, to make certain packets don't exceed some maximum
	// length
	generate if (F_MAX_PACKET > 0)
	begin : MAX_PACKET

		always @(*)
			`SLAVE_ASSUME(f_bytecount + f_vbytes <= F_MAX_PACKET);

	end endgenerate

	//
	// F_MIN_PACKET
	//
	// An optoinal check, forcing a minimum packet length
	generate if (F_MIN_PACKET > 0)
	begin : MIN_PACKET

		always @(*)
		if (i_tvalid && i_tlast)
			`SLAVE_ASSUME(f_bytecount + f_vbytes >= F_MIN_PACKET);

	end endgenerate

	//
	// F_MAX_STALL
	//
	// Another optional check, this time insisting that the READY flag can
	// only be low for up to F_MAX_STALL clocks.
	//
	generate if (F_MAX_STALL > 0)
	begin : MAX_STALL_CHECK

		always @(*)
			`SLAVE_ASSERT(f_stall_count < F_MAX_STALL);

	end endgenerate
endmodule
`undef	SLAVE_ASSUME
`undef	SLAVE_ASSERT