| Line 67... |
Line 67... |
// Creator: Dan Gisselquist, Ph.D.
|
// Creator: Dan Gisselquist, Ph.D.
|
// Gisselquist Technology, LLC
|
// Gisselquist Technology, LLC
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
|
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
|
//
|
//
|
// This program is free software (firmware): you can redistribute it and/or
|
// 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
|
// 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
|
// by the Free Software Foundation, either version 3 of the License, or (at
|
// your option) any later version.
|
// your option) any later version.
|
| Line 93... |
Line 93... |
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
`default_nettype none
|
`default_nettype none
|
//
|
//
|
`define TXU_BIT_ZERO 4'h0
|
|
`define TXU_BIT_ONE 4'h1
|
|
`define TXU_BIT_TWO 4'h2
|
|
`define TXU_BIT_THREE 4'h3
|
|
`define TXU_BIT_FOUR 4'h4
|
|
`define TXU_BIT_FIVE 4'h5
|
|
`define TXU_BIT_SIX 4'h6
|
|
`define TXU_BIT_SEVEN 4'h7
|
|
`define TXU_PARITY 4'h8 // Constant 1
|
|
`define TXU_STOP 4'h9 // Constant 1
|
|
`define TXU_SECOND_STOP 4'ha
|
|
// 4'hb // Unused
|
|
// 4'hc // Unused
|
|
// `define TXU_START 4'hd // An unused state
|
|
`define TXU_BREAK 4'he
|
|
`define TXU_IDLE 4'hf
|
|
//
|
|
//
|
//
|
module txuart(i_clk, i_reset, i_setup, i_break, i_wr, i_data,
|
module txuart(i_clk, i_reset, i_setup, i_break, i_wr, i_data,
|
i_cts_n, o_uart_tx, o_busy);
|
i_cts_n, o_uart_tx, o_busy);
|
parameter [30:0] INITIAL_SETUP = 31'd868;
|
parameter [30:0] INITIAL_SETUP = 31'd868;
|
|
//
|
|
localparam [3:0] TXU_BIT_ZERO = 4'h0;
|
|
localparam [3:0] TXU_BIT_ONE = 4'h1;
|
|
localparam [3:0] TXU_BIT_TWO = 4'h2;
|
|
localparam [3:0] TXU_BIT_THREE = 4'h3;
|
|
localparam [3:0] TXU_BIT_FOUR = 4'h4;
|
|
localparam [3:0] TXU_BIT_FIVE = 4'h5;
|
|
localparam [3:0] TXU_BIT_SIX = 4'h6;
|
|
localparam [3:0] TXU_BIT_SEVEN = 4'h7;
|
|
localparam [3:0] TXU_PARITY = 4'h8;
|
|
localparam [3:0] TXU_STOP = 4'h9;
|
|
localparam [3:0] TXU_SECOND_STOP = 4'ha;
|
|
//
|
|
localparam [3:0] TXU_BREAK = 4'he;
|
|
localparam [3:0] TXU_IDLE = 4'hf;
|
|
//
|
|
//
|
input wire i_clk, i_reset;
|
input wire i_clk, i_reset;
|
input wire [30:0] i_setup;
|
input wire [30:0] i_setup;
|
input wire i_break;
|
input wire i_break;
|
input wire i_wr;
|
input wire i_wr;
|
input wire [7:0] i_data;
|
input wire [7:0] i_data;
|
| Line 131... |
Line 131... |
// (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;
|
|
|
wire [27:0] clocks_per_baud, break_condition;
|
wire [27:0] clocks_per_baud, break_condition;
|
wire [1:0] data_bits;
|
wire [1:0] i_data_bits, data_bits;
|
wire use_parity, parity_even, dblstop, fixd_parity,
|
wire use_parity, parity_odd, dblstop, fixd_parity,
|
fixdp_value, hw_flow_control;
|
fixdp_value, hw_flow_control, i_parity_odd;
|
reg [30:0] r_setup;
|
reg [30:0] r_setup;
|
assign clocks_per_baud = { 4'h0, r_setup[23:0] };
|
assign clocks_per_baud = { 4'h0, r_setup[23:0] };
|
assign break_condition = { r_setup[23:0], 4'h0 };
|
assign break_condition = { r_setup[23:0], 4'h0 };
|
assign hw_flow_control = !r_setup[30];
|
assign hw_flow_control = !r_setup[30];
|
|
assign i_data_bits = i_setup[29:28];
|
assign data_bits = r_setup[29:28];
|
assign data_bits = r_setup[29:28];
|
assign dblstop = r_setup[27];
|
assign dblstop = r_setup[27];
|
assign use_parity = r_setup[26];
|
assign use_parity = r_setup[26];
|
assign fixd_parity = r_setup[25];
|
assign fixd_parity = r_setup[25];
|
assign parity_even = r_setup[24];
|
assign i_parity_odd = i_setup[24];
|
|
assign parity_odd = r_setup[24];
|
assign fixdp_value = r_setup[24];
|
assign fixdp_value = r_setup[24];
|
|
|
reg [27:0] baud_counter;
|
reg [27:0] baud_counter;
|
reg [3:0] state;
|
reg [3:0] state;
|
reg [7:0] lcl_data;
|
reg [7:0] lcl_data;
|
reg calc_parity, r_busy, zero_baud_counter;
|
reg calc_parity, r_busy, zero_baud_counter, last_state;
|
|
|
|
|
// First step ... handle any hardware flow control, if so enabled.
|
// First step ... handle any hardware flow control, if so enabled.
|
//
|
//
|
// Clock in the flow control data, two clocks to avoid metastability
|
// Clock in the flow control data, two clocks to avoid metastability
|
| Line 167... |
Line 169... |
//
|
//
|
// initial q_cts_n = 1'b1;
|
// initial q_cts_n = 1'b1;
|
// initial qq_cts_n = 1'b1;
|
// initial qq_cts_n = 1'b1;
|
// initial ck_cts = 1'b0;
|
// initial ck_cts = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
q_cts_n <= i_cts_n;
|
{ qq_cts_n, q_cts_n } <= { q_cts_n, i_cts_n };
|
always @(posedge i_clk)
|
|
qq_cts_n <= q_cts_n;
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
ck_cts <= (!qq_cts_n)||(!hw_flow_control);
|
ck_cts <= (!qq_cts_n)||(!hw_flow_control);
|
|
|
initial o_uart_tx = 1'b1;
|
initial o_uart_tx = 1'b1;
|
initial r_busy = 1'b1;
|
initial r_busy = 1'b1;
|
initial state = `TXU_IDLE;
|
initial state = TXU_IDLE;
|
initial lcl_data= 8'h0;
|
|
initial calc_parity = 1'b0;
|
|
// initial baud_counter = clocks_per_baud;//ILLEGAL--not constant
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
begin
|
|
if (i_reset)
|
if (i_reset)
|
begin
|
begin
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
state <= `TXU_IDLE;
|
state <= TXU_IDLE;
|
end else if (i_break)
|
end else if (i_break)
|
begin
|
begin
|
state <= `TXU_BREAK;
|
state <= TXU_BREAK;
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
end else if (!zero_baud_counter)
|
end else if (!zero_baud_counter)
|
begin // r_busy needs to be set coming into here
|
begin // r_busy needs to be set coming into here
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
end else if (state == `TXU_BREAK)
|
end else if (state == TXU_BREAK)
|
begin
|
begin
|
state <= `TXU_IDLE;
|
state <= TXU_IDLE;
|
r_busy <= 1'b1;
|
r_busy <= !ck_cts;
|
end else if (state == `TXU_IDLE) // STATE_IDLE
|
end else if (state == TXU_IDLE) // STATE_IDLE
|
begin
|
begin
|
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;
|
case(data_bits)
|
case(i_data_bits)
|
2'b00: state <= `TXU_BIT_ZERO;
|
2'b00: state <= TXU_BIT_ZERO;
|
2'b01: state <= `TXU_BIT_ONE;
|
2'b01: state <= TXU_BIT_ONE;
|
2'b10: state <= `TXU_BIT_TWO;
|
2'b10: state <= TXU_BIT_TWO;
|
2'b11: state <= `TXU_BIT_THREE;
|
2'b11: state <= TXU_BIT_THREE;
|
endcase
|
endcase
|
end else begin // Stay in idle
|
end else begin // Stay in idle
|
r_busy <= !ck_cts;
|
r_busy <= !ck_cts;
|
end
|
end
|
end else begin
|
end else begin
|
// One clock tick in each of these states ...
|
// One clock tick in each of these states ...
|
// baud_counter <= clocks_per_baud - 28'h01;
|
// baud_counter <= clocks_per_baud - 28'h01;
|
r_busy <= 1'b1;
|
r_busy <= 1'b1;
|
if (state[3] == 0) // First 8 bits
|
if (state[3] == 0) // First 8 bits
|
begin
|
begin
|
if (state == `TXU_BIT_SEVEN)
|
if (state == TXU_BIT_SEVEN)
|
state <= (use_parity)?`TXU_PARITY:`TXU_STOP;
|
state <= (use_parity)? TXU_PARITY:TXU_STOP;
|
else
|
else
|
state <= state + 1'b1;
|
state <= state + 1;
|
end else if (state == `TXU_PARITY)
|
end else if (state == TXU_PARITY)
|
begin
|
begin
|
state <= `TXU_STOP;
|
state <= TXU_STOP;
|
end else if (state == `TXU_STOP)
|
end else if (state == TXU_STOP)
|
begin // two stop bit(s)
|
begin // two stop bit(s)
|
if (dblstop)
|
if (dblstop)
|
state <= `TXU_SECOND_STOP;
|
state <= TXU_SECOND_STOP;
|
else
|
else
|
state <= `TXU_IDLE;
|
state <= TXU_IDLE;
|
end else // `TXU_SECOND_STOP and default:
|
end else // `TXU_SECOND_STOP and default:
|
begin
|
begin
|
state <= `TXU_IDLE; // Go back to idle
|
state <= TXU_IDLE; // Go back to idle
|
// Still r_busy, since we need to wait
|
// Still r_busy, since we need to wait
|
// for the baud clock to finish counting
|
// for the baud clock to finish counting
|
// out this last bit.
|
// out this last bit.
|
end
|
end
|
end
|
end
|
end
|
|
|
|
// o_busy
|
// o_busy
|
//
|
//
|
// This is a wire, designed to be true is we are ever busy above.
|
// 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
|
// originally, this was going to be true if we were ever not in the
|
| Line 257... |
Line 252... |
// broken out up top, and indicate what 1) our baud rate is, 2) our
|
// broken out up top, and indicate what 1) our baud rate is, 2) our
|
// number of stop bits, 3) what type of parity we are using, and 4)
|
// number of stop bits, 3) what type of parity we are using, and 4)
|
// the size of our data word.
|
// the size of our data word.
|
initial r_setup = INITIAL_SETUP;
|
initial r_setup = INITIAL_SETUP;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (state == `TXU_IDLE)
|
if (!o_busy)
|
r_setup <= i_setup;
|
r_setup <= i_setup;
|
|
|
// lcl_data
|
// lcl_data
|
//
|
//
|
// This is our working copy of the i_data register which we use
|
// This is our working copy of the i_data register which we use
|
| Line 269... |
Line 264... |
// allowed to be whatever at any other time. Hence, if r_busy isn't
|
// 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, 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.
|
// 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)
|
// Then, on any zero_baud_counter (i.e. change between baud intervals)
|
// we simple logically shift the register right to grab the next bit.
|
// we simple logically shift the register right to grab the next bit.
|
|
initial lcl_data = 8'hff;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!r_busy)
|
if (!r_busy)
|
lcl_data <= i_data;
|
lcl_data <= i_data;
|
else if (zero_baud_counter)
|
else if (zero_baud_counter)
|
lcl_data <= { 1'b0, lcl_data[7:1] };
|
lcl_data <= { 1'b0, lcl_data[7:1] };
|
| Line 298... |
Line 294... |
else if ((i_break)||((i_wr)&&(!r_busy)))
|
else if ((i_break)||((i_wr)&&(!r_busy)))
|
o_uart_tx <= 1'b0;
|
o_uart_tx <= 1'b0;
|
else if (zero_baud_counter)
|
else if (zero_baud_counter)
|
casez(state)
|
casez(state)
|
4'b0???: o_uart_tx <= lcl_data[0];
|
4'b0???: o_uart_tx <= lcl_data[0];
|
`TXU_PARITY: o_uart_tx <= calc_parity;
|
TXU_PARITY: o_uart_tx <= calc_parity;
|
default: o_uart_tx <= 1'b1;
|
default: o_uart_tx <= 1'b1;
|
endcase
|
endcase
|
|
|
|
|
// calc_parity
|
// calc_parity
|
//
|
//
|
// Calculate the parity to be placed into the parity bit. If the
|
// Calculate the parity to be placed into the parity bit. If the
|
// parity is fixed, then the parity bit is given by the fixed parity
|
// parity is fixed, then the parity bit is given by the fixed parity
|
// value (r_setup[24]). Otherwise the parity is given by the GF2
|
// value (r_setup[24]). Otherwise the parity is given by the GF2
|
// sum of all the data bits (plus one for even parity).
|
// sum of all the data bits (plus one for even parity).
|
|
initial calc_parity = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (fixd_parity)
|
if (!o_busy)
|
|
calc_parity <= i_setup[24];
|
|
else if (fixd_parity)
|
calc_parity <= fixdp_value;
|
calc_parity <= fixdp_value;
|
else if (zero_baud_counter)
|
else if (zero_baud_counter)
|
begin
|
begin
|
if (state[3] == 0) // First 8 bits of msg
|
if (state[3] == 0) // First 8 bits of msg
|
calc_parity <= calc_parity ^ lcl_data[0];
|
calc_parity <= calc_parity ^ lcl_data[0];
|
else
|
else if (state == TXU_IDLE)
|
calc_parity <= parity_even;
|
calc_parity <= parity_odd;
|
end else if (!r_busy)
|
end else if (!r_busy)
|
calc_parity <= parity_even;
|
calc_parity <= parity_odd;
|
|
|
|
|
// All of the above logic is driven by the baud counter. Bits must last
|
// 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
|
// clocks_per_baud in length, and this baud counter is what we use to
|
// make certain of that.
|
// make certain of that.
|
| Line 354... |
Line 353... |
// 3. In the idle state, we stop our counter--so that upon a request
|
// 3. In the idle state, we stop our counter--so that upon a request
|
// to transmit when idle we can start transmitting immediately, rather
|
// to transmit when idle we can start transmitting immediately, rather
|
// than waiting for the end of the next (fictitious and arbitrary) baud
|
// than waiting for the end of the next (fictitious and arbitrary) baud
|
// interval.
|
// interval.
|
//
|
//
|
// When (i_wr)&&(!r_busy)&&(state == `TXU_IDLE) then we're not only in
|
// When (i_wr)&&(!r_busy)&&(state == TXU_IDLE) then we're not only in
|
// the idle state, but we also just accepted a command to start writing
|
// 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
|
// 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.
|
// 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
|
| Line 374... |
Line 373... |
// Give ourselves 16 bauds before being ready
|
// Give ourselves 16 bauds before being ready
|
baud_counter <= break_condition;
|
baud_counter <= break_condition;
|
zero_baud_counter <= 1'b0;
|
zero_baud_counter <= 1'b0;
|
end else if (!zero_baud_counter)
|
end else if (!zero_baud_counter)
|
baud_counter <= baud_counter - 28'h01;
|
baud_counter <= baud_counter - 28'h01;
|
else if (state == `TXU_BREAK)
|
else if (state == TXU_BREAK)
|
// Give us four idle baud intervals before becoming
|
begin
|
// available
|
baud_counter <= 0;
|
baud_counter <= clocks_per_baud<<2;
|
zero_baud_counter <= 1'b1;
|
else if (state == `TXU_IDLE)
|
end else if (state == TXU_IDLE)
|
begin
|
begin
|
baud_counter <= 28'h0;
|
baud_counter <= 28'h0;
|
zero_baud_counter <= 1'b1;
|
zero_baud_counter <= 1'b1;
|
if ((i_wr)&&(!r_busy))
|
if ((i_wr)&&(!r_busy))
|
begin
|
begin
|
baud_counter <= clocks_per_baud - 28'h01;
|
baud_counter <= { 4'h0, i_setup[23:0]} - 28'h01;
|
zero_baud_counter <= 1'b0;
|
zero_baud_counter <= 1'b0;
|
end
|
end
|
end else
|
end else if (last_state)
|
|
baud_counter <= clocks_per_baud - 28'h02;
|
|
else
|
baud_counter <= clocks_per_baud - 28'h01;
|
baud_counter <= clocks_per_baud - 28'h01;
|
end
|
end
|
|
|
|
initial last_state = 1'b0;
|
|
always @(posedge i_clk)
|
|
if (dblstop)
|
|
last_state <= (state == TXU_SECOND_STOP);
|
|
else
|
|
last_state <= (state == TXU_STOP);
|
|
|
`ifdef FORMAL
|
`ifdef FORMAL
|
reg fsv_parity;
|
reg fsv_parity;
|
reg [30:0] fsv_setup;
|
reg [30:0] fsv_setup;
|
reg [7:0] fsv_data;
|
reg [7:0] fsv_data;
|
|
reg f_past_valid;
|
|
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
f_past_valid <= 1'b1;
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_wr)&&(!o_busy))
|
if ((i_wr)&&(!o_busy))
|
fsv_data <= i_data;
|
fsv_data <= i_data;
|
|
|
|
initial fsv_setup = INITIAL_SETUP;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_wr)&&(!o_busy))
|
if (!o_busy)
|
fsv_setup <= i_setup;
|
fsv_setup <= i_setup;
|
|
|
|
always @(*)
|
|
assert(r_setup == fsv_setup);
|
|
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
assert(zero_baud_counter == (baud_counter == 0));
|
assert(zero_baud_counter == (baud_counter == 0));
|
|
|
always @(*)
|
always @(*)
|
assume(i_setup[21:0] >= 2);
|
if (!o_busy)
|
always @(*)
|
assert(zero_baud_counter);
|
assume(i_setup[21:0] <= 16);
|
|
|
/*
|
|
*
|
|
* Will only pass if !i_break && !i_reset, otherwise the setup can
|
|
* change in the middle of this operation
|
|
*
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_break))
|
|
&&(($past(o_busy))||($past(i_wr))))
|
|
assert(baud_counter <= { fsv_setup[23:0], 4'h0 });
|
|
*/
|
|
|
// A single baud interval
|
// A single baud interval
|
sequence BAUD_INTERVAL(DAT, SR, ST);
|
always @(posedge i_clk)
|
((o_uart_tx == DAT)&&(state == ST)
|
if ((f_past_valid)&&(!$past(zero_baud_counter))
|
&&(lcl_data == SR)
|
&&(!$past(i_reset))&&(!$past(i_break)))
|
&&(baud_counter == fsv_setup[21:0]-1)
|
begin
|
&&(!zero_baud_counter))
|
assert($stable(o_uart_tx));
|
##1 ((o_uart_tx == DAT)&&(state == ST)
|
assert($stable(state));
|
&&(lcl_data == SR)
|
assert($stable(lcl_data));
|
&&(baud_counter == $past(baud_counter)-1)
|
if ((state != TXU_IDLE)&&(state != TXU_BREAK))
|
&&(baud_counter > 0)
|
assert($stable(calc_parity));
|
&&(baud_counter < fsv_setup[21:0])
|
assert(baud_counter == $past(baud_counter)-1'b1);
|
&&(!zero_baud_counter))[*0:$]
|
end
|
##1 (o_uart_tx == DAT)&&(state == ST)
|
|
&&(lcl_data == SR)
|
//
|
&&(zero_baud_counter);
|
// Our various sequence data declarations
|
endsequence
|
reg [5:0] f_five_seq;
|
|
reg [6:0] f_six_seq;
|
|
reg [7:0] f_seven_seq;
|
|
reg [8:0] f_eight_seq;
|
|
reg [2:0] f_stop_seq; // parity bit, stop bit, double stop bit
|
|
|
|
|
//
|
//
|
// One byte transmitted
|
// One byte transmitted
|
//
|
//
|
// DATA = the byte that is sent
|
// DATA = the byte that is sent
|
// CKS = the number of clocks per bit
|
// CKS = the number of clocks per bit
|
//
|
//
|
sequence SEND5(DATA);
|
////////////////////////////////////////////////////////////////////////
|
BAUD_INTERVAL(1'b0, DATA, 4'h3)
|
//
|
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h4)
|
// Five bit data
|
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h5)
|
//
|
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h6)
|
////////////////////////////////////////////////////////////////////////
|
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h7)
|
|
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h8);
|
initial f_five_seq = 0;
|
endsequence
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_break))
|
sequence SEND6(DATA);
|
f_five_seq = 0;
|
BAUD_INTERVAL(1'b0, DATA, 4'h2)
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h3)
|
&&(i_data_bits == 2'b11)) // five data bits
|
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h4)
|
f_five_seq <= 1;
|
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h5)
|
else if (zero_baud_counter)
|
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h6)
|
f_five_seq <= f_five_seq << 1;
|
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h7)
|
|
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h8);
|
always @(*)
|
endsequence
|
if (|f_five_seq)
|
|
begin
|
sequence SEND7(DATA);
|
assert(fsv_setup[29:28] == data_bits);
|
BAUD_INTERVAL(1'b0, DATA, 4'h1)
|
assert(data_bits == 2'b11);
|
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h2)
|
assert(baud_counter < fsv_setup[23:0]);
|
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h3)
|
|
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h4)
|
assert(1'b0 == |f_six_seq);
|
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h5)
|
assert(1'b0 == |f_seven_seq);
|
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h6)
|
assert(1'b0 == |f_eight_seq);
|
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h7)
|
assert(r_busy);
|
##1 BAUD_INTERVAL(DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h8);
|
assert(state > 4'h2);
|
endsequence
|
end
|
|
|
sequence SEND8(DATA);
|
always @(*)
|
BAUD_INTERVAL(1'b0, DATA, 4'h0)
|
case(f_five_seq)
|
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h1)
|
6'h00: begin assert(1); end
|
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h2)
|
6'h01: begin
|
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h3)
|
assert(state == 4'h3);
|
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h4)
|
assert(o_uart_tx == 1'b0);
|
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h5)
|
assert(lcl_data[4:0] == fsv_data[4:0]);
|
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h6)
|
if (!fixd_parity)
|
##1 BAUD_INTERVAL(DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h7)
|
assert(calc_parity == parity_odd);
|
##1 BAUD_INTERVAL(DATA[7], 8'hff, 4'h8);
|
end
|
endsequence
|
6'h02: begin
|
|
assert(state == 4'h4);
|
|
assert(o_uart_tx == fsv_data[0]);
|
|
assert(lcl_data[3:0] == fsv_data[4:1]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
|
end
|
|
6'h04: begin
|
|
assert(state == 4'h5);
|
|
assert(o_uart_tx == fsv_data[1]);
|
|
assert(lcl_data[2:0] == fsv_data[4:2]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
|
end
|
|
6'h08: begin
|
|
assert(state == 4'h6);
|
|
assert(o_uart_tx == fsv_data[2]);
|
|
assert(lcl_data[1:0] == fsv_data[4:3]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
|
end
|
|
6'h10: begin
|
|
assert(state == 4'h7);
|
|
assert(o_uart_tx == fsv_data[3]);
|
|
assert(lcl_data[0] == fsv_data[4]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
|
end
|
|
6'h20: begin
|
|
if (use_parity)
|
|
assert(state == 4'h8);
|
|
else
|
|
assert(state == 4'h9);
|
|
assert(o_uart_tx == fsv_data[4]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[4:0]) ^ parity_odd);
|
|
end
|
|
default: begin assert(0); end
|
|
endcase
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Six bit data
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
initial f_six_seq = 0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_break))
|
|
f_six_seq = 0;
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
|
&&(i_data_bits == 2'b10)) // six data bits
|
|
f_six_seq <= 1;
|
|
else if (zero_baud_counter)
|
|
f_six_seq <= f_six_seq << 1;
|
|
|
|
always @(*)
|
|
if (|f_six_seq)
|
|
begin
|
|
assert(fsv_setup[29:28] == 2'b10);
|
|
assert(fsv_setup[29:28] == data_bits);
|
|
assert(baud_counter < fsv_setup[23:0]);
|
|
|
|
assert(1'b0 == |f_five_seq);
|
|
assert(1'b0 == |f_seven_seq);
|
|
assert(1'b0 == |f_eight_seq);
|
|
assert(r_busy);
|
|
assert(state > 4'h1);
|
|
end
|
|
|
|
always @(*)
|
|
case(f_six_seq)
|
|
7'h00: begin assert(1); end
|
|
7'h01: begin
|
|
assert(state == 4'h2);
|
|
assert(o_uart_tx == 1'b0);
|
|
assert(lcl_data[5:0] == fsv_data[5:0]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == parity_odd);
|
|
end
|
|
7'h02: begin
|
|
assert(state == 4'h3);
|
|
assert(o_uart_tx == fsv_data[0]);
|
|
assert(lcl_data[4:0] == fsv_data[5:1]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
|
end
|
|
7'h04: begin
|
|
assert(state == 4'h4);
|
|
assert(o_uart_tx == fsv_data[1]);
|
|
assert(lcl_data[3:0] == fsv_data[5:2]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
|
end
|
|
7'h08: begin
|
|
assert(state == 4'h5);
|
|
assert(o_uart_tx == fsv_data[2]);
|
|
assert(lcl_data[2:0] == fsv_data[5:3]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
|
end
|
|
7'h10: begin
|
|
assert(state == 4'h6);
|
|
assert(o_uart_tx == fsv_data[3]);
|
|
assert(lcl_data[1:0] == fsv_data[5:4]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
|
end
|
|
7'h20: begin
|
|
assert(state == 4'h7);
|
|
assert(lcl_data[0] == fsv_data[5]);
|
|
assert(o_uart_tx == fsv_data[4]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[4:0]) ^ parity_odd));
|
|
end
|
|
7'h40: begin
|
|
if (use_parity)
|
|
assert(state == 4'h8);
|
|
else
|
|
assert(state == 4'h9);
|
|
assert(o_uart_tx == fsv_data[5]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[5:0]) ^ parity_odd));
|
|
end
|
|
default: begin if (f_past_valid) assert(0); end
|
|
endcase
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Seven bit data
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
initial f_seven_seq = 0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_break))
|
|
f_seven_seq = 0;
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
|
&&(i_data_bits == 2'b01)) // seven data bits
|
|
f_seven_seq <= 1;
|
|
else if (zero_baud_counter)
|
|
f_seven_seq <= f_seven_seq << 1;
|
|
|
|
always @(*)
|
|
if (|f_seven_seq)
|
|
begin
|
|
assert(fsv_setup[29:28] == 2'b01);
|
|
assert(fsv_setup[29:28] == data_bits);
|
|
assert(baud_counter < fsv_setup[23:0]);
|
|
|
|
assert(1'b0 == |f_five_seq);
|
|
assert(1'b0 == |f_six_seq);
|
|
assert(1'b0 == |f_eight_seq);
|
|
assert(r_busy);
|
|
assert(state != 4'h0);
|
|
end
|
|
|
|
always @(*)
|
|
case(f_seven_seq)
|
|
8'h00: begin assert(1); end
|
|
8'h01: begin
|
|
assert(state == 4'h1);
|
|
assert(o_uart_tx == 1'b0);
|
|
assert(lcl_data[6:0] == fsv_data[6:0]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == parity_odd);
|
|
end
|
|
8'h02: begin
|
|
assert(state == 4'h2);
|
|
assert(o_uart_tx == fsv_data[0]);
|
|
assert(lcl_data[5:0] == fsv_data[6:1]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
|
end
|
|
8'h04: begin
|
|
assert(state == 4'h3);
|
|
assert(o_uart_tx == fsv_data[1]);
|
|
assert(lcl_data[4:0] == fsv_data[6:2]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
|
end
|
|
8'h08: begin
|
|
assert(state == 4'h4);
|
|
assert(o_uart_tx == fsv_data[2]);
|
|
assert(lcl_data[3:0] == fsv_data[6:3]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
|
end
|
|
8'h10: begin
|
|
assert(state == 4'h5);
|
|
assert(o_uart_tx == fsv_data[3]);
|
|
assert(lcl_data[2:0] == fsv_data[6:4]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
|
end
|
|
8'h20: begin
|
|
assert(state == 4'h6);
|
|
assert(o_uart_tx == fsv_data[4]);
|
|
assert(lcl_data[1:0] == fsv_data[6:5]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[4:0]) ^ parity_odd));
|
|
end
|
|
8'h40: begin
|
|
assert(state == 4'h7);
|
|
assert(lcl_data[0] == fsv_data[6]);
|
|
assert(o_uart_tx == fsv_data[5]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[5:0]) ^ parity_odd));
|
|
end
|
|
8'h80: begin
|
|
if (use_parity)
|
|
assert(state == 4'h8);
|
|
else
|
|
assert(state == 4'h9);
|
|
assert(o_uart_tx == fsv_data[6]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[6:0]) ^ parity_odd));
|
|
end
|
|
default: begin if (f_past_valid) assert(0); end
|
|
endcase
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Eight bit data
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
initial f_eight_seq = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_break))
|
|
f_eight_seq = 0;
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
|
&&(i_data_bits == 2'b00)) // Eight data bits
|
|
f_eight_seq <= 1;
|
|
else if (zero_baud_counter)
|
|
f_eight_seq <= f_eight_seq << 1;
|
|
|
|
always @(*)
|
|
if (|f_eight_seq)
|
|
begin
|
|
assert(fsv_setup[29:28] == 2'b00);
|
|
assert(fsv_setup[29:28] == data_bits);
|
|
assert(baud_counter < { 6'h0, fsv_setup[23:0]});
|
|
|
|
assert(1'b0 == |f_five_seq);
|
|
assert(1'b0 == |f_six_seq);
|
|
assert(1'b0 == |f_seven_seq);
|
|
assert(r_busy);
|
|
end
|
|
|
|
always @(*)
|
|
case(f_eight_seq)
|
|
9'h000: begin assert(1); end
|
|
9'h001: begin
|
|
assert(state == 4'h0);
|
|
assert(o_uart_tx == 1'b0);
|
|
assert(lcl_data[7:0] == fsv_data[7:0]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == parity_odd);
|
|
end
|
|
9'h002: begin
|
|
assert(state == 4'h1);
|
|
assert(o_uart_tx == fsv_data[0]);
|
|
assert(lcl_data[6:0] == fsv_data[7:1]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
|
end
|
|
9'h004: begin
|
|
assert(state == 4'h2);
|
|
assert(o_uart_tx == fsv_data[1]);
|
|
assert(lcl_data[5:0] == fsv_data[7:2]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
|
end
|
|
9'h008: begin
|
|
assert(state == 4'h3);
|
|
assert(o_uart_tx == fsv_data[2]);
|
|
assert(lcl_data[4:0] == fsv_data[7:3]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
|
end
|
|
9'h010: begin
|
|
assert(state == 4'h4);
|
|
assert(o_uart_tx == fsv_data[3]);
|
|
assert(lcl_data[3:0] == fsv_data[7:4]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
|
end
|
|
9'h020: begin
|
|
assert(state == 4'h5);
|
|
assert(o_uart_tx == fsv_data[4]);
|
|
assert(lcl_data[2:0] == fsv_data[7:5]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[4:0]) ^ parity_odd);
|
|
end
|
|
9'h040: begin
|
|
assert(state == 4'h6);
|
|
assert(o_uart_tx == fsv_data[5]);
|
|
assert(lcl_data[1:0] == fsv_data[7:6]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == (^fsv_data[5:0]) ^ parity_odd);
|
|
end
|
|
9'h080: begin
|
|
assert(state == 4'h7);
|
|
assert(o_uart_tx == fsv_data[6]);
|
|
assert(lcl_data[0] == fsv_data[7]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[6:0]) ^ parity_odd));
|
|
end
|
|
9'h100: begin
|
|
if (use_parity)
|
|
assert(state == 4'h8);
|
|
else
|
|
assert(state == 4'h9);
|
|
assert(o_uart_tx == fsv_data[7]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == ((^fsv_data[7:0]) ^ parity_odd));
|
|
end
|
|
default: begin if (f_past_valid) assert(0); end
|
|
endcase
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Combined properties for all of the data sequences
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
always @(posedge i_clk)
|
|
if (((|f_five_seq[5:0]) || (|f_six_seq[6:0]) || (|f_seven_seq[7:0])
|
|
|| (|f_eight_seq[8:0]))
|
|
&& ($past(zero_baud_counter)))
|
|
assert(baud_counter == { 4'h0, fsv_setup[23:0] }-1);
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// The stop sequence
|
|
//
|
|
// This consists of any parity bit, as well as one or two stop bits
|
|
////////////////////////////////////////////////////////////////////////
|
|
initial f_stop_seq = 1'b0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_break))
|
|
f_stop_seq <= 0;
|
|
else if (zero_baud_counter)
|
|
begin
|
|
f_stop_seq <= 0;
|
|
if (f_stop_seq[0]) // Coming from a parity bit
|
|
begin
|
|
if (dblstop)
|
|
f_stop_seq[1] <= 1'b1;
|
|
else
|
|
f_stop_seq[2] <= 1'b1;
|
|
end
|
|
|
|
if (f_stop_seq[1])
|
|
f_stop_seq[2] <= 1'b1;
|
|
|
|
if (f_eight_seq[8] | f_seven_seq[7] | f_six_seq[6]
|
|
| f_five_seq[5])
|
|
begin
|
|
if (use_parity)
|
|
f_stop_seq[0] <= 1'b1;
|
|
else if (dblstop)
|
|
f_stop_seq[1] <= 1'b1;
|
|
else
|
|
f_stop_seq[2] <= 1'b1;
|
|
end
|
|
end
|
|
|
|
always @(*)
|
|
if (|f_stop_seq)
|
|
begin
|
|
assert(1'b0 == |f_five_seq[4:0]);
|
|
assert(1'b0 == |f_six_seq[5:0]);
|
|
assert(1'b0 == |f_seven_seq[6:0]);
|
|
assert(1'b0 == |f_eight_seq[7:0]);
|
|
|
|
assert(r_busy);
|
|
end
|
|
|
|
always @(*)
|
|
if (f_stop_seq[0])
|
|
begin
|
|
// 9 if dblstop and use_parity
|
|
if (dblstop)
|
|
assert(state == TXU_STOP);
|
|
else
|
|
assert(state == TXU_STOP);
|
|
assert(use_parity);
|
|
assert(o_uart_tx == fsv_parity);
|
|
end
|
|
|
|
always @(*)
|
|
if (f_stop_seq[1])
|
|
begin
|
|
// if (!use_parity)
|
|
assert(state == TXU_SECOND_STOP);
|
|
assert(dblstop);
|
|
assert(o_uart_tx);
|
|
end
|
|
|
|
always @(*)
|
|
if (f_stop_seq[2])
|
|
begin
|
|
assert(state == 4'hf);
|
|
assert(o_uart_tx);
|
|
assert(baud_counter < fsv_setup[23:0]-1'b1);
|
|
end
|
|
|
|
|
|
always @(*)
|
if (fsv_setup[25])
|
if (fsv_setup[25])
|
fsv_parity <= fsv_setup[24];
|
fsv_parity <= fsv_setup[24];
|
else
|
else
|
case(fsv_setup[29:28])
|
case(fsv_setup[29:28])
|
2'b00: fsv_parity <= (^fsv_data[4:0]) ^ fsv_setup[24];
|
2'b00: fsv_parity = (^fsv_data[7:0]) ^ fsv_setup[24];
|
2'b01: fsv_parity <= (^fsv_data[5:0]) ^ fsv_setup[24];
|
2'b01: fsv_parity = (^fsv_data[6:0]) ^ fsv_setup[24];
|
2'b10: fsv_parity <= (^fsv_data[6:0]) ^ fsv_setup[24];
|
2'b10: fsv_parity = (^fsv_data[5:0]) ^ fsv_setup[24];
|
2'b11: fsv_parity <= (^fsv_data[7:0]) ^ fsv_setup[24];
|
2'b11: fsv_parity = (^fsv_data[4:0]) ^ fsv_setup[24];
|
endcase
|
endcase
|
|
|
assert property( @(posedge i_clk)
|
//////////////////////////////////////////////////////////////////////
|
(o_busy)[*2] |=> $stable(fsv_parity));
|
//
|
|
// The break sequence
|
assert property( @(posedge i_clk)
|
//
|
(o_busy) |=> $stable(fsv_data));
|
//////////////////////////////////////////////////////////////////////
|
|
reg [1:0] f_break_seq;
|
assert property( @(posedge i_clk)
|
initial f_break_seq = 2'b00;
|
(o_busy) |=> $stable(fsv_setup));
|
always @(posedge i_clk)
|
|
if (i_reset)
|
sequence SENDPARITY(SETUP);
|
f_break_seq <= 2'b00;
|
((o_uart_tx == fsv_parity)&&(state == `TXU_PARITY)
|
else if (i_break)
|
&&(SETUP[26])
|
f_break_seq <= 2'b01;
|
&&(baud_counter == SETUP[21:0]-1)
|
else if (!zero_baud_counter)
|
&&(!zero_baud_counter))
|
f_break_seq <= { |f_break_seq, 1'b0 };
|
##1 ((o_uart_tx == fsv_parity)&&(state == `TXU_PARITY)
|
else
|
&&(SETUP[26])
|
f_break_seq <= 0;
|
&&(baud_counter < SETUP[21:0])
|
|
&&(baud_counter > 0)
|
always @(posedge i_clk)
|
&&(baud_counter == $past(baud_counter)-1)
|
if (f_break_seq[0])
|
&&(!zero_baud_counter))[*0:$]
|
assert(baud_counter == { $past(fsv_setup[23:0]), 4'h0 });
|
##1 (o_uart_tx == fsv_parity)&&(state == `TXU_PARITY)
|
always @(posedge i_clk)
|
&&(SETUP[26])
|
if ((f_past_valid)&&($past(f_break_seq[1]))&&(state != TXU_BREAK))
|
&&(zero_baud_counter);
|
begin
|
endsequence
|
assert(state == TXU_IDLE);
|
|
assert(o_uart_tx == 1'b1);
|
sequence SENDSINGLESTOP(CKS,ST);
|
end
|
((o_uart_tx == 1'b1)&&(state == ST)
|
|
&&(baud_counter == CKS-1)
|
always @(*)
|
&&(!zero_baud_counter))
|
if (|f_break_seq)
|
##1 ((o_uart_tx == 1'b1)&&(state == ST)
|
begin
|
&&(baud_counter > 0)
|
assert(state == TXU_BREAK);
|
&&(baud_counter == $past(baud_counter)-1)
|
assert(r_busy);
|
&&(!zero_baud_counter))[*0:$]
|
assert(o_uart_tx == 1'b0);
|
##1 (o_uart_tx == 1'b1)&&(state == ST)
|
end
|
&&(zero_baud_counter);
|
|
endsequence
|
//////////////////////////////////////////////////////////////////////
|
|
//
|
sequence SENDFULLSTOP(SETUP);
|
// Properties for use during induction if we are made a submodule of
|
((!SETUP[27]) throughout SENDSINGLESTOP(SETUP[21:0],`TXU_STOP))
|
// the rxuart
|
or (SETUP[27]) throughout
|
//
|
SENDSINGLESTOP(SETUP[21:0],`TXU_STOP)
|
//////////////////////////////////////////////////////////////////////
|
##1 SENDSINGLESTOP(SETUP[21:0],`TXU_SECOND_STOP);
|
|
endsequence
|
// Need enough bits for reset (24+4) plus enough bits for all of the
|
|
// various characters, 24+4, so 24+5 is a minimum of this counter
|
sequence UART_IDLE;
|
//
|
(!o_busy)&&(o_uart_tx)&&(zero_baud_counter);
|
`ifndef TXUART
|
endsequence
|
reg [28:0] f_counter;
|
|
initial f_counter = 0;
|
assert property ( @(posedge i_clk) (!o_busy) |-> UART_IDLE);
|
always @(posedge i_clk)
|
|
if (!o_busy)
|
|
f_counter <= 1'b0;
|
assert property ( @(posedge i_clk)
|
else
|
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b00) |=>
|
f_counter <= f_counter + 1'b1;
|
((o_busy) throughout
|
|
SEND5(fsv_data)
|
always @(*)
|
##1 SENDPARITY(fsv_setup)
|
if (f_five_seq[0]|f_six_seq[0]|f_seven_seq[0]|f_eight_seq[0])
|
##1 SENDFULLSTOP(fsv_setup)
|
assert(f_counter == (fsv_setup[23:0] - baud_counter - 1));
|
)
|
else if (f_five_seq[1]|f_six_seq[1]|f_seven_seq[1]|f_eight_seq[1])
|
##1 UART_IDLE);
|
assert(f_counter == ({4'h0, fsv_setup[23:0], 1'b0} - baud_counter - 1));
|
|
else if (f_five_seq[2]|f_six_seq[2]|f_seven_seq[2]|f_eight_seq[2])
|
assert property ( @(posedge i_clk)
|
assert(f_counter == ({4'h0, fsv_setup[23:0], 1'b0}
|
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b01) |=>
|
+{5'h0, fsv_setup[23:0]}
|
((o_busy) throughout
|
- baud_counter - 1));
|
SEND6(fsv_data)
|
else if (f_five_seq[3]|f_six_seq[3]|f_seven_seq[3]|f_eight_seq[3])
|
##1 SENDPARITY(fsv_setup)
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
##1 SENDFULLSTOP(fsv_setup)
|
- baud_counter - 1));
|
)
|
else if (f_five_seq[4]|f_six_seq[4]|f_seven_seq[4]|f_eight_seq[4])
|
##1 UART_IDLE);
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
|
+{5'h0, fsv_setup[23:0]}
|
assert property ( @(posedge i_clk)
|
- baud_counter - 1));
|
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b10) |=>
|
else if (f_five_seq[5]|f_six_seq[5]|f_seven_seq[5]|f_eight_seq[5])
|
((o_busy) throughout
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
SEND7(fsv_data)
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
##1 SENDPARITY(fsv_setup)
|
- baud_counter - 1));
|
##1 SENDFULLSTOP(fsv_setup)
|
else if (f_six_seq[6]|f_seven_seq[6]|f_eight_seq[6])
|
)
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
##1 UART_IDLE);
|
+{5'h0, fsv_setup[23:0]}
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
assert property ( @(posedge i_clk)
|
- baud_counter - 1));
|
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b11) |=>
|
else if (f_seven_seq[7]|f_eight_seq[7])
|
((o_busy) throughout
|
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 8
|
SEND8(fsv_data)
|
- baud_counter - 1));
|
##1 SENDPARITY(fsv_setup)
|
else if (f_eight_seq[8])
|
##1 SENDFULLSTOP(fsv_setup)
|
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 9
|
)
|
+{5'h0, fsv_setup[23:0]}
|
##1 UART_IDLE);
|
- baud_counter - 1));
|
|
else if (f_stop_seq[0] || (!use_parity && f_stop_seq[1]))
|
|
begin
|
|
// Parity bit, or first of two stop bits
|
|
case(data_bits)
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
|
- baud_counter - 1));
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
|
- baud_counter - 1));
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
- baud_counter - 1)); // 8
|
|
2'b11: assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 7
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 1));
|
|
endcase
|
|
end else if (!use_parity && !dblstop && f_stop_seq[2])
|
|
begin
|
|
// No parity, single stop bit
|
|
// Different from the one above, since the last counter is has
|
|
// one fewer items within it
|
|
case(data_bits)
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
|
- baud_counter - 2));
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
|
- baud_counter - 2));
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
- baud_counter - 2)); // 8
|
|
2'b11: assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 7
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 2));
|
|
endcase
|
|
end else if (f_stop_seq[1])
|
|
begin
|
|
// Parity and the first of two stop bits
|
|
assert(dblstop && use_parity);
|
|
case(data_bits)
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 11
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 1));
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
|
- baud_counter - 1));
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
|
- baud_counter - 1));
|
|
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
- baud_counter - 1)); // 8
|
|
endcase
|
|
end else if ((dblstop ^ use_parity) && f_stop_seq[2])
|
|
begin
|
|
// Parity and one stop bit
|
|
// assert(!dblstop && use_parity);
|
|
case(data_bits)
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 11
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 2));
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
|
- baud_counter - 2));
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
|
- baud_counter - 2));
|
|
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
- baud_counter - 2)); // 8
|
|
endcase
|
|
end else if (f_stop_seq[2])
|
|
begin
|
|
assert(dblstop);
|
|
assert(use_parity);
|
|
// Parity and two stop bits
|
|
case(data_bits)
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{3'h0, fsv_setup[23:0], 2'b00} // 12
|
|
- baud_counter - 2));
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 11
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 2));
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
|
- baud_counter - 2));
|
|
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
|
- baud_counter - 2));
|
|
endcase
|
|
end
|
|
`endif
|
|
|
|
//////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Other properties, not necessarily associated with any sequences
|
|
//
|
|
//////////////////////////////////////////////////////////////////////
|
|
always @(*)
|
|
assert((state < 4'hb)||(state >= 4'he));
|
|
//////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Careless/limiting assumption section
|
|
//
|
|
//////////////////////////////////////////////////////////////////////
|
|
always @(*)
|
|
assume(i_setup[23:0] > 2);
|
|
always @(*)
|
|
assert(fsv_setup[23:0] > 2);
|
|
|
`endif // FORMAL
|
`endif // FORMAL
|
endmodule
|
endmodule
|
|
|
|
|
No newline at end of file
|
No newline at end of file
|
