|
|
|
@@ -0,0 +1,472 @@
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
//
|
|
|
|
|
// 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
|