////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	txuartlite.v
// {{{
// Project:	wbuart32, a full featured UART with simulator
//
// Purpose:	Transmit outputs over a single UART line.  This particular UART
//		implementation has been extremely simplified: it does not handle
//	generating break conditions, nor does it handle anything other than the
//	8N1 (8 data bits, no parity, 1 stop bit) UART sub-protocol.
//
//	To interface with this module, connect it to your system clock, and
//	pass it the byte of data you wish to transmit.  Strobe the i_wr line
//	high for one cycle, and your data will be off.  Wait until the 'o_busy'
//	line is low before strobing the i_wr line again--this implementation
//	has NO BUFFER, so strobing i_wr while the core is busy will just
//	get ignored.  The output will be placed on the o_txuart output line.
//
//	(I often set both data and strobe on the same clock, and then just leave
//	them set until the busy line is low.  Then I move on to the next piece
//	of data.)
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
// }}}
// Copyright (C) 2015-2021, Gisselquist Technology, LLC
// {{{
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
// for more details.
//
// You should have received a copy of the GNU General Public License along
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
// target there if the PDF file isn't present.)  If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License:	GPL, v3, as defined and found on www.gnu.org,
//		http://www.gnu.org/licenses/gpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
// }}}
module txuartlite #(
		// {{{
		// TIMING_BITS -- the number of bits required to represent
		// the number of clocks per baud.  24 should be sufficient for
		// most baud rates, but you can trim it down to save logic if
		// you would like.  TB is just an abbreviation for TIMING_BITS.
		parameter	[4:0]	TIMING_BITS = 5'd24,
		// CLOCKS_PER_BAUD -- the number of system clocks per baud
		// interval.
		parameter	[(TB-1):0]	CLOCKS_PER_BAUD = 8 // 24'd868
		// }}}
	) (
		// {{{
		input	wire		i_clk,
		input	wire		i_wr,
		input	wire	[7:0]	i_data,
		// And the UART input line itself
		output	reg		o_uart_tx,
		// A line to tell others when we are ready to accept data.  If
		// (i_wr)&&(!o_busy) is ever true, then the core has accepted
		// a byte for transmission.
		output	wire		o_busy
		// }}}
	);

	localparam		TB = TIMING_BITS;

	// Register/net declarations
	// {{{
	localparam [3:0]	TXUL_BIT_ZERO  = 4'h0,
			//	TXUL_BIT_ONE   = 4'h1,
			//	TXUL_BIT_TWO   = 4'h2,
			//	TXUL_BIT_THREE = 4'h3,
			//	TXUL_BIT_FOUR  = 4'h4,
			//	TXUL_BIT_FIVE  = 4'h5,
			//	TXUL_BIT_SIX   = 4'h6,
			//	TXUL_BIT_SEVEN = 4'h7,
				TXUL_STOP      = 4'h8,
				TXUL_IDLE      = 4'hf;

	reg	[(TB-1):0]	baud_counter;
	reg	[3:0]	state;
	reg	[7:0]	lcl_data;
	reg		r_busy, zero_baud_counter;
	// }}}

	// Big state machine controlling: r_busy, state
	// {{{
	//


	initial	r_busy = 1'b1;
	initial	state  = TXUL_IDLE;
	always @(posedge i_clk)
	begin
		if (!zero_baud_counter)
			// r_busy needs to be set coming into here
			r_busy <= 1'b1;
		else if (state > TXUL_STOP)	// STATE_IDLE
		begin
			state <= TXUL_IDLE;
			r_busy <= 1'b0;
			if ((i_wr)&&(!r_busy))
			begin	// Immediately start us off with a start bit
				r_busy <= 1'b1;
				state <= TXUL_BIT_ZERO;
			end
		end else begin
			// One clock tick in each of these states ...
			r_busy <= 1'b1;
			if (state <=TXUL_STOP) // start bit, 8-d bits, stop-b
				state <= state + 1'b1;
			else
				state <= TXUL_IDLE;
		end
	end
	// }}}

	// o_busy
	// {{{
	//
	// This is a wire, designed to be true is we are ever busy above.
	// originally, this was going to be true if we were ever not in the
	// idle state.  The logic has since become more complex, hence we have
	// a register dedicated to this and just copy out that registers value.
	assign	o_busy = (r_busy);
	// }}}

	// lcl_data
	// {{{
	//
	// This is our working copy of the i_data register which we use
	// when transmitting.  It is only of interest during transmit, and is
	// allowed to be whatever at any other time.  Hence, if r_busy isn't
	// true, we can always set it.  On the one clock where r_busy isn't
	// true and i_wr is, we set it and r_busy is true thereafter.
	// Then, on any zero_baud_counter (i.e. change between baud intervals)
	// we simple logically shift the register right to grab the next bit.
	initial	lcl_data = 8'hff;
	always @(posedge i_clk)
		if ((i_wr)&&(!r_busy))
			lcl_data <= i_data;
		else if (zero_baud_counter)
			lcl_data <= { 1'b1, lcl_data[7:1] };
	// }}}

	// o_uart_tx
	// {{{
	//
	// This is the final result/output desired of this core.  It's all
	// centered about o_uart_tx.  This is what finally needs to follow
	// the UART protocol.
	//
	initial	o_uart_tx = 1'b1;
	always @(posedge i_clk)
		if ((i_wr)&&(!r_busy))
			o_uart_tx <= 1'b0;	// Set the start bit on writes
		else if (zero_baud_counter)	// Set the data bit.
			o_uart_tx <= lcl_data[0];
	// }}}

	// Baud counter
	// {{{
	// All of the above logic is driven by the baud counter.  Bits must last
	// CLOCKS_PER_BAUD in length, and this baud counter is what we use to
	// make certain of that.
	//
	// The basic logic is this: at the beginning of a bit interval, start
	// the baud counter and set it to count CLOCKS_PER_BAUD.  When it gets
	// to zero, restart it.
	//
	// However, comparing a 28'bit number to zero can be rather complex--
	// especially if we wish to do anything else on that same clock.  For
	// that reason, we create "zero_baud_counter".  zero_baud_counter is
	// nothing more than a flag that is true anytime baud_counter is zero.
	// It's true when the logic (above) needs to step to the next bit.
	// Simple enough?
	//
	// I wish we could stop there, but there are some other (ugly)
	// conditions to deal with that offer exceptions to this basic logic.
	//
	// 1. When the user has commanded a BREAK across the line, we need to
	// wait several baud intervals following the break before we start
	// transmitting, to give any receiver a chance to recognize that we are
	// out of the break condition, and to know that the next bit will be
	// a stop bit.
	//
	// 2. A reset is similar to a break condition--on both we wait several
	// baud intervals before allowing a start bit.
	//
	// 3. In the idle state, we stop our counter--so that upon a request
	// to transmit when idle we can start transmitting immediately, rather
	// than waiting for the end of the next (fictitious and arbitrary) baud
	// interval.
	//
	// When (i_wr)&&(!r_busy)&&(state == TXUL_IDLE) then we're not only in
	// the idle state, but we also just accepted a command to start writing
	// the next word.  At this point, the baud counter needs to be reset
	// to the number of CLOCKS_PER_BAUD, and zero_baud_counter set to zero.
	//
	// The logic is a bit twisted here, in that it will only check for the
	// above condition when zero_baud_counter is false--so as to make
	// certain the STOP bit is complete.
	initial	zero_baud_counter = 1'b1;
	initial	baud_counter = 0;
	always @(posedge i_clk)
	begin
		zero_baud_counter <= (baud_counter == 1);
		if (state == TXUL_IDLE)
		begin
			baud_counter <= 0;
			zero_baud_counter <= 1'b1;
			if ((i_wr)&&(!r_busy))
			begin
				baud_counter <= CLOCKS_PER_BAUD - 1'b1;
				zero_baud_counter <= 1'b0;
			end
		end else if (!zero_baud_counter)
			baud_counter <= baud_counter - 1'b1;
		else if (state > TXUL_STOP)
		begin
			baud_counter <= 0;
			zero_baud_counter <= 1'b1;
		end else if (state == TXUL_STOP)
			// Need to complete this state one clock early, so
			// we can release busy one clock before the stop bit
			// is complete, so we can start on the next byte
			// exactly 10*CLOCKS_PER_BAUD clocks after we started
			// the last one
			baud_counter <= CLOCKS_PER_BAUD - 2;
		else // All other states
			baud_counter <= CLOCKS_PER_BAUD - 1'b1;
	end
	// }}}
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
// FORMAL METHODS
// {{{
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
`ifdef	FORMAL
	// Declarations
`ifdef	TXUARTLITE
`define	ASSUME	assume
`else
`define	ASSUME	assert
`endif
	reg			f_past_valid, f_last_clk;
	reg	[(TB-1):0]	f_baud_count;
	reg	[9:0]		f_txbits;
	reg	[3:0]		f_bitcount;
	reg	[7:0]		f_request_tx_data;
	wire	[3:0]		subcount;

	// Setup
	// {{{
	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid <= 1'b1;

	initial	`ASSUME(!i_wr);
	always @(posedge i_clk)
		if ((f_past_valid)&&($past(i_wr))&&($past(o_busy)))
		begin
			`ASSUME(i_wr   == $past(i_wr));
			`ASSUME(i_data == $past(i_data));
		end
	// }}}

	// Check the baud counter
	// {{{
	always @(posedge i_clk)
		assert(zero_baud_counter == (baud_counter == 0));

	always @(posedge i_clk)
	if ((f_past_valid)&&($past(baud_counter != 0))&&($past(state != TXUL_IDLE)))
		assert(baud_counter == $past(baud_counter - 1'b1));

	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(zero_baud_counter))&&($past(state != TXUL_IDLE)))
		assert($stable(o_uart_tx));

	initial	f_baud_count = 1'b0;
	always @(posedge i_clk)
	if (zero_baud_counter)
		f_baud_count <= 0;
	else
		f_baud_count <= f_baud_count + 1'b1;

	always @(posedge i_clk)
		assert(f_baud_count < CLOCKS_PER_BAUD);

	always @(posedge i_clk)
	if (baud_counter != 0)
		assert(o_busy);
	// }}}

	// {{{
	initial	f_txbits = 0;
	always @(posedge i_clk)
	if (zero_baud_counter)
		f_txbits <= { o_uart_tx, f_txbits[9:1] };

	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(zero_baud_counter))
			&&(!$past(state==TXUL_IDLE)))
		assert(state == $past(state));

	initial	f_bitcount = 0;
	always @(posedge i_clk)
	if ((!f_past_valid)||(!$past(f_past_valid)))
		f_bitcount <= 0;
	else if ((state == TXUL_IDLE)&&(zero_baud_counter))
		f_bitcount <= 0;
	else if (zero_baud_counter)
		f_bitcount <= f_bitcount + 1'b1;

	always @(posedge i_clk)
		assert(f_bitcount <= 4'ha);

	always @(*)
	if (!o_busy)
		assert(zero_baud_counter);

	always @(posedge i_clk)
	if ((i_wr)&&(!o_busy))
		f_request_tx_data <= i_data;

	assign	subcount = 10-f_bitcount;
	always @(posedge i_clk)
	if (f_bitcount > 0)
		assert(!f_txbits[subcount]);

	always @(posedge i_clk)
	if (f_bitcount == 4'ha)
	begin
		assert(f_txbits[8:1] == f_request_tx_data);
		assert( f_txbits[9]);
	end

	always @(posedge i_clk)
		assert((state <= TXUL_STOP + 1'b1)||(state == TXUL_IDLE));

	always @(posedge i_clk)
	if ((f_past_valid)&&($past(f_past_valid))&&($past(o_busy)))
		cover(!o_busy);
	// }}}

`endif	// FORMAL
`ifdef	VERIFIC_SVA
	reg	[7:0]	fsv_data;

	//
	// Grab a copy of the data any time we are sent a new byte to transmit
	// We'll use this in a moment to compare the item transmitted against
	// what is supposed to be transmitted
	//
	always @(posedge i_clk)
	if ((i_wr)&&(!o_busy))
		fsv_data <= i_data;

	//
	// One baud interval
	// {{{
	//
	// 1. The UART output is constant at DAT
	// 2. The internal state remains constant at ST
	// 3. CKS = the number of clocks per bit.
	//
	// Everything stays constant during the CKS clocks with the exception
	// of (zero_baud_counter), which is *only* raised on the last clock
	// interval
	sequence	BAUD_INTERVAL(CKS, DAT, SR, ST);
		((o_uart_tx == DAT)&&(state == ST)
			&&(lcl_data == SR)
			&&(!zero_baud_counter))[*(CKS-1)]
		##1 (o_uart_tx == DAT)&&(state == ST)
			&&(lcl_data == SR)
			&&(zero_baud_counter);
	endsequence
	// }}}

	//
	// One byte transmitted
	// {{{
	//
	// DATA = the byte that is sent
	// CKS  = the number of clocks per bit
	//
	sequence	SEND(CKS, DATA);
		BAUD_INTERVAL(CKS, 1'b0, DATA, 4'h0)
		##1 BAUD_INTERVAL(CKS, DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h1)
		##1 BAUD_INTERVAL(CKS, DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h2)
		##1 BAUD_INTERVAL(CKS, DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h3)
		##1 BAUD_INTERVAL(CKS, DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h4)
		##1 BAUD_INTERVAL(CKS, DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h5)
		##1 BAUD_INTERVAL(CKS, DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h6)
		##1 BAUD_INTERVAL(CKS, DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h7)
		##1 BAUD_INTERVAL(CKS, DATA[7], 8'hff, 4'h8)
		##1 BAUD_INTERVAL(CKS-1, 1'b1, 8'hff, 4'h9);
	endsequence
	// }}}

	//
	// Transmit one byte
	// {{{
	// Once the byte is transmitted, make certain we return to
	// idle
	//
	assert property (
		@(posedge i_clk)
		(i_wr)&&(!o_busy)
		|=> ((o_busy) throughout SEND(CLOCKS_PER_BAUD,fsv_data))
		##1 (!o_busy)&&(o_uart_tx)&&(zero_baud_counter));
	// }}}

	// {{{
	assume property (
		@(posedge i_clk)
		(i_wr)&&(o_busy) |=>
			(i_wr)&&($stable(i_data)));

	//
	// Make certain that o_busy is true any time zero_baud_counter is
	// non-zero
	//
	always @(*)
		assert((o_busy)||(zero_baud_counter) );

	// If and only if zero_baud_counter is true, baud_counter must be zero
	// Insist on that relationship here.
	always @(*)
		assert(zero_baud_counter == (baud_counter == 0));

	// To make certain baud_counter stays below CLOCKS_PER_BAUD
	always @(*)
		assert(baud_counter < CLOCKS_PER_BAUD);

	//
	// Insist that we are only ever in a valid state
	always @(*)
		assert((state <= TXUL_STOP+1'b1)||(state == TXUL_IDLE));
	// }}}

`endif // Verific SVA
// }}}
endmodule