Megatest

////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	rxuartlite.v
//
// Project:	wbuart32, a full featured UART with simulator
//
// Purpose:	Receive and decode inputs from a single UART line.
//
//
//	To interface with this module, connect it to your system clock,
//	and a UART input.  Set the parameter to the number of clocks per
//	baud.  When data becomes available, the o_wr line will be asserted
//	for one clock cycle.
//
//	This interface only handles 8N1 serial port communications.  It does
//	not handle the break, parity, or frame error conditions.
//
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2020, 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
//
`define	RXUL_BIT_ZERO		4'h0
`define	RXUL_BIT_ONE		4'h1
`define	RXUL_BIT_TWO		4'h2
`define	RXUL_BIT_THREE		4'h3
`define	RXUL_BIT_FOUR		4'h4
`define	RXUL_BIT_FIVE		4'h5
`define	RXUL_BIT_SIX		4'h6
`define	RXUL_BIT_SEVEN		4'h7
`define	RXUL_STOP		4'h8
`define	RXUL_WAIT		4'h9
`define	RXUL_IDLE		4'hf

module rxuartlite(i_clk, i_uart_rx, o_wr, o_data);
	parameter			TIMER_BITS = 10;
`ifdef	FORMAL
	parameter  [(TIMER_BITS-1):0]	CLOCKS_PER_BAUD = 16; // Necessary for formal proof
`else
	parameter  [(TIMER_BITS-1):0]	CLOCKS_PER_BAUD = 868;	// 115200 MBaud at 100MHz
`endif
	localparam			TB = TIMER_BITS;
	input	wire		i_clk;
	input	wire		i_uart_rx;
	output	reg		o_wr;
	output	reg	[7:0]	o_data;


	wire	[(TB-1):0]	half_baud;
	reg	[3:0]		state;

	assign	half_baud = { 1'b0, CLOCKS_PER_BAUD[(TB-1):1] };
	reg	[(TB-1):0]	baud_counter;
	reg			zero_baud_counter;


	// Since this is an asynchronous receiver, we need to register our
	// input a couple of clocks over to avoid any problems with 
	// metastability.  We do that here, and then ignore all but the
	// ck_uart wire.
	reg	q_uart, qq_uart, ck_uart;
	initial	q_uart  = 1'b1;
	initial	qq_uart = 1'b1;
	initial	ck_uart = 1'b1;
	always @(posedge i_clk)
		{ ck_uart, qq_uart, q_uart } <= { qq_uart, q_uart, i_uart_rx };

	// Keep track of the number of clocks since the last change.
	//
	// This is used to determine if we are in either a break or an idle
	// condition, as discussed further below.
	reg	[(TB-1):0]	chg_counter;
	initial	chg_counter = {(TB){1'b1}};
	always @(posedge i_clk)
	if (qq_uart != ck_uart)
		chg_counter <= 0;
	else if (chg_counter != { (TB){1'b1} })
		chg_counter <= chg_counter + 1;

	// Are we in the middle of a baud iterval?  Specifically, are we
	// in the middle of a start bit?  Set this to high if so.  We'll use
	// this within our state machine to transition out of the IDLE
	// state.
	reg	half_baud_time;
	initial	half_baud_time = 0;
	always @(posedge i_clk)
		half_baud_time <= (!ck_uart)&&(chg_counter >= half_baud-1'b1-1'b1);


	initial	state = `RXUL_IDLE;
	always @(posedge i_clk)
	if (state == `RXUL_IDLE)
	begin // Idle state, independent of baud counter
		// By default, just stay in the IDLE state
		state <= `RXUL_IDLE;
		if ((!ck_uart)&&(half_baud_time))
			// UNLESS: We are in the center of a valid
			// start bit
			state <= `RXUL_BIT_ZERO;
	end else if ((state >= `RXUL_WAIT)&&(ck_uart))
		state <= `RXUL_IDLE;
	else if (zero_baud_counter)
	begin
		if (state <= `RXUL_STOP)
			// Data arrives least significant bit first.
			// By the time this is clocked in, it's what
			// you'll have.
			state <= state + 1;
	end

	// Data bit capture logic.
	//
	// This is drastically simplified from the state machine above, based
	// upon: 1) it doesn't matter what it is until the end of a captured
	// byte, and 2) the data register will flush itself of any invalid
	// data in all other cases.  Hence, let's keep it real simple.
	reg	[7:0]	data_reg;
	always @(posedge i_clk)
	if ((zero_baud_counter)&&(state != `RXUL_STOP))
		data_reg <= { qq_uart, data_reg[7:1] };

	// Our data bit logic doesn't need nearly the complexity of all that
	// work above.  Indeed, we only need to know if we are at the end of
	// a stop bit, in which case we copy the data_reg into our output
	// data register, o_data, and tell others (for one clock) that data is
	// available.
	//
	initial	o_wr = 1'b0;
	initial	o_data = 8'h00;
	always @(posedge i_clk)
	if ((zero_baud_counter)&&(state == `RXUL_STOP)&&(ck_uart))
	begin
		o_wr   <= 1'b1;
		o_data <= data_reg;
	end else
		o_wr   <= 1'b0;

	// The baud counter
	//
	// This is used as a "clock divider" if you will, but the clock needs
	// to be reset before any byte can be decoded.  In all other respects,
	// we set ourselves up for CLOCKS_PER_BAUD counts between baud
	// intervals.
	initial	baud_counter = 0;
	always @(posedge i_clk)
	if (((state==`RXUL_IDLE))&&(!ck_uart)&&(half_baud_time))
		baud_counter <= CLOCKS_PER_BAUD-1'b1;
	else if (state == `RXUL_WAIT)
		baud_counter <= 0;
	else if ((zero_baud_counter)&&(state < `RXUL_STOP))
		baud_counter <= CLOCKS_PER_BAUD-1'b1;
	else if (!zero_baud_counter)
		baud_counter <= baud_counter-1'b1;

	// zero_baud_counter
	//
	// Rather than testing whether or not (baud_counter == 0) within our
	// (already too complicated) state transition tables, we use
	// zero_baud_counter to pre-charge that test on the clock
	// before--cleaning up some otherwise difficult timing dependencies.
	initial	zero_baud_counter = 1'b1;
	always @(posedge i_clk)
	if ((state == `RXUL_IDLE)&&(!ck_uart)&&(half_baud_time))
		zero_baud_counter <= 1'b0;
	else if (state == `RXUL_WAIT)
		zero_baud_counter <= 1'b1;
	else if ((zero_baud_counter)&&(state < `RXUL_STOP))
		zero_baud_counter <= 1'b0;
	else if (baud_counter == 1)
		zero_baud_counter <= 1'b1;

`ifdef	FORMAL
`define	FORMAL_VERILATOR
`else
`ifdef	VERILATOR
`define	FORMAL_VERILATOR
`endif
`endif

`ifdef	FORMAL
`define ASSUME	assume
`define ASSERT	assert
`ifdef	VERIFIC
	(* gclk *) wire	gbl_clk;
	global clocking @(posedge gbl_clk); endclocking
`endif


	localparam	F_CKRES = 10;

	(* anyseq *) wire	f_tx_start;
	(* anyconst *) wire	[(F_CKRES-1):0]	f_tx_step;
	reg			f_tx_zclk;
	reg	[(TB-1):0]	f_tx_timer;
	wire	[7:0]		f_rx_newdata;
	reg	[(TB-1):0]	f_tx_baud;
	wire			f_tx_zbaud;

	wire	[(TB-1):0]	f_max_baud_difference;
	reg	[(TB-1):0]	f_baud_difference;
	reg	[(TB+3):0]	f_tx_count, f_rx_count;
	(* anyseq *) wire	[7:0]		f_tx_data;



	wire			f_txclk;
	reg	[1:0]		f_rx_clock;
	reg	[(F_CKRES-1):0]	f_tx_clock;
	reg			f_past_valid, f_past_valid_tx;

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

	initial	f_rx_clock = 3'h0;
	always @($global_clock)
		f_rx_clock <= f_rx_clock + 1'b1;

	always @(*)
		assume(i_clk == f_rx_clock[1]);
	///////////////////////////////////////////////////////////
	//
	//
	// Generate a transmitted signal
	//
	//
	///////////////////////////////////////////////////////////
	// First, calculate the transmit clock
	localparam [(F_CKRES-1):0] F_MIDSTEP = { 2'b01, {(F_CKRES-2){1'b0}} };
	//
	// Need to allow us to slip by half a baud clock over 10 baud intervals
	//
	// (F_STEP / (2^F_CKRES)) * (CLOCKS_PER_BAUD)*10 < CLOCKS_PER_BAUD/2
	// F_STEP * 2 * 10 < 2^F_CKRES
	localparam [(F_CKRES-1):0] F_HALFSTEP= F_MIDSTEP/32;
	localparam [(F_CKRES-1):0] F_MINSTEP = F_MIDSTEP - F_HALFSTEP + 1;
	localparam [(F_CKRES-1):0] F_MAXSTEP = F_MIDSTEP + F_HALFSTEP - 1;
	initial assert(F_MINSTEP <= F_MIDSTEP);
	initial assert(F_MIDSTEP <= F_MAXSTEP);
	//	assume((f_tx_step >= F_MINSTEP)&&(f_tx_step <= F_MAXSTEP));
	//
	//
	always @(*) assume((f_tx_step == F_MINSTEP)
			||(f_tx_step == F_MIDSTEP)
			||(f_tx_step == F_MAXSTEP));
	always @($global_clock)
		f_tx_clock <= f_tx_clock + f_tx_step;
	assign	f_txclk = f_tx_clock[F_CKRES-1];
	// 
	initial	f_past_valid_tx = 1'b0;
	always @(posedge f_txclk)
		f_past_valid_tx <= 1'b1;
	initial	assume(i_uart_rx);
	//////////////////////////////////////////////
	//
	//
	// Build a simulated transmitter
	//
	//
	//////////////////////////////////////////////
	//
	// First, the simulated timing generator
	// parameter	TIMER_BITS = 10;
	// parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 868;
	// localparam	TB = TIMER_BITS;
	always @(*)
	if (f_tx_busy)
		assume(!f_tx_start);
	initial	f_tx_baud = 0;
	always @(posedge f_txclk)
	if ((f_tx_zbaud)&&((f_tx_busy)||(f_tx_start)))
		f_tx_baud <= CLOCKS_PER_BAUD-1'b1;
	else if (!f_tx_zbaud)
		f_tx_baud <= f_tx_baud - 1'b1;
	always @(*)
		`ASSERT(f_tx_baud < CLOCKS_PER_BAUD);
	always @(*)
	if (!f_tx_busy)
		`ASSERT(f_tx_baud == 0);
	assign	f_tx_zbaud = (f_tx_baud == 0);
	// But only if we aren't busy
	initial	assume(f_tx_data == 0);
	always @(posedge f_txclk)
	if ((!f_tx_zbaud)||(f_tx_busy)||(!f_tx_start))
		assume(f_tx_data == $past(f_tx_data));
	// Force the data to change on a clock only
	always @($global_clock)
	if ((f_past_valid)&&(!$rose(f_txclk)))
		assume($stable(f_tx_data));
	else if (f_tx_busy)
		assume($stable(f_tx_data));
	//
	always @($global_clock)
	if ((!f_past_valid)||(!$rose(f_txclk)))
	begin
		assume($stable(f_tx_start));
		assume($stable(f_tx_data));
	end
	//
	//
	//
	reg	[9:0]	f_tx_reg;
	reg		f_tx_busy;
	// Here's the transmitter itself (roughly)
	initial	f_tx_busy   = 1'b0;
	initial	f_tx_reg    = 0;
	always @(posedge f_txclk)
	if (!f_tx_zbaud)
	begin
		`ASSERT(f_tx_busy);
	end else begin
		f_tx_reg  <= { 1'b0, f_tx_reg[9:1] };
		if (f_tx_start)
			f_tx_reg <= { 1'b1, f_tx_data, 1'b0 };
	end
	// Create a busy flag that we'll use
	always @(*)
	if (!f_tx_zbaud)
		f_tx_busy <= 1'b1;
	else if (|f_tx_reg)
		f_tx_busy <= 1'b1;
	else
		f_tx_busy <= 1'b0;
	//
	// Tie the TX register to the TX data
	always @(posedge f_txclk)
	if (f_tx_reg[9])
		`ASSERT(f_tx_reg[8:0] == { f_tx_data, 1'b0 });
	else if (f_tx_reg[8])
		`ASSERT(f_tx_reg[7:0] == f_tx_data[7:0] );
	else if (f_tx_reg[7])
		`ASSERT(f_tx_reg[6:0] == f_tx_data[7:1] );
	else if (f_tx_reg[6])
		`ASSERT(f_tx_reg[5:0] == f_tx_data[7:2] );
	else if (f_tx_reg[5])
		`ASSERT(f_tx_reg[4:0] == f_tx_data[7:3] );
	else if (f_tx_reg[4])
		`ASSERT(f_tx_reg[3:0] == f_tx_data[7:4] );
	else if (f_tx_reg[3])
		`ASSERT(f_tx_reg[2:0] == f_tx_data[7:5] );
	else if (f_tx_reg[2])
		`ASSERT(f_tx_reg[1:0] == f_tx_data[7:6] );
	else if (f_tx_reg[1])
		`ASSERT(f_tx_reg[0] == f_tx_data[7]);
	// Our counter since we start
	initial	f_tx_count = 0;
	always @(posedge f_txclk)
	if (!f_tx_busy)
		f_tx_count <= 0;
	else
		f_tx_count <= f_tx_count + 1'b1;
	always @(*)
	if (f_tx_reg == 10'h0)
		assume(i_uart_rx);
	else
		assume(i_uart_rx == f_tx_reg[0]);
	//
	// Make sure the absolute transmit clock timer matches our state
	//
	always @(posedge f_txclk)
	if (!f_tx_busy)
	begin
		if ((!f_past_valid_tx)||(!$past(f_tx_busy)))
			`ASSERT(f_tx_count == 0);
	end else if (f_tx_reg[9])
		`ASSERT(f_tx_count ==
				    CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[8])
		`ASSERT(f_tx_count ==
				2 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[7])
		`ASSERT(f_tx_count ==
				3 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[6])
		`ASSERT(f_tx_count ==
				4 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[5])
		`ASSERT(f_tx_count ==
				5 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[4])
		`ASSERT(f_tx_count ==
				6 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[3])
		`ASSERT(f_tx_count ==
				7 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[2])
		`ASSERT(f_tx_count ==
				8 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[1])
		`ASSERT(f_tx_count ==
				9 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else if (f_tx_reg[0])
		`ASSERT(f_tx_count ==
				10 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	else
		`ASSERT(f_tx_count ==
				11 * CLOCKS_PER_BAUD -1 -f_tx_baud);
	///////////////////////////////////////
	//
	// Receiver
	//
	///////////////////////////////////////
	//
	// Count RX clocks since the start of the first stop bit, measured in
	// rx clocks
	initial	f_rx_count = 0;
	always @(posedge i_clk)
	if (state == `RXUL_IDLE)
		f_rx_count = (!ck_uart) ? (chg_counter+2) : 0;
	else
		f_rx_count <= f_rx_count + 1'b1;
	always @(posedge i_clk)
	if (state == 0)
		`ASSERT(f_rx_count
				== half_baud + (CLOCKS_PER_BAUD-baud_counter));
	else if (state == 1)
		`ASSERT(f_rx_count == half_baud + 2 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 2)
		`ASSERT(f_rx_count == half_baud + 3 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 3)
		`ASSERT(f_rx_count == half_baud + 4 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 4)
		`ASSERT(f_rx_count == half_baud + 5 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 5)
		`ASSERT(f_rx_count == half_baud + 6 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 6)
		`ASSERT(f_rx_count == half_baud + 7 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 7)
		`ASSERT(f_rx_count == half_baud + 8 * CLOCKS_PER_BAUD
					- baud_counter);
	else if (state == 8)
		`ASSERT((f_rx_count == half_baud + 9 * CLOCKS_PER_BAUD
					- baud_counter)
			||(f_rx_count == half_baud + 10 * CLOCKS_PER_BAUD
					- baud_counter));
	always @(*)
		`ASSERT( ((!zero_baud_counter)
				&&(state == `RXUL_IDLE)
				&&(baud_counter == 0))
			||((zero_baud_counter)&&(baud_counter == 0))
			||((!zero_baud_counter)&&(baud_counter != 0)));
	always @(posedge i_clk)
	if (!f_past_valid)
		`ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0)
			&&(zero_baud_counter));
	always @(*)
	begin
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h2);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h4);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h5);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h6);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h9);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'ha);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hb);
		`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hd);
	end
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)&&($past(ck_uart)))
		`ASSERT(state == `RXUL_IDLE);
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)
			&&(($past(state) != `RXUL_IDLE)||(state == `RXUL_IDLE)))
		`ASSERT(zero_baud_counter);
	// Calculate an absolute value of the difference between the two baud
	// clocks
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(state)==`RXUL_IDLE)&&(state == `RXUL_IDLE))
	begin
		`ASSERT(($past(ck_uart))
			||(chg_counter <=
				{ 1'b0, CLOCKS_PER_BAUD[(TB-1):1] }));
	end
	always @(posedge f_txclk)
	if (!f_past_valid_tx)
		`ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0)
			&&(zero_baud_counter)&&(!f_tx_busy));
	wire	[(TB+3):0]	f_tx_count_two_clocks_ago;
	assign	f_tx_count_two_clocks_ago = f_tx_count - 2;
	always @(*)
	if (f_tx_count >= f_rx_count + 2)
		f_baud_difference = f_tx_count_two_clocks_ago - f_rx_count;
	else
		f_baud_difference = f_rx_count - f_tx_count_two_clocks_ago;
	localparam	F_SYNC_DLY = 8;
	reg	[(TB+4+F_CKRES-1):0]	f_sub_baud_difference;
	reg	[F_CKRES-1:0]	ck_tx_clock;
	reg	[((F_SYNC_DLY-1)*F_CKRES)-1:0]	q_tx_clock;
	reg	[TB+3:0]	ck_tx_count;
	reg	[(F_SYNC_DLY-1)*(TB+4)-1:0]	q_tx_count;
	initial	q_tx_count = 0;
	initial	ck_tx_count = 0;
	initial	q_tx_clock = 0;
	initial	ck_tx_clock = 0;
	always @($global_clock)
		{ ck_tx_clock, q_tx_clock } <= { q_tx_clock, f_tx_clock };
	always @($global_clock)
		{ ck_tx_count, q_tx_count } <= { q_tx_count, f_tx_count };
	reg	[TB+4+F_CKRES-1:0]	f_ck_tx_time, f_rx_time;
	always @(*)
		f_ck_tx_time = { ck_tx_count, !ck_tx_clock[F_CKRES-1],
						ck_tx_clock[F_CKRES-2:0] };
	always @(*)
		f_rx_time = { f_rx_count, !f_rx_clock[1], f_rx_clock[0],
						{(F_CKRES-2){1'b0}} };
	reg	[TB+4+F_CKRES-1:0]	f_signed_difference;
	always @(*)
		f_signed_difference = f_ck_tx_time - f_rx_time;
	always @(*)
	if (f_signed_difference[TB+4+F_CKRES-1])
		f_sub_baud_difference = -f_signed_difference;
	else
		f_sub_baud_difference =  f_signed_difference;
	always @($global_clock)
	if (state == `RXUL_WAIT)
		`ASSERT((!f_tx_busy)||(f_tx_reg[9:1] == 0));
	always @($global_clock)
	if (state == `RXUL_IDLE)
	begin
		`ASSERT((!f_tx_busy)||(f_tx_reg[9])||(f_tx_reg[9:1]==0));
		if (!ck_uart)
			;//`PHASE_TWO_ASSERT((f_rx_count < 4)||(f_sub_baud_difference <= ((CLOCKS_PER_BAUD<<F_CKRES)/20)));
		else
			`ASSERT((f_tx_reg[9:1]==0)||(f_tx_count < (3 + CLOCKS_PER_BAUD/2)));
	end else if (state == 0)
		`ASSERT(f_sub_baud_difference
				<=  2 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 1)
		`ASSERT(f_sub_baud_difference
				<=  3 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 2)
		`ASSERT(f_sub_baud_difference
				<=  4 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 3)
		`ASSERT(f_sub_baud_difference
				<=  5 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 4)
		`ASSERT(f_sub_baud_difference
				<=  6 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 5)
		`ASSERT(f_sub_baud_difference
				<=  7 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 6)
		`ASSERT(f_sub_baud_difference
				<=  8 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 7)
		`ASSERT(f_sub_baud_difference
				<=  9 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	else if (state == 8)
		`ASSERT(f_sub_baud_difference
				<= 10 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
	always @(posedge i_clk)
	if (o_wr)
		`ASSERT(o_data == $past(f_tx_data,4));
	// always @(posedge i_clk)
	// if ((zero_baud_counter)&&(state != 4'hf)&&(CLOCKS_PER_BAUD > 6))
		// assert(i_uart_rx == ck_uart);
	// Make sure the data register matches
	always @(posedge i_clk)
	// if ((f_past_valid)&&(state != $past(state)))
	begin
		if (state == 4'h0)
			`ASSERT(!data_reg[7]);
		if (state == 4'h1)
			`ASSERT((data_reg[7]
				== $past(f_tx_data[0]))&&(!data_reg[6]));
		if (state == 4'h2)
			`ASSERT(data_reg[7:6]
					== $past(f_tx_data[1:0]));
		if (state == 4'h3)
			`ASSERT(data_reg[7:5] == $past(f_tx_data[2:0]));
		if (state == 4'h4)
			`ASSERT(data_reg[7:4] == $past(f_tx_data[3:0]));
		if (state == 4'h5)
			`ASSERT(data_reg[7:3] == $past(f_tx_data[4:0]));
		if (state == 4'h6)
			`ASSERT(data_reg[7:2] == $past(f_tx_data[5:0]));
		if (state == 4'h7)
			`ASSERT(data_reg[7:1] == $past(f_tx_data[6:0]));
		if (state == 4'h8)
			`ASSERT(data_reg[7:0] == $past(f_tx_data[7:0]));
	end
	////////////////////////////////////////////////////////////////////////
	//
	// Cover properties
	//
	////////////////////////////////////////////////////////////////////////
	//
	always @(posedge i_clk)
		cover(o_wr); // Step 626, takes about 20mins
	always @(posedge i_clk)
	begin
		cover(!ck_uart);
		cover((f_past_valid)&&($rose(ck_uart)));               //  82
		cover((zero_baud_counter)&&(state == `RXUL_BIT_ZERO)); // 110
		cover((zero_baud_counter)&&(state == `RXUL_BIT_ONE));  // 174
		cover((zero_baud_counter)&&(state == `RXUL_BIT_TWO));  // 238
		cover((zero_baud_counter)&&(state == `RXUL_BIT_THREE));// 302
		cover((zero_baud_counter)&&(state == `RXUL_BIT_FOUR)); // 366
		cover((zero_baud_counter)&&(state == `RXUL_BIT_FIVE)); // 430
		cover((zero_baud_counter)&&(state == `RXUL_BIT_SIX));  // 494
		cover((zero_baud_counter)&&(state == `RXUL_BIT_SEVEN));// 558
		cover((zero_baud_counter)&&(state == `RXUL_STOP));     // 622
		cover((zero_baud_counter)&&(state == `RXUL_WAIT));     // 626
	end
`endif
`ifdef	FORMAL_VERILATOR
	// FORMAL properties which can be tested via Verilator as well as
	// Yosys FORMAL
	always @(*)
		assert((state == 4'hf)||(state <= `RXUL_WAIT));
	always @(*)
		assert(zero_baud_counter == (baud_counter == 0)? 1'b1:1'b0);
	always @(*)
		assert(baud_counter <= CLOCKS_PER_BAUD-1'b1);
`endif
endmodule

////////////////////////////////////////////////////////////////////////////////
//
// 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-2020, 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
//
`define	TXUL_BIT_ZERO	4'h0
`define	TXUL_BIT_ONE	4'h1
`define	TXUL_BIT_TWO	4'h2
`define	TXUL_BIT_THREE	4'h3
`define	TXUL_BIT_FOUR	4'h4
`define	TXUL_BIT_FIVE	4'h5
`define	TXUL_BIT_SIX	4'h6
`define	TXUL_BIT_SEVEN	4'h7
`define	TXUL_STOP	4'h8
`define	TXUL_IDLE	4'hf
//
//
module txuartlite(i_clk, i_wr, i_data, o_uart_tx, o_busy);
	parameter	[4:0]	TIMING_BITS = 5'd24;
	localparam		TB = TIMING_BITS;
	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;

	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)&&(state == 4'h9))
		begin
			baud_counter <= 0;
			zero_baud_counter <= 1'b1;
		end else if (!zero_baud_counter)
			baud_counter <= baud_counter - 1'b1;
		else
			baud_counter <= CLOCKS_PER_BAUD - 1'b1;
	end
	// }}}
//
//
// FORMAL METHODS
//
//
//
`ifdef	FORMAL

`ifdef	TXUARTLITE
`define	ASSUME	assume
`else
`define	ASSUME	assert
`endif

	// Setup
	// {{{
	reg	f_past_valid, f_last_clk;

	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));

	reg	[(TB-1):0]	f_baud_count;
	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);
	// }}}

	reg	[9:0]	f_txbits;
	// {{{
	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));

	reg	[3:0]	f_bitcount;
	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);

	reg	[7:0]	f_request_tx_data;
	always @(posedge i_clk)
		if ((i_wr)&&(!o_busy))
			f_request_tx_data <= i_data;

	wire	[3:0]	subcount;
	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'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)&&(o_busy)&&($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