////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	xlnxstream_2018_3
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	To test the formal tools on an AXI stream master core that is
//		"known" to work.  This core was generated via the IP packager
//	in Vivado 2018.3.  Sadly, it's broken in a couple of ways, one which
//	is prominently the TLAST signal which may be set even through the
//	channel is stalled.  Feel free to try it out.
//
//	This core will fail a verification check.
//
// Creator:	Vivado, 2018.3
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
//
`timescale 1 ns / 1 ps

module xlnxstream_2018_3 #
	(
		// Users to add parameters here

		// User parameters ends
		// Do not modify the parameters beyond this line

		// Width of S_AXIS address bus. The slave accepts the read and write addresses of width C_M_AXIS_TDATA_WIDTH.
		parameter integer C_M_AXIS_TDATA_WIDTH	= 32,
		// Start count is the number of clock cycles the master will wait before initiating/issuing any transaction.
		parameter integer C_M_START_COUNT	= 32
	)
	(
		// Users to add ports here

		// User ports ends
		// Do not modify the ports beyond this line

		// Global ports
		input wire  M_AXIS_ACLK,
		//
		input wire  M_AXIS_ARESETN,
		// Master Stream Ports. TVALID indicates that the master
		// is driving a valid transfer, A transfer takes place
		// when both TVALID and TREADY are asserted.
		output wire  M_AXIS_TVALID,
		// TDATA is the primary payload that is used to provide the
		// data that is passing across the interface from the master.
		output wire [C_M_AXIS_TDATA_WIDTH-1 : 0] M_AXIS_TDATA,
		// TSTRB is the byte qualifier that indicates whether the
		// content of the associated byte of TDATA is processed as a
		// data byte or a position byte.
		output wire [(C_M_AXIS_TDATA_WIDTH/8)-1 : 0] M_AXIS_TSTRB,
		// TLAST indicates the boundary of a packet.
		output wire  M_AXIS_TLAST,
		// TREADY indicates that the slave can accept a transfer in
		// the current cycle.
		input wire  M_AXIS_TREADY
	);
	// Total number of output data
	localparam NUMBER_OF_OUTPUT_WORDS = 8;

	// function called clogb2 that returns an integer which has the
	// value of the ceiling of the log base 2.
	function integer clogb2 (input integer bit_depth);
	begin
		for(clogb2=0; bit_depth>0; clogb2=clogb2+1)
			bit_depth = bit_depth >> 1;
	end endfunction

	// WAIT_COUNT_BITS is the width of the wait counter.
	localparam integer WAIT_COUNT_BITS = clogb2(C_M_START_COUNT-1);

	// bit_num gives the minimum number of bits needed to address 'depth'
	// size of FIFO.
	localparam bit_num  = clogb2(NUMBER_OF_OUTPUT_WORDS);

	// Define the states of state machine
	// The control state machine oversees the writing of input streaming
	// data to the FIFO, and outputs the streaming data from the FIFO
	parameter [1:0] IDLE = 2'b00,	// This is the initial/idle state

		INIT_COUNTER  = 2'b01,	// This state initializes the counter,
					// once the counter reaches
					// C_M_START_COUNT count, the state
					// machine changes state to SEND_STREAM
		SEND_STREAM   = 2'b10;	// In this state the
					// stream data is output through M_AXIS_TDATA
	// State variable
	reg [1:0] mst_exec_state;
	// Example design FIFO read pointer
	reg [bit_num-1:0] read_pointer;

	// AXI Stream internal signals
	// wait counter. The master waits for the user defined number of
	// clock cycles before initiating a transfer.
	reg [WAIT_COUNT_BITS-1 : 0] 	count;
	//streaming data valid
	wire  	axis_tvalid;
	//streaming data valid delayed by one clock cycle
	reg  	axis_tvalid_delay;
	//Last of the streaming data
	wire  	axis_tlast;
	//Last of the streaming data delayed by one clock cycle
	reg  	axis_tlast_delay;
	//FIFO implementation signals
	reg [C_M_AXIS_TDATA_WIDTH-1 : 0] 	stream_data_out;
	wire  	tx_en;
	//The master has issued all the streaming data stored in FIFO
	reg  	tx_done;


	// I/O Connections assignments

	assign M_AXIS_TVALID	= axis_tvalid_delay;
	assign M_AXIS_TDATA	= stream_data_out;
	assign M_AXIS_TLAST	= axis_tlast_delay;
	assign M_AXIS_TSTRB	= {(C_M_AXIS_TDATA_WIDTH/8){1'b1}};


	// Control state machine implementation
	always @(posedge M_AXIS_ACLK)
	if (!M_AXIS_ARESETN)
	// Synchronous reset (active low)
	begin
		mst_exec_state <= IDLE;
		count <= 0;
	end else case (mst_exec_state)
	IDLE:
		// The slave starts accepting tdata when
		// there tvalid is asserted to mark the
		// presence of valid streaming data
		//if ( count == 0 )
		//  begin
		mst_exec_state  <= INIT_COUNTER;
		//  end
		//else
		//  begin
		//    mst_exec_state  <= IDLE;
		//  end

	INIT_COUNTER:
		// The slave starts accepting tdata when
		// there tvalid is asserted to mark the
		// presence of valid streaming data
		if ( count == C_M_START_COUNT - 1 )
			mst_exec_state  <= SEND_STREAM;
		else begin
			count <= count + 1;
			mst_exec_state  <= INIT_COUNTER;
		end

	SEND_STREAM:
		// The example design streaming master functionality starts when
		// the master drives output tdata from the FIFO and the slave
		// has finished storing the S_AXIS_TDATA
		if (tx_done)
			mst_exec_state <= IDLE;
		else
			mst_exec_state <= SEND_STREAM;
	endcase


	//tvalid generation
	//axis_tvalid is asserted when the control state machine's state
	// is SEND_STREAM and number of output streaming data is less than
	// the NUMBER_OF_OUTPUT_WORDS.
	assign axis_tvalid = ((mst_exec_state == SEND_STREAM) && (read_pointer < NUMBER_OF_OUTPUT_WORDS));

	// AXI tlast generation
	// axis_tlast is asserted number of output streaming data
	// is NUMBER_OF_OUTPUT_WORDS-1 (0 to NUMBER_OF_OUTPUT_WORDS-1)
	assign axis_tlast = (read_pointer == NUMBER_OF_OUTPUT_WORDS-1);


	// Delay the axis_tvalid and axis_tlast signal by one clock cycle
	// to match the latency of M_AXIS_TDATA
	always @(posedge M_AXIS_ACLK)
	if (!M_AXIS_ARESETN)
	begin
		axis_tvalid_delay <= 1'b0;
		axis_tlast_delay <= 1'b0;
	end else begin
		axis_tvalid_delay <= axis_tvalid;
		axis_tlast_delay <= axis_tlast;
	end


	//read_pointer pointer
	always@(posedge M_AXIS_ACLK)
	if(!M_AXIS_ARESETN)
	begin
		read_pointer <= 0;
		tx_done <= 1'b0;
	end else if (read_pointer <= NUMBER_OF_OUTPUT_WORDS-1)
	begin
		if (tx_en)
		// read pointer is incremented after every read from the FIFO
		// when FIFO read signal is enabled.
		begin
			read_pointer <= read_pointer + 1;
			tx_done <= 1'b0;
		end
	end else if (read_pointer == NUMBER_OF_OUTPUT_WORDS)
	begin
		// tx_done is asserted when NUMBER_OF_OUTPUT_WORDS numbers
		// of streaming data has been out.
		tx_done <= 1'b1;
	end


	//FIFO read enable generation
	assign tx_en = M_AXIS_TREADY && axis_tvalid;

		// Streaming output data is read from FIFO
	always @( posedge M_AXIS_ACLK )
	if(!M_AXIS_ARESETN)
		stream_data_out <= 1;
	else if (tx_en)// && M_AXIS_TSTRB[byte_index]
		stream_data_out <= read_pointer + 32'b1;

	////////////////////////////////////////////////////////////////////////
	//
	// Add user logic here
	//
	// The below initial lines, and FORMAL section following, were not in
	// Xilinx's original demo example.
	//
	// This initial logic is used to keep the formal proof consistent
	// below.  It's not strictly needed, neither was it part of Xilinx's
	// original example demo.
	initial count = 0;
	initial mst_exec_state = IDLE;
	initial	read_pointer = 0;
	initial tx_done = 0;
	// User logic ends
`ifdef	FORMAL
	localparam	F_LGDEPTH = $clog2(NUMBER_OF_OUTPUT_WORDS+1)+2;
	localparam	AW  = 1;
	localparam	IDW = 1;

	wire	[F_LGDEPTH-1:0]	f_bytecount;
	wire	[AW+IDW-1:0]	f_routecheck;

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

	//
	// Insist that the proof starts in reset
	//
	always @(*)
	if (!f_past_valid)
		assume(!M_AXIS_ARESETN);

	//
	// Insist on reset values
	//
	always @(posedge M_AXIS_ACLK)
	if (!f_past_valid || $past(!M_AXIS_ARESETN))
	begin
		assert(mst_exec_state == IDLE);
		assert(read_pointer == 0);
		assert(count == 0);
		assert(!tx_done);
	end

	//
	faxis_master #(
		.F_LGDEPTH(F_LGDEPTH),
		.F_MAX_PACKET({NUMBER_OF_OUTPUT_WORDS, 2'b00}+4),
		.C_S_AXI_DATA_WIDTH(C_M_AXIS_TDATA_WIDTH),
		.OPT_ASYNC_RESET(1'b0),
		.C_S_AXI_ADDR_WIDTH(AW),
		.C_S_AXI_ID_WIDTH(IDW),
		.C_S_AXI_USER_WIDTH(1))
	axi_stream_check(.i_aclk(M_AXIS_ACLK),
		.i_aresetn(M_AXIS_ARESETN),
		.i_tvalid(M_AXIS_TVALID),
		.i_tready(M_AXIS_TREADY),
		.i_tdata(M_AXIS_TDATA),
		.i_tstrb(M_AXIS_TSTRB),
		.i_tkeep(4'hf),
		.i_tid(0),
		.i_tdest(0),
		.i_tuser(0),
		.i_tlast(M_AXIS_TLAST),
		.f_bytecount(f_bytecount),
		.f_routecheck(f_routecheck));

// `define	INDUCTION_PROOF
`ifdef	INDUCTION_PROOF
	always @(*)
		assert(count <= C_M_START_COUNT-1);

	always @(*)
	if (count != C_M_START_COUNT-1)
	begin
		assert(!M_AXIS_TVALID);
		assert(read_pointer == 0);
	end

	always @(*)
	if (tx_done)
	begin
		assert(read_pointer == NUMBER_OF_OUTPUT_WORDS);
		// assert();
	end

	always @(*)
		assert(read_pointer <= NUMBER_OF_OUTPUT_WORDS);

	always @(*)
	if (tx_done)
		assert(!M_AXIS_TVALID);

	always @(*)
	if ((read_pointer > 0)&&(!tx_done))
		assert(M_AXIS_TVALID);

	always @(posedge M_AXIS_ACLK)
	if (f_past_valid)
		cover(M_AXIS_ARESETN && !M_AXIS_TVALID
			&& $past(M_AXIS_TVALID && M_AXIS_TLAST));

	always @(*)
	if (tx_done || M_AXIS_TVALID)
		assert(count == C_M_START_COUNT-1);

	always @(*)
		assert((mst_exec_state == IDLE)
			||(mst_exec_state == INIT_COUNTER)
			||(mst_exec_state == SEND_STREAM));

	// If you actually want to get induction to pass, you'll also need
	// to assume TREADY
	// always @(*)
	//	assume(M_AXIS_TREADY);
`endif

	////////////////////////////////////////////////////////////////////////
	//
	// Cover checks
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	reg	[3:0]	final_counter = 0;

	initial	final_counter = 0;
	always @(posedge M_AXIS_ACLK)
	if (!M_AXIS_ARESETN)
		final_counter <= 0;
	else if (tx_done)
		final_counter <= final_counter + 1;

	always @(*)
		cover(tx_done);

	always @(*)
		cover(&final_counter);
`endif
endmodule