forked from tanchou/Verilog
		
	
		
			
	
	
		
			473 lines
		
	
	
		
			14 KiB
		
	
	
	
		
			Coq
		
	
	
	
	
	
		
		
			
		
	
	
			473 lines
		
	
	
		
			14 KiB
		
	
	
	
		
			Coq
		
	
	
	
	
	
|   | //////////////////////////////////////////////////////////////////////////////// | ||
|  | // | ||
|  | // 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-2024, 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'd8, | ||
|  | 		localparam		TB = TIMING_BITS, | ||
|  | 		// CLOCKS_PER_BAUD -- the number of system clocks per baud | ||
|  | 		// interval. | ||
|  | 		parameter	[(TB-1):0]	CLOCKS_PER_BAUD = 234 // 24'd868 | ||
|  | 		// }}} | ||
|  | 	) ( | ||
|  | 		// {{{ | ||
|  | 		input	wire		i_clk, i_reset, | ||
|  | 		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 | ||
|  | 		// }}} | ||
|  | 	); | ||
|  | 
 | ||
|  | 	// 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) | ||
|  | 	if (i_reset) | ||
|  | 	begin | ||
|  | 		r_busy <= 1'b1; | ||
|  | 		state  <= TXUL_IDLE; | ||
|  | 	end else 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 | ||
|  | 	// }}} | ||
|  | 
 | ||
|  | 	// 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_reset) | ||
|  | 		lcl_data <= 8'hff; | ||
|  | 	else 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_reset) | ||
|  | 		o_uart_tx <= 1'b1; | ||
|  | 	else 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) | ||
|  | 	if (i_reset) | ||
|  | 	begin | ||
|  | 		zero_baud_counter <= 1'b1; | ||
|  | 		baud_counter <= 0; | ||
|  | 	end else 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(i_reset) && $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(i_reset) && !$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(i_reset)&& !$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 |