| Line 62... |
Line 62... |
`define TXUL_STOP 4'h8
|
`define TXUL_STOP 4'h8
|
`define TXUL_IDLE 4'hf
|
`define TXUL_IDLE 4'hf
|
//
|
//
|
//
|
//
|
module txuartlite(i_clk, i_wr, i_data, o_uart_tx, o_busy);
|
module txuartlite(i_clk, i_wr, i_data, o_uart_tx, o_busy);
|
parameter [23:0] CLOCKS_PER_BAUD = 24'd8; // 24'd868;
|
parameter [4:0] TIMING_BITS = 5'd24;
|
|
localparam TB = TIMING_BITS;
|
|
parameter [(TB-1):0] CLOCKS_PER_BAUD = 8; // 24'd868;
|
|
parameter [0:0] F_OPT_CLK2FFLOGIC = 1'b0;
|
input wire i_clk;
|
input wire i_clk;
|
input wire i_wr;
|
input wire i_wr;
|
input wire [7:0] i_data;
|
input wire [7:0] i_data;
|
// And the UART input line itself
|
// And the UART input line itself
|
output reg o_uart_tx;
|
output reg o_uart_tx;
|
// A line to tell others when we are ready to accept data. If
|
// 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
|
// (i_wr)&&(!o_busy) is ever true, then the core has accepted a byte
|
// for transmission.
|
// for transmission.
|
output wire o_busy;
|
output wire o_busy;
|
|
|
reg [23:0] baud_counter;
|
reg [(TB-1):0] baud_counter;
|
reg [3:0] state;
|
reg [3:0] state;
|
reg [7:0] lcl_data;
|
reg [7:0] lcl_data;
|
reg r_busy, zero_baud_counter;
|
reg r_busy, zero_baud_counter;
|
|
|
initial r_busy = 1'b1;
|
initial r_busy = 1'b1;
|
| Line 85... |
Line 88... |
always @(posedge i_clk)
|
always @(posedge i_clk)
|
begin
|
begin
|
if (!zero_baud_counter)
|
if (!zero_baud_counter)
|
// r_busy needs to be set coming into here
|
// r_busy needs to be set coming into here
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
else if (state == `TXUL_IDLE) // STATE_IDLE
|
else if (state > `TXUL_STOP) // STATE_IDLE
|
begin
|
begin
|
|
state <= `TXUL_IDLE;
|
r_busy <= 1'b0;
|
r_busy <= 1'b0;
|
if ((i_wr)&&(!r_busy))
|
if ((i_wr)&&(!r_busy))
|
begin // Immediately start us off with a start bit
|
begin // Immediately start us off with a start bit
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
state <= `TXUL_BIT_ZERO;
|
state <= `TXUL_BIT_ZERO;
|
end
|
end
|
end else begin
|
end else begin
|
// One clock tick in each of these states ...
|
// One clock tick in each of these states ...
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
if (state <=`TXUL_STOP) // start bit, 8-d bits, stop-b
|
if (state <=`TXUL_STOP) // start bit, 8-d bits, stop-b
|
state <= state + 1;
|
state <= state + 1'b1;
|
else
|
else
|
state <= `TXUL_IDLE;
|
state <= `TXUL_IDLE;
|
end
|
end
|
end
|
end
|
|
|
| Line 182... |
Line 186... |
// to the number of CLOCKS_PER_BAUD, and zero_baud_counter set to zero.
|
// 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
|
// 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
|
// above condition when zero_baud_counter is false--so as to make
|
// certain the STOP bit is complete.
|
// certain the STOP bit is complete.
|
initial zero_baud_counter = 1'b0;
|
initial zero_baud_counter = 1'b1;
|
initial baud_counter = 24'h05;
|
initial baud_counter = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
begin
|
begin
|
zero_baud_counter <= (baud_counter == 24'h01);
|
zero_baud_counter <= (baud_counter == 24'h01);
|
if (state == `TXUL_IDLE)
|
if (state == `TXUL_IDLE)
|
begin
|
begin
|
| Line 196... |
Line 200... |
if ((i_wr)&&(!r_busy))
|
if ((i_wr)&&(!r_busy))
|
begin
|
begin
|
baud_counter <= CLOCKS_PER_BAUD - 24'h01;
|
baud_counter <= CLOCKS_PER_BAUD - 24'h01;
|
zero_baud_counter <= 1'b0;
|
zero_baud_counter <= 1'b0;
|
end
|
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)
|
end else if (!zero_baud_counter)
|
baud_counter <= baud_counter - 24'h01;
|
baud_counter <= baud_counter - 24'h01;
|
else
|
else
|
baud_counter <= CLOCKS_PER_BAUD - 24'h01;
|
baud_counter <= CLOCKS_PER_BAUD - 24'h01;
|
end
|
end
|
| Line 220... |
Line 228... |
|
|
// Setup
|
// Setup
|
|
|
reg f_past_valid, f_last_clk;
|
reg f_past_valid, f_last_clk;
|
|
|
|
generate if (F_OPT_CLK2FFLOGIC)
|
|
begin
|
|
|
always @($global_clock)
|
always @($global_clock)
|
begin
|
begin
|
restrict(i_clk == !f_last_clk);
|
restrict(i_clk == !f_last_clk);
|
f_last_clk <= i_clk;
|
f_last_clk <= i_clk;
|
if (!$rose(i_clk))
|
if (!$rose(i_clk))
|
| Line 231... |
Line 242... |
`ASSUME($stable(i_wr));
|
`ASSUME($stable(i_wr));
|
`ASSUME($stable(i_data));
|
`ASSUME($stable(i_data));
|
end
|
end
|
end
|
end
|
|
|
|
end endgenerate
|
|
|
initial f_past_valid = 1'b0;
|
initial f_past_valid = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
f_past_valid <= 1'b1;
|
f_past_valid <= 1'b1;
|
|
|
|
initial `ASSUME(!i_wr);
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_wr))&&($past(o_busy)))
|
if ((f_past_valid)&&($past(i_wr))&&($past(o_busy)))
|
begin
|
begin
|
`ASSUME(i_wr == $past(i_wr));
|
`ASSUME(i_wr == $past(i_wr));
|
`ASSUME(i_data == $past(i_data));
|
`ASSUME(i_data == $past(i_data));
|
end
|
end
|
|
|
// Check the baud counter
|
// Check the baud counter
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (zero_baud_counter)
|
assert(zero_baud_counter == (baud_counter == 0));
|
assert(baud_counter == 0);
|
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(baud_counter != 0))&&($past(state != `TXUL_IDLE)))
|
if ((f_past_valid)&&($past(baud_counter != 0))&&($past(state != `TXUL_IDLE)))
|
assert(baud_counter == $past(baud_counter - 1'b1));
|
assert(baud_counter == $past(baud_counter - 1'b1));
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&(!$past(zero_baud_counter))&&($past(state != `TXUL_IDLE)))
|
if ((f_past_valid)&&(!$past(zero_baud_counter))&&($past(state != `TXUL_IDLE)))
|
assert($stable(o_uart_tx));
|
assert($stable(o_uart_tx));
|
|
|
reg [23:0] f_baud_count;
|
reg [(TB-1):0] f_baud_count;
|
initial f_baud_count = 1'b0;
|
initial f_baud_count = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (zero_baud_counter)
|
if (zero_baud_counter)
|
f_baud_count <= 0;
|
f_baud_count <= 0;
|
else
|
else
|
| Line 276... |
Line 289... |
initial f_txbits = 0;
|
initial f_txbits = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (zero_baud_counter)
|
if (zero_baud_counter)
|
f_txbits <= { o_uart_tx, f_txbits[9:1] };
|
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;
|
reg [3:0] f_bitcount;
|
initial f_bitcount = 0;
|
initial f_bitcount = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
//if (baud_counter == CLOCKS_PER_BAUD - 24'h01)
|
|
//f_bitcount <= f_bitcount + 1'b1;
|
|
if ((!f_past_valid)||(!$past(f_past_valid)))
|
if ((!f_past_valid)||(!$past(f_past_valid)))
|
f_bitcount <= 0;
|
f_bitcount <= 0;
|
else if ((state == `TXUL_IDLE)&&(zero_baud_counter))
|
else if ((state == `TXUL_IDLE)&&(zero_baud_counter))
|
f_bitcount <= 0;
|
f_bitcount <= 0;
|
else if (zero_baud_counter)
|
else if (zero_baud_counter)
|
| Line 301... |
Line 317... |
wire [3:0] subcount;
|
wire [3:0] subcount;
|
assign subcount = 10-f_bitcount;
|
assign subcount = 10-f_bitcount;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (f_bitcount > 0)
|
if (f_bitcount > 0)
|
assert(!f_txbits[subcount]);
|
assert(!f_txbits[subcount]);
|
/*
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_bitcount > 2)&&(f_bitcount <= 10))
|
|
assert(f_txbits[f_bitcount-2:0]
|
|
== f_request_tx_data[7:(9-f_bitcount)]);
|
|
*/
|
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (f_bitcount == 4'ha)
|
if (f_bitcount == 4'ha)
|
begin
|
begin
|
assert(f_txbits[8:1] == f_request_tx_data);
|
assert(f_txbits[8:1] == f_request_tx_data);
|
assert( f_txbits[9]);
|
assert( f_txbits[9]);
|
end
|
end
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
assert((state <= `TXUL_STOP + 1'b1)||(state == `TXUL_IDLE));
|
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;
|
|
|
`endif // FORMAL
|
//
|
|
// 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
|
endmodule
|
|
|
|
|
No newline at end of file
|
No newline at end of file
|
