1139 lines
34 KiB
Verilog
1139 lines
34 KiB
Verilog
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Filename: txuart.v
|
|
//
|
|
// Project: wbuart32, a full featured UART with simulator
|
|
//
|
|
// Purpose: Transmit outputs over a single UART line.
|
|
//
|
|
// To interface with this module, connect it to your system clock,
|
|
// pass it the 32 bit setup register (defined below) and the byte
|
|
// of data you wish to transmit. Strobe the i_wr line high for one
|
|
// clock 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
|
|
// cause your data to be lost. The output will be placed on the o_txuart
|
|
// output line. If you wish to set/send a break condition, assert the
|
|
// i_break line otherwise leave it low.
|
|
//
|
|
// There is a synchronous reset line, logic high.
|
|
//
|
|
// Now for the setup register. The register is 32 bits, so that this
|
|
// UART may be set up over a 32-bit bus.
|
|
//
|
|
// i_setup[30] Set this to zero to use hardware flow control, and to
|
|
// one to ignore hardware flow control. Only works if the hardware
|
|
// flow control has been properly wired.
|
|
//
|
|
// If you don't want hardware flow control, fix the i_rts bit to
|
|
// 1'b1, and let the synthesys tools optimize out the logic.
|
|
//
|
|
// i_setup[29:28] Indicates the number of data bits per word. This will
|
|
// either be 2'b00 for an 8-bit word, 2'b01 for a 7-bit word, 2'b10
|
|
// for a six bit word, or 2'b11 for a five bit word.
|
|
//
|
|
// i_setup[27] Indicates whether or not to use one or two stop bits.
|
|
// Set this to one to expect two stop bits, zero for one.
|
|
//
|
|
// i_setup[26] Indicates whether or not a parity bit exists. Set this
|
|
// to 1'b1 to include parity.
|
|
//
|
|
// i_setup[25] Indicates whether or not the parity bit is fixed. Set
|
|
// to 1'b1 to include a fixed bit of parity, 1'b0 to allow the
|
|
// parity to be set based upon data. (Both assume the parity
|
|
// enable value is set.)
|
|
//
|
|
// i_setup[24] This bit is ignored if parity is not used. Otherwise,
|
|
// in the case of a fixed parity bit, this bit indicates whether
|
|
// mark (1'b1) or space (1'b0) parity is used. Likewise if the
|
|
// parity is not fixed, a 1'b1 selects even parity, and 1'b0
|
|
// selects odd.
|
|
//
|
|
// i_setup[23:0] Indicates the speed of the UART in terms of clocks.
|
|
// So, for example, if you have a 200 MHz clock and wish to
|
|
// run your UART at 9600 baud, you would take 200 MHz and divide
|
|
// by 9600 to set this value to 24'd20834. Likewise if you wished
|
|
// to run this serial port at 115200 baud from a 200 MHz clock,
|
|
// you would set the value to 24'd1736
|
|
//
|
|
// Thus, to set the UART for the common setting of an 8-bit word,
|
|
// one stop bit, no parity, and 115200 baud over a 200 MHz clock, you
|
|
// would want to set the setup value to:
|
|
//
|
|
// 32'h0006c8 // For 115,200 baud, 8 bit, no parity
|
|
// 32'h005161 // For 9600 baud, 8 bit, no parity
|
|
//
|
|
//
|
|
// Creator: Dan Gisselquist, Ph.D.
|
|
// Gisselquist Technology, LLC
|
|
//
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Copyright (C) 2015-2019, 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 txuart(i_clk, i_reset, i_setup, i_break, i_wr, i_data,
|
|
i_cts_n, o_uart_tx, o_busy);
|
|
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 [30:0] i_setup;
|
|
input wire i_break;
|
|
input wire i_wr;
|
|
input wire [7:0] i_data;
|
|
// Hardware flow control Ready-To-Send bit. Set this to one to use
|
|
// the core without flow control. (A more appropriate name would be
|
|
// the Ready-To-Receive bit ...)
|
|
input wire i_cts_n;
|
|
// 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;
|
|
|
|
wire [27:0] clocks_per_baud, break_condition;
|
|
wire [1:0] i_data_bits, data_bits;
|
|
wire use_parity, parity_odd, dblstop, fixd_parity,
|
|
fixdp_value, hw_flow_control, i_parity_odd;
|
|
reg [30:0] r_setup;
|
|
assign clocks_per_baud = { 4'h0, r_setup[23:0] };
|
|
assign break_condition = { r_setup[23:0], 4'h0 };
|
|
assign hw_flow_control = !r_setup[30];
|
|
assign i_data_bits = i_setup[29:28];
|
|
assign data_bits = r_setup[29:28];
|
|
assign dblstop = r_setup[27];
|
|
assign use_parity = r_setup[26];
|
|
assign fixd_parity = r_setup[25];
|
|
assign i_parity_odd = i_setup[24];
|
|
assign parity_odd = r_setup[24];
|
|
assign fixdp_value = r_setup[24];
|
|
|
|
reg [27:0] baud_counter;
|
|
reg [3:0] state;
|
|
reg [7:0] lcl_data;
|
|
reg calc_parity, r_busy, zero_baud_counter, last_state;
|
|
|
|
|
|
// First step ... handle any hardware flow control, if so enabled.
|
|
//
|
|
// Clock in the flow control data, two clocks to avoid metastability
|
|
// Default to using hardware flow control (uart_setup[30]==0 to use it).
|
|
// Set this high order bit off if you do not wish to use it.
|
|
reg q_cts_n, qq_cts_n, ck_cts;
|
|
// While we might wish to give initial values to q_rts and ck_cts,
|
|
// 1) it's not required since the transmitter starts in a long wait
|
|
// state, and 2) doing so will prevent the synthesizer from optimizing
|
|
// this pin in the case it is hard set to 1'b1 external to this
|
|
// peripheral.
|
|
//
|
|
// initial q_cts_n = 1'b1;
|
|
// initial qq_cts_n = 1'b1;
|
|
// initial ck_cts = 1'b0;
|
|
always @(posedge i_clk)
|
|
{ qq_cts_n, q_cts_n } <= { q_cts_n, i_cts_n };
|
|
always @(posedge i_clk)
|
|
ck_cts <= (!qq_cts_n)||(!hw_flow_control);
|
|
|
|
initial o_uart_tx = 1'b1;
|
|
initial r_busy = 1'b1;
|
|
initial state = TXU_IDLE;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
begin
|
|
r_busy <= 1'b1;
|
|
state <= TXU_IDLE;
|
|
end else if (i_break)
|
|
begin
|
|
state <= TXU_BREAK;
|
|
r_busy <= 1'b1;
|
|
end else if (!zero_baud_counter)
|
|
begin // r_busy needs to be set coming into here
|
|
r_busy <= 1'b1;
|
|
end else if (state == TXU_BREAK)
|
|
begin
|
|
state <= TXU_IDLE;
|
|
r_busy <= !ck_cts;
|
|
end else if (state == TXU_IDLE) // STATE_IDLE
|
|
begin
|
|
if ((i_wr)&&(!r_busy))
|
|
begin // Immediately start us off with a start bit
|
|
r_busy <= 1'b1;
|
|
case(i_data_bits)
|
|
2'b00: state <= TXU_BIT_ZERO;
|
|
2'b01: state <= TXU_BIT_ONE;
|
|
2'b10: state <= TXU_BIT_TWO;
|
|
2'b11: state <= TXU_BIT_THREE;
|
|
endcase
|
|
end else begin // Stay in idle
|
|
r_busy <= !ck_cts;
|
|
end
|
|
end else begin
|
|
// One clock tick in each of these states ...
|
|
// baud_counter <= clocks_per_baud - 28'h01;
|
|
r_busy <= 1'b1;
|
|
if (state[3] == 0) // First 8 bits
|
|
begin
|
|
if (state == TXU_BIT_SEVEN)
|
|
state <= (use_parity)? TXU_PARITY:TXU_STOP;
|
|
else
|
|
state <= state + 1;
|
|
end else if (state == TXU_PARITY)
|
|
begin
|
|
state <= TXU_STOP;
|
|
end else if (state == TXU_STOP)
|
|
begin // two stop bit(s)
|
|
if (dblstop)
|
|
state <= TXU_SECOND_STOP;
|
|
else
|
|
state <= TXU_IDLE;
|
|
end else // `TXU_SECOND_STOP and default:
|
|
begin
|
|
state <= TXU_IDLE; // Go back to idle
|
|
// Still r_busy, since we need to wait
|
|
// for the baud clock to finish counting
|
|
// out this last bit.
|
|
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);
|
|
|
|
|
|
// r_setup
|
|
//
|
|
// Our setup register. Accept changes between any pair of transmitted
|
|
// words. The register itself has many fields to it. These are
|
|
// 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)
|
|
// the size of our data word.
|
|
initial r_setup = INITIAL_SETUP;
|
|
always @(posedge i_clk)
|
|
if (!o_busy)
|
|
r_setup <= i_setup;
|
|
|
|
// 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 (!r_busy)
|
|
lcl_data <= i_data;
|
|
else if (zero_baud_counter)
|
|
lcl_data <= { 1'b0, 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.
|
|
//
|
|
// Ok, that said, our rules are:
|
|
// 1'b0 on any break condition
|
|
// 1'b0 on a start bit (IDLE, write, and not busy)
|
|
// lcl_data[0] during any data transfer, but only at the baud
|
|
// change
|
|
// PARITY -- During the parity bit. This depends upon whether or
|
|
// not the parity bit is fixed, then what it's fixed to,
|
|
// or changing, and hence what it's calculated value is.
|
|
// 1'b1 at all other times (stop bits, idle, etc)
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
o_uart_tx <= 1'b1;
|
|
else if ((i_break)||((i_wr)&&(!r_busy)))
|
|
o_uart_tx <= 1'b0;
|
|
else if (zero_baud_counter)
|
|
casez(state)
|
|
4'b0???: o_uart_tx <= lcl_data[0];
|
|
TXU_PARITY: o_uart_tx <= calc_parity;
|
|
default: o_uart_tx <= 1'b1;
|
|
endcase
|
|
|
|
|
|
// calc_parity
|
|
//
|
|
// 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
|
|
// value (r_setup[24]). Otherwise the parity is given by the GF2
|
|
// sum of all the data bits (plus one for even parity).
|
|
initial calc_parity = 1'b0;
|
|
always @(posedge i_clk)
|
|
if (!o_busy)
|
|
calc_parity <= i_setup[24];
|
|
else if (fixd_parity)
|
|
calc_parity <= fixdp_value;
|
|
else if (zero_baud_counter)
|
|
begin
|
|
if (state[3] == 0) // First 8 bits of msg
|
|
calc_parity <= calc_parity ^ lcl_data[0];
|
|
else if (state == TXU_IDLE)
|
|
calc_parity <= parity_odd;
|
|
end else if (!r_busy)
|
|
calc_parity <= parity_odd;
|
|
|
|
|
|
// 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 == TXU_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'b0;
|
|
initial baud_counter = 28'h05;
|
|
always @(posedge i_clk)
|
|
begin
|
|
zero_baud_counter <= (baud_counter == 28'h01);
|
|
if ((i_reset)||(i_break))
|
|
begin
|
|
// Give ourselves 16 bauds before being ready
|
|
baud_counter <= break_condition;
|
|
zero_baud_counter <= 1'b0;
|
|
end else if (!zero_baud_counter)
|
|
baud_counter <= baud_counter - 28'h01;
|
|
else if (state == TXU_BREAK)
|
|
begin
|
|
baud_counter <= 0;
|
|
zero_baud_counter <= 1'b1;
|
|
end else if (state == TXU_IDLE)
|
|
begin
|
|
baud_counter <= 28'h0;
|
|
zero_baud_counter <= 1'b1;
|
|
if ((i_wr)&&(!r_busy))
|
|
begin
|
|
baud_counter <= { 4'h0, i_setup[23:0]} - 28'h01;
|
|
zero_baud_counter <= 1'b0;
|
|
end
|
|
end else if (last_state)
|
|
baud_counter <= clocks_per_baud - 28'h02;
|
|
else
|
|
baud_counter <= clocks_per_baud - 28'h01;
|
|
end
|
|
|
|
initial last_state = 1'b0;
|
|
always @(posedge i_clk)
|
|
if (dblstop)
|
|
last_state <= (state == TXU_SECOND_STOP);
|
|
else
|
|
last_state <= (state == TXU_STOP);
|
|
|
|
// Verilator lint_off UNUSED
|
|
wire [2:0] unused;
|
|
assign unused = { i_parity_odd, data_bits };
|
|
// Verilator lint_on UNUSED
|
|
|
|
`ifdef FORMAL
|
|
reg fsv_parity;
|
|
reg [30:0] fsv_setup;
|
|
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)
|
|
if ((i_wr)&&(!o_busy))
|
|
fsv_data <= i_data;
|
|
|
|
initial fsv_setup = INITIAL_SETUP;
|
|
always @(posedge i_clk)
|
|
if (!o_busy)
|
|
fsv_setup <= i_setup;
|
|
|
|
always @(*)
|
|
assert(r_setup == fsv_setup);
|
|
|
|
|
|
always @(posedge i_clk)
|
|
assert(zero_baud_counter == (baud_counter == 0));
|
|
|
|
always @(*)
|
|
if (!o_busy)
|
|
assert(zero_baud_counter);
|
|
|
|
/*
|
|
*
|
|
* 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
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(zero_baud_counter))
|
|
&&(!$past(i_reset))&&(!$past(i_break)))
|
|
begin
|
|
assert($stable(o_uart_tx));
|
|
assert($stable(state));
|
|
assert($stable(lcl_data));
|
|
if ((state != TXU_IDLE)&&(state != TXU_BREAK))
|
|
assert($stable(calc_parity));
|
|
assert(baud_counter == $past(baud_counter)-1'b1);
|
|
end
|
|
|
|
//
|
|
// Our various sequence data declarations
|
|
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
|
|
//
|
|
// DATA = the byte that is sent
|
|
// CKS = the number of clocks per bit
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Five bit data
|
|
//
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
initial f_five_seq = 0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_break))
|
|
f_five_seq = 0;
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
|
&&(i_data_bits == 2'b11)) // five data bits
|
|
f_five_seq <= 1;
|
|
else if (zero_baud_counter)
|
|
f_five_seq <= f_five_seq << 1;
|
|
|
|
always @(*)
|
|
if (|f_five_seq)
|
|
begin
|
|
assert(fsv_setup[29:28] == data_bits);
|
|
assert(data_bits == 2'b11);
|
|
assert(baud_counter < fsv_setup[23:0]);
|
|
|
|
assert(1'b0 == |f_six_seq);
|
|
assert(1'b0 == |f_seven_seq);
|
|
assert(1'b0 == |f_eight_seq);
|
|
assert(r_busy);
|
|
assert(state > 4'h2);
|
|
end
|
|
|
|
always @(*)
|
|
case(f_five_seq)
|
|
6'h00: begin assert(1); end
|
|
6'h01: begin
|
|
assert(state == 4'h3);
|
|
assert(o_uart_tx == 1'b0);
|
|
assert(lcl_data[4:0] == fsv_data[4:0]);
|
|
if (!fixd_parity)
|
|
assert(calc_parity == parity_odd);
|
|
end
|
|
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)
|
|
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])
|
|
fsv_parity <= fsv_setup[24];
|
|
else
|
|
case(fsv_setup[29:28])
|
|
2'b00: fsv_parity = (^fsv_data[7:0]) ^ fsv_setup[24];
|
|
2'b01: 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[4:0]) ^ fsv_setup[24];
|
|
endcase
|
|
|
|
//////////////////////////////////////////////////////////////////////
|
|
//
|
|
// The break sequence
|
|
//
|
|
//////////////////////////////////////////////////////////////////////
|
|
reg [1:0] f_break_seq;
|
|
initial f_break_seq = 2'b00;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
f_break_seq <= 2'b00;
|
|
else if (i_break)
|
|
f_break_seq <= 2'b01;
|
|
else if (!zero_baud_counter)
|
|
f_break_seq <= { |f_break_seq, 1'b0 };
|
|
else
|
|
f_break_seq <= 0;
|
|
|
|
always @(posedge i_clk)
|
|
if (f_break_seq[0])
|
|
assert(baud_counter == { $past(fsv_setup[23:0]), 4'h0 });
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(f_break_seq[1]))&&(state != TXU_BREAK))
|
|
begin
|
|
assert(state == TXU_IDLE);
|
|
assert(o_uart_tx == 1'b1);
|
|
end
|
|
|
|
always @(*)
|
|
if (|f_break_seq)
|
|
begin
|
|
assert(state == TXU_BREAK);
|
|
assert(r_busy);
|
|
assert(o_uart_tx == 1'b0);
|
|
end
|
|
|
|
//////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Properties for use during induction if we are made a submodule of
|
|
// the rxuart
|
|
//
|
|
//////////////////////////////////////////////////////////////////////
|
|
|
|
// 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
|
|
//
|
|
`ifndef TXUART
|
|
reg [28:0] f_counter;
|
|
initial f_counter = 0;
|
|
always @(posedge i_clk)
|
|
if (!o_busy)
|
|
f_counter <= 1'b0;
|
|
else
|
|
f_counter <= f_counter + 1'b1;
|
|
|
|
always @(*)
|
|
if (f_five_seq[0]|f_six_seq[0]|f_seven_seq[0]|f_eight_seq[0])
|
|
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])
|
|
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(f_counter == ({4'h0, fsv_setup[23:0], 1'b0}
|
|
+{5'h0, fsv_setup[23:0]}
|
|
- baud_counter - 1));
|
|
else if (f_five_seq[3]|f_six_seq[3]|f_seven_seq[3]|f_eight_seq[3])
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
|
- baud_counter - 1));
|
|
else if (f_five_seq[4]|f_six_seq[4]|f_seven_seq[4]|f_eight_seq[4])
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
|
+{5'h0, fsv_setup[23:0]}
|
|
- baud_counter - 1));
|
|
else if (f_five_seq[5]|f_six_seq[5]|f_seven_seq[5]|f_eight_seq[5])
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 1));
|
|
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}
|
|
+{5'h0, fsv_setup[23:0]}
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
|
- baud_counter - 1));
|
|
else if (f_seven_seq[7]|f_eight_seq[7])
|
|
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 8
|
|
- baud_counter - 1));
|
|
else if (f_eight_seq[8])
|
|
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 9
|
|
+{5'h0, fsv_setup[23:0]}
|
|
- 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
|
|
endmodule
|
|
|