1 |
2 |
dgisselq |
////////////////////////////////////////////////////////////////////////////////
|
2 |
|
|
//
|
3 |
|
|
// Filename: txuart.v
|
4 |
|
|
//
|
5 |
|
|
// Project: wbuart32, a full featured UART with simulator
|
6 |
|
|
//
|
7 |
|
|
// Purpose: Transmit outputs over a single UART line.
|
8 |
|
|
//
|
9 |
|
|
// To interface with this module, connect it to your system clock,
|
10 |
|
|
// pass it the 32 bit setup register (defined below) and the byte
|
11 |
|
|
// of data you wish to transmit. Strobe the i_wr line high for one
|
12 |
|
|
// clock cycle, and your data will be off. Wait until the 'o_busy'
|
13 |
|
|
// line is low before strobing the i_wr line again--this implementation
|
14 |
|
|
// has NO BUFFER, so strobing i_wr while the core is busy will just
|
15 |
|
|
// cause your data to be lost. The output will be placed on the o_txuart
|
16 |
|
|
// output line. If you wish to set/send a break condition, assert the
|
17 |
|
|
// i_break line otherwise leave it low.
|
18 |
|
|
//
|
19 |
|
|
// There is a synchronous reset line, logic high.
|
20 |
|
|
//
|
21 |
|
|
// Now for the setup register. The register is 32 bits, so that this
|
22 |
|
|
// UART may be set up over a 32-bit bus.
|
23 |
|
|
//
|
24 |
9 |
dgisselq |
// i_setup[30] Set this to zero to use hardware flow control, and to
|
25 |
|
|
// one to ignore hardware flow control. Only works if the hardware
|
26 |
|
|
// flow control has been properly wired.
|
27 |
|
|
//
|
28 |
|
|
// If you don't want hardware flow control, fix the i_rts bit to
|
29 |
|
|
// 1'b1, and let the synthesys tools optimize out the logic.
|
30 |
|
|
//
|
31 |
2 |
dgisselq |
// i_setup[29:28] Indicates the number of data bits per word. This will
|
32 |
9 |
dgisselq |
// either be 2'b00 for an 8-bit word, 2'b01 for a 7-bit word, 2'b10
|
33 |
|
|
// for a six bit word, or 2'b11 for a five bit word.
|
34 |
2 |
dgisselq |
//
|
35 |
|
|
// i_setup[27] Indicates whether or not to use one or two stop bits.
|
36 |
|
|
// Set this to one to expect two stop bits, zero for one.
|
37 |
|
|
//
|
38 |
|
|
// i_setup[26] Indicates whether or not a parity bit exists. Set this
|
39 |
|
|
// to 1'b1 to include parity.
|
40 |
|
|
//
|
41 |
|
|
// i_setup[25] Indicates whether or not the parity bit is fixed. Set
|
42 |
|
|
// to 1'b1 to include a fixed bit of parity, 1'b0 to allow the
|
43 |
|
|
// parity to be set based upon data. (Both assume the parity
|
44 |
|
|
// enable value is set.)
|
45 |
|
|
//
|
46 |
|
|
// i_setup[24] This bit is ignored if parity is not used. Otherwise,
|
47 |
|
|
// in the case of a fixed parity bit, this bit indicates whether
|
48 |
|
|
// mark (1'b1) or space (1'b0) parity is used. Likewise if the
|
49 |
|
|
// parity is not fixed, a 1'b1 selects even parity, and 1'b0
|
50 |
|
|
// selects odd.
|
51 |
|
|
//
|
52 |
|
|
// i_setup[23:0] Indicates the speed of the UART in terms of clocks.
|
53 |
|
|
// So, for example, if you have a 200 MHz clock and wish to
|
54 |
|
|
// run your UART at 9600 baud, you would take 200 MHz and divide
|
55 |
|
|
// by 9600 to set this value to 24'd20834. Likewise if you wished
|
56 |
|
|
// to run this serial port at 115200 baud from a 200 MHz clock,
|
57 |
|
|
// you would set the value to 24'd1736
|
58 |
|
|
//
|
59 |
|
|
// Thus, to set the UART for the common setting of an 8-bit word,
|
60 |
|
|
// one stop bit, no parity, and 115200 baud over a 200 MHz clock, you
|
61 |
|
|
// would want to set the setup value to:
|
62 |
|
|
//
|
63 |
|
|
// 32'h0006c8 // For 115,200 baud, 8 bit, no parity
|
64 |
|
|
// 32'h005161 // For 9600 baud, 8 bit, no parity
|
65 |
|
|
//
|
66 |
|
|
//
|
67 |
|
|
// Creator: Dan Gisselquist, Ph.D.
|
68 |
|
|
// Gisselquist Technology, LLC
|
69 |
|
|
//
|
70 |
|
|
////////////////////////////////////////////////////////////////////////////////
|
71 |
|
|
//
|
72 |
26 |
dgisselq |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
|
73 |
2 |
dgisselq |
//
|
74 |
|
|
// This program is free software (firmware): you can redistribute it and/or
|
75 |
|
|
// modify it under the terms of the GNU General Public License as published
|
76 |
|
|
// by the Free Software Foundation, either version 3 of the License, or (at
|
77 |
|
|
// your option) any later version.
|
78 |
|
|
//
|
79 |
|
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
80 |
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
81 |
|
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
82 |
|
|
// for more details.
|
83 |
|
|
//
|
84 |
|
|
// You should have received a copy of the GNU General Public License along
|
85 |
9 |
dgisselq |
// with this program. (It's in the $(ROOT)/doc directory. Run make with no
|
86 |
2 |
dgisselq |
// target there if the PDF file isn't present.) If not, see
|
87 |
|
|
// <http://www.gnu.org/licenses/> for a copy.
|
88 |
|
|
//
|
89 |
|
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
90 |
|
|
// http://www.gnu.org/licenses/gpl.html
|
91 |
|
|
//
|
92 |
|
|
//
|
93 |
|
|
////////////////////////////////////////////////////////////////////////////////
|
94 |
|
|
//
|
95 |
|
|
//
|
96 |
17 |
dgisselq |
`default_nettype none
|
97 |
|
|
//
|
98 |
2 |
dgisselq |
//
|
99 |
9 |
dgisselq |
module txuart(i_clk, i_reset, i_setup, i_break, i_wr, i_data,
|
100 |
15 |
dgisselq |
i_cts_n, o_uart_tx, o_busy);
|
101 |
9 |
dgisselq |
parameter [30:0] INITIAL_SETUP = 31'd868;
|
102 |
26 |
dgisselq |
//
|
103 |
|
|
localparam [3:0] TXU_BIT_ZERO = 4'h0;
|
104 |
|
|
localparam [3:0] TXU_BIT_ONE = 4'h1;
|
105 |
|
|
localparam [3:0] TXU_BIT_TWO = 4'h2;
|
106 |
|
|
localparam [3:0] TXU_BIT_THREE = 4'h3;
|
107 |
|
|
localparam [3:0] TXU_BIT_FOUR = 4'h4;
|
108 |
|
|
localparam [3:0] TXU_BIT_FIVE = 4'h5;
|
109 |
|
|
localparam [3:0] TXU_BIT_SIX = 4'h6;
|
110 |
|
|
localparam [3:0] TXU_BIT_SEVEN = 4'h7;
|
111 |
|
|
localparam [3:0] TXU_PARITY = 4'h8;
|
112 |
|
|
localparam [3:0] TXU_STOP = 4'h9;
|
113 |
|
|
localparam [3:0] TXU_SECOND_STOP = 4'ha;
|
114 |
|
|
//
|
115 |
|
|
localparam [3:0] TXU_BREAK = 4'he;
|
116 |
|
|
localparam [3:0] TXU_IDLE = 4'hf;
|
117 |
|
|
//
|
118 |
|
|
//
|
119 |
17 |
dgisselq |
input wire i_clk, i_reset;
|
120 |
|
|
input wire [30:0] i_setup;
|
121 |
|
|
input wire i_break;
|
122 |
|
|
input wire i_wr;
|
123 |
|
|
input wire [7:0] i_data;
|
124 |
9 |
dgisselq |
// Hardware flow control Ready-To-Send bit. Set this to one to use
|
125 |
|
|
// the core without flow control. (A more appropriate name would be
|
126 |
|
|
// the Ready-To-Receive bit ...)
|
127 |
17 |
dgisselq |
input wire i_cts_n;
|
128 |
9 |
dgisselq |
// And the UART input line itself
|
129 |
5 |
dgisselq |
output reg o_uart_tx;
|
130 |
9 |
dgisselq |
// A line to tell others when we are ready to accept data. If
|
131 |
|
|
// (i_wr)&&(!o_busy) is ever true, then the core has accepted a byte
|
132 |
|
|
// for transmission.
|
133 |
2 |
dgisselq |
output wire o_busy;
|
134 |
|
|
|
135 |
|
|
wire [27:0] clocks_per_baud, break_condition;
|
136 |
26 |
dgisselq |
wire [1:0] i_data_bits, data_bits;
|
137 |
|
|
wire use_parity, parity_odd, dblstop, fixd_parity,
|
138 |
|
|
fixdp_value, hw_flow_control, i_parity_odd;
|
139 |
9 |
dgisselq |
reg [30:0] r_setup;
|
140 |
2 |
dgisselq |
assign clocks_per_baud = { 4'h0, r_setup[23:0] };
|
141 |
|
|
assign break_condition = { r_setup[23:0], 4'h0 };
|
142 |
9 |
dgisselq |
assign hw_flow_control = !r_setup[30];
|
143 |
26 |
dgisselq |
assign i_data_bits = i_setup[29:28];
|
144 |
9 |
dgisselq |
assign data_bits = r_setup[29:28];
|
145 |
|
|
assign dblstop = r_setup[27];
|
146 |
|
|
assign use_parity = r_setup[26];
|
147 |
|
|
assign fixd_parity = r_setup[25];
|
148 |
26 |
dgisselq |
assign i_parity_odd = i_setup[24];
|
149 |
|
|
assign parity_odd = r_setup[24];
|
150 |
9 |
dgisselq |
assign fixdp_value = r_setup[24];
|
151 |
2 |
dgisselq |
|
152 |
|
|
reg [27:0] baud_counter;
|
153 |
|
|
reg [3:0] state;
|
154 |
|
|
reg [7:0] lcl_data;
|
155 |
26 |
dgisselq |
reg calc_parity, r_busy, zero_baud_counter, last_state;
|
156 |
2 |
dgisselq |
|
157 |
9 |
dgisselq |
|
158 |
|
|
// First step ... handle any hardware flow control, if so enabled.
|
159 |
|
|
//
|
160 |
|
|
// Clock in the flow control data, two clocks to avoid metastability
|
161 |
|
|
// Default to using hardware flow control (uart_setup[30]==0 to use it).
|
162 |
|
|
// Set this high order bit off if you do not wish to use it.
|
163 |
15 |
dgisselq |
reg q_cts_n, qq_cts_n, ck_cts;
|
164 |
|
|
// While we might wish to give initial values to q_rts and ck_cts,
|
165 |
9 |
dgisselq |
// 1) it's not required since the transmitter starts in a long wait
|
166 |
|
|
// state, and 2) doing so will prevent the synthesizer from optimizing
|
167 |
|
|
// this pin in the case it is hard set to 1'b1 external to this
|
168 |
|
|
// peripheral.
|
169 |
|
|
//
|
170 |
15 |
dgisselq |
// initial q_cts_n = 1'b1;
|
171 |
|
|
// initial qq_cts_n = 1'b1;
|
172 |
|
|
// initial ck_cts = 1'b0;
|
173 |
9 |
dgisselq |
always @(posedge i_clk)
|
174 |
26 |
dgisselq |
{ qq_cts_n, q_cts_n } <= { q_cts_n, i_cts_n };
|
175 |
9 |
dgisselq |
always @(posedge i_clk)
|
176 |
15 |
dgisselq |
ck_cts <= (!qq_cts_n)||(!hw_flow_control);
|
177 |
9 |
dgisselq |
|
178 |
5 |
dgisselq |
initial o_uart_tx = 1'b1;
|
179 |
2 |
dgisselq |
initial r_busy = 1'b1;
|
180 |
26 |
dgisselq |
initial state = TXU_IDLE;
|
181 |
2 |
dgisselq |
always @(posedge i_clk)
|
182 |
26 |
dgisselq |
if (i_reset)
|
183 |
2 |
dgisselq |
begin
|
184 |
26 |
dgisselq |
r_busy <= 1'b1;
|
185 |
|
|
state <= TXU_IDLE;
|
186 |
|
|
end else if (i_break)
|
187 |
|
|
begin
|
188 |
|
|
state <= TXU_BREAK;
|
189 |
|
|
r_busy <= 1'b1;
|
190 |
|
|
end else if (!zero_baud_counter)
|
191 |
|
|
begin // r_busy needs to be set coming into here
|
192 |
|
|
r_busy <= 1'b1;
|
193 |
|
|
end else if (state == TXU_BREAK)
|
194 |
|
|
begin
|
195 |
|
|
state <= TXU_IDLE;
|
196 |
|
|
r_busy <= !ck_cts;
|
197 |
|
|
end else if (state == TXU_IDLE) // STATE_IDLE
|
198 |
|
|
begin
|
199 |
|
|
if ((i_wr)&&(!r_busy))
|
200 |
|
|
begin // Immediately start us off with a start bit
|
201 |
2 |
dgisselq |
r_busy <= 1'b1;
|
202 |
26 |
dgisselq |
case(i_data_bits)
|
203 |
|
|
2'b00: state <= TXU_BIT_ZERO;
|
204 |
|
|
2'b01: state <= TXU_BIT_ONE;
|
205 |
|
|
2'b10: state <= TXU_BIT_TWO;
|
206 |
|
|
2'b11: state <= TXU_BIT_THREE;
|
207 |
|
|
endcase
|
208 |
|
|
end else begin // Stay in idle
|
209 |
|
|
r_busy <= !ck_cts;
|
210 |
|
|
end
|
211 |
|
|
end else begin
|
212 |
|
|
// One clock tick in each of these states ...
|
213 |
|
|
// baud_counter <= clocks_per_baud - 28'h01;
|
214 |
|
|
r_busy <= 1'b1;
|
215 |
|
|
if (state[3] == 0) // First 8 bits
|
216 |
2 |
dgisselq |
begin
|
217 |
26 |
dgisselq |
if (state == TXU_BIT_SEVEN)
|
218 |
|
|
state <= (use_parity)? TXU_PARITY:TXU_STOP;
|
219 |
|
|
else
|
220 |
|
|
state <= state + 1;
|
221 |
|
|
end else if (state == TXU_PARITY)
|
222 |
2 |
dgisselq |
begin
|
223 |
26 |
dgisselq |
state <= TXU_STOP;
|
224 |
|
|
end else if (state == TXU_STOP)
|
225 |
|
|
begin // two stop bit(s)
|
226 |
|
|
if (dblstop)
|
227 |
|
|
state <= TXU_SECOND_STOP;
|
228 |
|
|
else
|
229 |
|
|
state <= TXU_IDLE;
|
230 |
|
|
end else // `TXU_SECOND_STOP and default:
|
231 |
2 |
dgisselq |
begin
|
232 |
26 |
dgisselq |
state <= TXU_IDLE; // Go back to idle
|
233 |
|
|
// Still r_busy, since we need to wait
|
234 |
|
|
// for the baud clock to finish counting
|
235 |
|
|
// out this last bit.
|
236 |
|
|
end
|
237 |
|
|
end
|
238 |
2 |
dgisselq |
|
239 |
6 |
dgisselq |
// o_busy
|
240 |
|
|
//
|
241 |
|
|
// This is a wire, designed to be true is we are ever busy above.
|
242 |
|
|
// originally, this was going to be true if we were ever not in the
|
243 |
|
|
// idle state. The logic has since become more complex, hence we have
|
244 |
|
|
// a register dedicated to this and just copy out that registers value.
|
245 |
2 |
dgisselq |
assign o_busy = (r_busy);
|
246 |
|
|
|
247 |
|
|
|
248 |
6 |
dgisselq |
// r_setup
|
249 |
|
|
//
|
250 |
|
|
// Our setup register. Accept changes between any pair of transmitted
|
251 |
|
|
// words. The register itself has many fields to it. These are
|
252 |
|
|
// broken out up top, and indicate what 1) our baud rate is, 2) our
|
253 |
|
|
// number of stop bits, 3) what type of parity we are using, and 4)
|
254 |
|
|
// the size of our data word.
|
255 |
14 |
dgisselq |
initial r_setup = INITIAL_SETUP;
|
256 |
6 |
dgisselq |
always @(posedge i_clk)
|
257 |
26 |
dgisselq |
if (!o_busy)
|
258 |
|
|
r_setup <= i_setup;
|
259 |
6 |
dgisselq |
|
260 |
|
|
// lcl_data
|
261 |
|
|
//
|
262 |
|
|
// This is our working copy of the i_data register which we use
|
263 |
|
|
// when transmitting. It is only of interest during transmit, and is
|
264 |
|
|
// allowed to be whatever at any other time. Hence, if r_busy isn't
|
265 |
|
|
// true, we can always set it. On the one clock where r_busy isn't
|
266 |
|
|
// true and i_wr is, we set it and r_busy is true thereafter.
|
267 |
|
|
// Then, on any zero_baud_counter (i.e. change between baud intervals)
|
268 |
|
|
// we simple logically shift the register right to grab the next bit.
|
269 |
26 |
dgisselq |
initial lcl_data = 8'hff;
|
270 |
6 |
dgisselq |
always @(posedge i_clk)
|
271 |
26 |
dgisselq |
if (!r_busy)
|
272 |
|
|
lcl_data <= i_data;
|
273 |
|
|
else if (zero_baud_counter)
|
274 |
|
|
lcl_data <= { 1'b0, lcl_data[7:1] };
|
275 |
6 |
dgisselq |
|
276 |
|
|
// o_uart_tx
|
277 |
|
|
//
|
278 |
|
|
// This is the final result/output desired of this core. It's all
|
279 |
|
|
// centered about o_uart_tx. This is what finally needs to follow
|
280 |
|
|
// the UART protocol.
|
281 |
|
|
//
|
282 |
|
|
// Ok, that said, our rules are:
|
283 |
|
|
// 1'b0 on any break condition
|
284 |
|
|
// 1'b0 on a start bit (IDLE, write, and not busy)
|
285 |
|
|
// lcl_data[0] during any data transfer, but only at the baud
|
286 |
|
|
// change
|
287 |
|
|
// PARITY -- During the parity bit. This depends upon whether or
|
288 |
|
|
// not the parity bit is fixed, then what it's fixed to,
|
289 |
|
|
// or changing, and hence what it's calculated value is.
|
290 |
|
|
// 1'b1 at all other times (stop bits, idle, etc)
|
291 |
|
|
always @(posedge i_clk)
|
292 |
26 |
dgisselq |
if (i_reset)
|
293 |
|
|
o_uart_tx <= 1'b1;
|
294 |
|
|
else if ((i_break)||((i_wr)&&(!r_busy)))
|
295 |
|
|
o_uart_tx <= 1'b0;
|
296 |
|
|
else if (zero_baud_counter)
|
297 |
|
|
casez(state)
|
298 |
|
|
4'b0???: o_uart_tx <= lcl_data[0];
|
299 |
|
|
TXU_PARITY: o_uart_tx <= calc_parity;
|
300 |
|
|
default: o_uart_tx <= 1'b1;
|
301 |
|
|
endcase
|
302 |
6 |
dgisselq |
|
303 |
|
|
|
304 |
|
|
// calc_parity
|
305 |
|
|
//
|
306 |
|
|
// Calculate the parity to be placed into the parity bit. If the
|
307 |
|
|
// parity is fixed, then the parity bit is given by the fixed parity
|
308 |
|
|
// value (r_setup[24]). Otherwise the parity is given by the GF2
|
309 |
|
|
// sum of all the data bits (plus one for even parity).
|
310 |
26 |
dgisselq |
initial calc_parity = 1'b0;
|
311 |
6 |
dgisselq |
always @(posedge i_clk)
|
312 |
26 |
dgisselq |
if (!o_busy)
|
313 |
|
|
calc_parity <= i_setup[24];
|
314 |
|
|
else if (fixd_parity)
|
315 |
|
|
calc_parity <= fixdp_value;
|
316 |
|
|
else if (zero_baud_counter)
|
317 |
|
|
begin
|
318 |
|
|
if (state[3] == 0) // First 8 bits of msg
|
319 |
|
|
calc_parity <= calc_parity ^ lcl_data[0];
|
320 |
|
|
else if (state == TXU_IDLE)
|
321 |
|
|
calc_parity <= parity_odd;
|
322 |
|
|
end else if (!r_busy)
|
323 |
|
|
calc_parity <= parity_odd;
|
324 |
6 |
dgisselq |
|
325 |
|
|
|
326 |
|
|
// All of the above logic is driven by the baud counter. Bits must last
|
327 |
|
|
// clocks_per_baud in length, and this baud counter is what we use to
|
328 |
|
|
// make certain of that.
|
329 |
|
|
//
|
330 |
|
|
// The basic logic is this: at the beginning of a bit interval, start
|
331 |
|
|
// the baud counter and set it to count clocks_per_baud. When it gets
|
332 |
|
|
// to zero, restart it.
|
333 |
|
|
//
|
334 |
|
|
// However, comparing a 28'bit number to zero can be rather complex--
|
335 |
|
|
// especially if we wish to do anything else on that same clock. For
|
336 |
|
|
// that reason, we create "zero_baud_counter". zero_baud_counter is
|
337 |
|
|
// nothing more than a flag that is true anytime baud_counter is zero.
|
338 |
|
|
// It's true when the logic (above) needs to step to the next bit.
|
339 |
|
|
// Simple enough?
|
340 |
|
|
//
|
341 |
|
|
// I wish we could stop there, but there are some other (ugly)
|
342 |
|
|
// conditions to deal with that offer exceptions to this basic logic.
|
343 |
|
|
//
|
344 |
|
|
// 1. When the user has commanded a BREAK across the line, we need to
|
345 |
|
|
// wait several baud intervals following the break before we start
|
346 |
|
|
// transmitting, to give any receiver a chance to recognize that we are
|
347 |
|
|
// out of the break condition, and to know that the next bit will be
|
348 |
|
|
// a stop bit.
|
349 |
|
|
//
|
350 |
|
|
// 2. A reset is similar to a break condition--on both we wait several
|
351 |
|
|
// baud intervals before allowing a start bit.
|
352 |
|
|
//
|
353 |
|
|
// 3. In the idle state, we stop our counter--so that upon a request
|
354 |
|
|
// to transmit when idle we can start transmitting immediately, rather
|
355 |
|
|
// than waiting for the end of the next (fictitious and arbitrary) baud
|
356 |
|
|
// interval.
|
357 |
|
|
//
|
358 |
26 |
dgisselq |
// When (i_wr)&&(!r_busy)&&(state == TXU_IDLE) then we're not only in
|
359 |
6 |
dgisselq |
// the idle state, but we also just accepted a command to start writing
|
360 |
|
|
// the next word. At this point, the baud counter needs to be reset
|
361 |
|
|
// to the number of clocks per baud, and zero_baud_counter set to zero.
|
362 |
|
|
//
|
363 |
|
|
// The logic is a bit twisted here, in that it will only check for the
|
364 |
|
|
// above condition when zero_baud_counter is false--so as to make
|
365 |
|
|
// certain the STOP bit is complete.
|
366 |
2 |
dgisselq |
initial zero_baud_counter = 1'b0;
|
367 |
|
|
initial baud_counter = 28'h05;
|
368 |
|
|
always @(posedge i_clk)
|
369 |
|
|
begin
|
370 |
|
|
zero_baud_counter <= (baud_counter == 28'h01);
|
371 |
|
|
if ((i_reset)||(i_break))
|
372 |
5 |
dgisselq |
begin
|
373 |
2 |
dgisselq |
// Give ourselves 16 bauds before being ready
|
374 |
|
|
baud_counter <= break_condition;
|
375 |
5 |
dgisselq |
zero_baud_counter <= 1'b0;
|
376 |
6 |
dgisselq |
end else if (!zero_baud_counter)
|
377 |
2 |
dgisselq |
baud_counter <= baud_counter - 28'h01;
|
378 |
26 |
dgisselq |
else if (state == TXU_BREAK)
|
379 |
2 |
dgisselq |
begin
|
380 |
26 |
dgisselq |
baud_counter <= 0;
|
381 |
|
|
zero_baud_counter <= 1'b1;
|
382 |
|
|
end else if (state == TXU_IDLE)
|
383 |
|
|
begin
|
384 |
6 |
dgisselq |
baud_counter <= 28'h0;
|
385 |
|
|
zero_baud_counter <= 1'b1;
|
386 |
|
|
if ((i_wr)&&(!r_busy))
|
387 |
|
|
begin
|
388 |
26 |
dgisselq |
baud_counter <= { 4'h0, i_setup[23:0]} - 28'h01;
|
389 |
6 |
dgisselq |
zero_baud_counter <= 1'b0;
|
390 |
|
|
end
|
391 |
26 |
dgisselq |
end else if (last_state)
|
392 |
|
|
baud_counter <= clocks_per_baud - 28'h02;
|
393 |
|
|
else
|
394 |
2 |
dgisselq |
baud_counter <= clocks_per_baud - 28'h01;
|
395 |
|
|
end
|
396 |
23 |
dgisselq |
|
397 |
26 |
dgisselq |
initial last_state = 1'b0;
|
398 |
|
|
always @(posedge i_clk)
|
399 |
|
|
if (dblstop)
|
400 |
|
|
last_state <= (state == TXU_SECOND_STOP);
|
401 |
|
|
else
|
402 |
|
|
last_state <= (state == TXU_STOP);
|
403 |
|
|
|
404 |
23 |
dgisselq |
`ifdef FORMAL
|
405 |
|
|
reg fsv_parity;
|
406 |
|
|
reg [30:0] fsv_setup;
|
407 |
|
|
reg [7:0] fsv_data;
|
408 |
26 |
dgisselq |
reg f_past_valid;
|
409 |
23 |
dgisselq |
|
410 |
26 |
dgisselq |
initial f_past_valid = 1'b0;
|
411 |
|
|
always @(posedge i_clk)
|
412 |
|
|
f_past_valid <= 1'b1;
|
413 |
|
|
|
414 |
23 |
dgisselq |
always @(posedge i_clk)
|
415 |
26 |
dgisselq |
if ((i_wr)&&(!o_busy))
|
416 |
|
|
fsv_data <= i_data;
|
417 |
23 |
dgisselq |
|
418 |
26 |
dgisselq |
initial fsv_setup = INITIAL_SETUP;
|
419 |
23 |
dgisselq |
always @(posedge i_clk)
|
420 |
26 |
dgisselq |
if (!o_busy)
|
421 |
|
|
fsv_setup <= i_setup;
|
422 |
23 |
dgisselq |
|
423 |
26 |
dgisselq |
always @(*)
|
424 |
|
|
assert(r_setup == fsv_setup);
|
425 |
|
|
|
426 |
|
|
|
427 |
23 |
dgisselq |
always @(posedge i_clk)
|
428 |
|
|
assert(zero_baud_counter == (baud_counter == 0));
|
429 |
|
|
|
430 |
|
|
always @(*)
|
431 |
26 |
dgisselq |
if (!o_busy)
|
432 |
|
|
assert(zero_baud_counter);
|
433 |
23 |
dgisselq |
|
434 |
26 |
dgisselq |
/*
|
435 |
|
|
*
|
436 |
|
|
* Will only pass if !i_break && !i_reset, otherwise the setup can
|
437 |
|
|
* change in the middle of this operation
|
438 |
|
|
*
|
439 |
|
|
always @(posedge i_clk)
|
440 |
|
|
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_break))
|
441 |
|
|
&&(($past(o_busy))||($past(i_wr))))
|
442 |
|
|
assert(baud_counter <= { fsv_setup[23:0], 4'h0 });
|
443 |
|
|
*/
|
444 |
|
|
|
445 |
23 |
dgisselq |
// A single baud interval
|
446 |
26 |
dgisselq |
always @(posedge i_clk)
|
447 |
|
|
if ((f_past_valid)&&(!$past(zero_baud_counter))
|
448 |
|
|
&&(!$past(i_reset))&&(!$past(i_break)))
|
449 |
|
|
begin
|
450 |
|
|
assert($stable(o_uart_tx));
|
451 |
|
|
assert($stable(state));
|
452 |
|
|
assert($stable(lcl_data));
|
453 |
|
|
if ((state != TXU_IDLE)&&(state != TXU_BREAK))
|
454 |
|
|
assert($stable(calc_parity));
|
455 |
|
|
assert(baud_counter == $past(baud_counter)-1'b1);
|
456 |
|
|
end
|
457 |
23 |
dgisselq |
|
458 |
|
|
//
|
459 |
26 |
dgisselq |
// Our various sequence data declarations
|
460 |
|
|
reg [5:0] f_five_seq;
|
461 |
|
|
reg [6:0] f_six_seq;
|
462 |
|
|
reg [7:0] f_seven_seq;
|
463 |
|
|
reg [8:0] f_eight_seq;
|
464 |
|
|
reg [2:0] f_stop_seq; // parity bit, stop bit, double stop bit
|
465 |
|
|
|
466 |
|
|
|
467 |
|
|
//
|
468 |
23 |
dgisselq |
// One byte transmitted
|
469 |
|
|
//
|
470 |
|
|
// DATA = the byte that is sent
|
471 |
|
|
// CKS = the number of clocks per bit
|
472 |
|
|
//
|
473 |
26 |
dgisselq |
////////////////////////////////////////////////////////////////////////
|
474 |
|
|
//
|
475 |
|
|
// Five bit data
|
476 |
|
|
//
|
477 |
|
|
////////////////////////////////////////////////////////////////////////
|
478 |
23 |
dgisselq |
|
479 |
26 |
dgisselq |
initial f_five_seq = 0;
|
480 |
|
|
always @(posedge i_clk)
|
481 |
|
|
if ((i_reset)||(i_break))
|
482 |
|
|
f_five_seq = 0;
|
483 |
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
484 |
|
|
&&(i_data_bits == 2'b11)) // five data bits
|
485 |
|
|
f_five_seq <= 1;
|
486 |
|
|
else if (zero_baud_counter)
|
487 |
|
|
f_five_seq <= f_five_seq << 1;
|
488 |
23 |
dgisselq |
|
489 |
26 |
dgisselq |
always @(*)
|
490 |
|
|
if (|f_five_seq)
|
491 |
|
|
begin
|
492 |
|
|
assert(fsv_setup[29:28] == data_bits);
|
493 |
|
|
assert(data_bits == 2'b11);
|
494 |
|
|
assert(baud_counter < fsv_setup[23:0]);
|
495 |
23 |
dgisselq |
|
496 |
26 |
dgisselq |
assert(1'b0 == |f_six_seq);
|
497 |
|
|
assert(1'b0 == |f_seven_seq);
|
498 |
|
|
assert(1'b0 == |f_eight_seq);
|
499 |
|
|
assert(r_busy);
|
500 |
|
|
assert(state > 4'h2);
|
501 |
|
|
end
|
502 |
23 |
dgisselq |
|
503 |
26 |
dgisselq |
always @(*)
|
504 |
|
|
case(f_five_seq)
|
505 |
|
|
6'h00: begin assert(1); end
|
506 |
|
|
6'h01: begin
|
507 |
|
|
assert(state == 4'h3);
|
508 |
|
|
assert(o_uart_tx == 1'b0);
|
509 |
|
|
assert(lcl_data[4:0] == fsv_data[4:0]);
|
510 |
|
|
if (!fixd_parity)
|
511 |
|
|
assert(calc_parity == parity_odd);
|
512 |
|
|
end
|
513 |
|
|
6'h02: begin
|
514 |
|
|
assert(state == 4'h4);
|
515 |
|
|
assert(o_uart_tx == fsv_data[0]);
|
516 |
|
|
assert(lcl_data[3:0] == fsv_data[4:1]);
|
517 |
|
|
if (!fixd_parity)
|
518 |
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
519 |
|
|
end
|
520 |
|
|
6'h04: begin
|
521 |
|
|
assert(state == 4'h5);
|
522 |
|
|
assert(o_uart_tx == fsv_data[1]);
|
523 |
|
|
assert(lcl_data[2:0] == fsv_data[4:2]);
|
524 |
|
|
if (!fixd_parity)
|
525 |
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
526 |
|
|
end
|
527 |
|
|
6'h08: begin
|
528 |
|
|
assert(state == 4'h6);
|
529 |
|
|
assert(o_uart_tx == fsv_data[2]);
|
530 |
|
|
assert(lcl_data[1:0] == fsv_data[4:3]);
|
531 |
|
|
if (!fixd_parity)
|
532 |
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
533 |
|
|
end
|
534 |
|
|
6'h10: begin
|
535 |
|
|
assert(state == 4'h7);
|
536 |
|
|
assert(o_uart_tx == fsv_data[3]);
|
537 |
|
|
assert(lcl_data[0] == fsv_data[4]);
|
538 |
|
|
if (!fixd_parity)
|
539 |
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
540 |
|
|
end
|
541 |
|
|
6'h20: begin
|
542 |
|
|
if (use_parity)
|
543 |
|
|
assert(state == 4'h8);
|
544 |
|
|
else
|
545 |
|
|
assert(state == 4'h9);
|
546 |
|
|
assert(o_uart_tx == fsv_data[4]);
|
547 |
|
|
if (!fixd_parity)
|
548 |
|
|
assert(calc_parity == (^fsv_data[4:0]) ^ parity_odd);
|
549 |
|
|
end
|
550 |
|
|
default: begin assert(0); end
|
551 |
|
|
endcase
|
552 |
|
|
|
553 |
|
|
////////////////////////////////////////////////////////////////////////
|
554 |
|
|
//
|
555 |
|
|
// Six bit data
|
556 |
|
|
//
|
557 |
|
|
////////////////////////////////////////////////////////////////////////
|
558 |
|
|
|
559 |
|
|
initial f_six_seq = 0;
|
560 |
23 |
dgisselq |
always @(posedge i_clk)
|
561 |
26 |
dgisselq |
if ((i_reset)||(i_break))
|
562 |
|
|
f_six_seq = 0;
|
563 |
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
564 |
|
|
&&(i_data_bits == 2'b10)) // six data bits
|
565 |
|
|
f_six_seq <= 1;
|
566 |
|
|
else if (zero_baud_counter)
|
567 |
|
|
f_six_seq <= f_six_seq << 1;
|
568 |
23 |
dgisselq |
|
569 |
26 |
dgisselq |
always @(*)
|
570 |
|
|
if (|f_six_seq)
|
571 |
|
|
begin
|
572 |
|
|
assert(fsv_setup[29:28] == 2'b10);
|
573 |
|
|
assert(fsv_setup[29:28] == data_bits);
|
574 |
|
|
assert(baud_counter < fsv_setup[23:0]);
|
575 |
23 |
dgisselq |
|
576 |
26 |
dgisselq |
assert(1'b0 == |f_five_seq);
|
577 |
|
|
assert(1'b0 == |f_seven_seq);
|
578 |
|
|
assert(1'b0 == |f_eight_seq);
|
579 |
|
|
assert(r_busy);
|
580 |
|
|
assert(state > 4'h1);
|
581 |
|
|
end
|
582 |
23 |
dgisselq |
|
583 |
26 |
dgisselq |
always @(*)
|
584 |
|
|
case(f_six_seq)
|
585 |
|
|
7'h00: begin assert(1); end
|
586 |
|
|
7'h01: begin
|
587 |
|
|
assert(state == 4'h2);
|
588 |
|
|
assert(o_uart_tx == 1'b0);
|
589 |
|
|
assert(lcl_data[5:0] == fsv_data[5:0]);
|
590 |
|
|
if (!fixd_parity)
|
591 |
|
|
assert(calc_parity == parity_odd);
|
592 |
|
|
end
|
593 |
|
|
7'h02: begin
|
594 |
|
|
assert(state == 4'h3);
|
595 |
|
|
assert(o_uart_tx == fsv_data[0]);
|
596 |
|
|
assert(lcl_data[4:0] == fsv_data[5:1]);
|
597 |
|
|
if (!fixd_parity)
|
598 |
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
599 |
|
|
end
|
600 |
|
|
7'h04: begin
|
601 |
|
|
assert(state == 4'h4);
|
602 |
|
|
assert(o_uart_tx == fsv_data[1]);
|
603 |
|
|
assert(lcl_data[3:0] == fsv_data[5:2]);
|
604 |
|
|
if (!fixd_parity)
|
605 |
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
606 |
|
|
end
|
607 |
|
|
7'h08: begin
|
608 |
|
|
assert(state == 4'h5);
|
609 |
|
|
assert(o_uart_tx == fsv_data[2]);
|
610 |
|
|
assert(lcl_data[2:0] == fsv_data[5:3]);
|
611 |
|
|
if (!fixd_parity)
|
612 |
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
613 |
|
|
end
|
614 |
|
|
7'h10: begin
|
615 |
|
|
assert(state == 4'h6);
|
616 |
|
|
assert(o_uart_tx == fsv_data[3]);
|
617 |
|
|
assert(lcl_data[1:0] == fsv_data[5:4]);
|
618 |
|
|
if (!fixd_parity)
|
619 |
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
620 |
|
|
end
|
621 |
|
|
7'h20: begin
|
622 |
|
|
assert(state == 4'h7);
|
623 |
|
|
assert(lcl_data[0] == fsv_data[5]);
|
624 |
|
|
assert(o_uart_tx == fsv_data[4]);
|
625 |
|
|
if (!fixd_parity)
|
626 |
|
|
assert(calc_parity == ((^fsv_data[4:0]) ^ parity_odd));
|
627 |
|
|
end
|
628 |
|
|
7'h40: begin
|
629 |
|
|
if (use_parity)
|
630 |
|
|
assert(state == 4'h8);
|
631 |
|
|
else
|
632 |
|
|
assert(state == 4'h9);
|
633 |
|
|
assert(o_uart_tx == fsv_data[5]);
|
634 |
|
|
if (!fixd_parity)
|
635 |
|
|
assert(calc_parity == ((^fsv_data[5:0]) ^ parity_odd));
|
636 |
|
|
end
|
637 |
|
|
default: begin if (f_past_valid) assert(0); end
|
638 |
|
|
endcase
|
639 |
23 |
dgisselq |
|
640 |
26 |
dgisselq |
////////////////////////////////////////////////////////////////////////
|
641 |
|
|
//
|
642 |
|
|
// Seven bit data
|
643 |
|
|
//
|
644 |
|
|
////////////////////////////////////////////////////////////////////////
|
645 |
|
|
initial f_seven_seq = 0;
|
646 |
|
|
always @(posedge i_clk)
|
647 |
|
|
if ((i_reset)||(i_break))
|
648 |
|
|
f_seven_seq = 0;
|
649 |
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
650 |
|
|
&&(i_data_bits == 2'b01)) // seven data bits
|
651 |
|
|
f_seven_seq <= 1;
|
652 |
|
|
else if (zero_baud_counter)
|
653 |
|
|
f_seven_seq <= f_seven_seq << 1;
|
654 |
23 |
dgisselq |
|
655 |
26 |
dgisselq |
always @(*)
|
656 |
|
|
if (|f_seven_seq)
|
657 |
|
|
begin
|
658 |
|
|
assert(fsv_setup[29:28] == 2'b01);
|
659 |
|
|
assert(fsv_setup[29:28] == data_bits);
|
660 |
|
|
assert(baud_counter < fsv_setup[23:0]);
|
661 |
23 |
dgisselq |
|
662 |
26 |
dgisselq |
assert(1'b0 == |f_five_seq);
|
663 |
|
|
assert(1'b0 == |f_six_seq);
|
664 |
|
|
assert(1'b0 == |f_eight_seq);
|
665 |
|
|
assert(r_busy);
|
666 |
|
|
assert(state != 4'h0);
|
667 |
|
|
end
|
668 |
23 |
dgisselq |
|
669 |
26 |
dgisselq |
always @(*)
|
670 |
|
|
case(f_seven_seq)
|
671 |
|
|
8'h00: begin assert(1); end
|
672 |
|
|
8'h01: begin
|
673 |
|
|
assert(state == 4'h1);
|
674 |
|
|
assert(o_uart_tx == 1'b0);
|
675 |
|
|
assert(lcl_data[6:0] == fsv_data[6:0]);
|
676 |
|
|
if (!fixd_parity)
|
677 |
|
|
assert(calc_parity == parity_odd);
|
678 |
|
|
end
|
679 |
|
|
8'h02: begin
|
680 |
|
|
assert(state == 4'h2);
|
681 |
|
|
assert(o_uart_tx == fsv_data[0]);
|
682 |
|
|
assert(lcl_data[5:0] == fsv_data[6:1]);
|
683 |
|
|
if (!fixd_parity)
|
684 |
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
685 |
|
|
end
|
686 |
|
|
8'h04: begin
|
687 |
|
|
assert(state == 4'h3);
|
688 |
|
|
assert(o_uart_tx == fsv_data[1]);
|
689 |
|
|
assert(lcl_data[4:0] == fsv_data[6:2]);
|
690 |
|
|
if (!fixd_parity)
|
691 |
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
692 |
|
|
end
|
693 |
|
|
8'h08: begin
|
694 |
|
|
assert(state == 4'h4);
|
695 |
|
|
assert(o_uart_tx == fsv_data[2]);
|
696 |
|
|
assert(lcl_data[3:0] == fsv_data[6:3]);
|
697 |
|
|
if (!fixd_parity)
|
698 |
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
699 |
|
|
end
|
700 |
|
|
8'h10: begin
|
701 |
|
|
assert(state == 4'h5);
|
702 |
|
|
assert(o_uart_tx == fsv_data[3]);
|
703 |
|
|
assert(lcl_data[2:0] == fsv_data[6:4]);
|
704 |
|
|
if (!fixd_parity)
|
705 |
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
706 |
|
|
end
|
707 |
|
|
8'h20: begin
|
708 |
|
|
assert(state == 4'h6);
|
709 |
|
|
assert(o_uart_tx == fsv_data[4]);
|
710 |
|
|
assert(lcl_data[1:0] == fsv_data[6:5]);
|
711 |
|
|
if (!fixd_parity)
|
712 |
|
|
assert(calc_parity == ((^fsv_data[4:0]) ^ parity_odd));
|
713 |
|
|
end
|
714 |
|
|
8'h40: begin
|
715 |
|
|
assert(state == 4'h7);
|
716 |
|
|
assert(lcl_data[0] == fsv_data[6]);
|
717 |
|
|
assert(o_uart_tx == fsv_data[5]);
|
718 |
|
|
if (!fixd_parity)
|
719 |
|
|
assert(calc_parity == ((^fsv_data[5:0]) ^ parity_odd));
|
720 |
|
|
end
|
721 |
|
|
8'h80: begin
|
722 |
|
|
if (use_parity)
|
723 |
|
|
assert(state == 4'h8);
|
724 |
|
|
else
|
725 |
|
|
assert(state == 4'h9);
|
726 |
|
|
assert(o_uart_tx == fsv_data[6]);
|
727 |
|
|
if (!fixd_parity)
|
728 |
|
|
assert(calc_parity == ((^fsv_data[6:0]) ^ parity_odd));
|
729 |
|
|
end
|
730 |
|
|
default: begin if (f_past_valid) assert(0); end
|
731 |
|
|
endcase
|
732 |
23 |
dgisselq |
|
733 |
|
|
|
734 |
26 |
dgisselq |
////////////////////////////////////////////////////////////////////////
|
735 |
|
|
//
|
736 |
|
|
// Eight bit data
|
737 |
|
|
//
|
738 |
|
|
////////////////////////////////////////////////////////////////////////
|
739 |
|
|
initial f_eight_seq = 0;
|
740 |
|
|
always @(posedge i_clk)
|
741 |
|
|
if ((i_reset)||(i_break))
|
742 |
|
|
f_eight_seq = 0;
|
743 |
|
|
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy)
|
744 |
|
|
&&(i_data_bits == 2'b00)) // Eight data bits
|
745 |
|
|
f_eight_seq <= 1;
|
746 |
|
|
else if (zero_baud_counter)
|
747 |
|
|
f_eight_seq <= f_eight_seq << 1;
|
748 |
23 |
dgisselq |
|
749 |
26 |
dgisselq |
always @(*)
|
750 |
|
|
if (|f_eight_seq)
|
751 |
|
|
begin
|
752 |
|
|
assert(fsv_setup[29:28] == 2'b00);
|
753 |
|
|
assert(fsv_setup[29:28] == data_bits);
|
754 |
|
|
assert(baud_counter < { 6'h0, fsv_setup[23:0]});
|
755 |
23 |
dgisselq |
|
756 |
26 |
dgisselq |
assert(1'b0 == |f_five_seq);
|
757 |
|
|
assert(1'b0 == |f_six_seq);
|
758 |
|
|
assert(1'b0 == |f_seven_seq);
|
759 |
|
|
assert(r_busy);
|
760 |
|
|
end
|
761 |
23 |
dgisselq |
|
762 |
26 |
dgisselq |
always @(*)
|
763 |
|
|
case(f_eight_seq)
|
764 |
|
|
9'h000: begin assert(1); end
|
765 |
|
|
9'h001: begin
|
766 |
|
|
assert(state == 4'h0);
|
767 |
|
|
assert(o_uart_tx == 1'b0);
|
768 |
|
|
assert(lcl_data[7:0] == fsv_data[7:0]);
|
769 |
|
|
if (!fixd_parity)
|
770 |
|
|
assert(calc_parity == parity_odd);
|
771 |
|
|
end
|
772 |
|
|
9'h002: begin
|
773 |
|
|
assert(state == 4'h1);
|
774 |
|
|
assert(o_uart_tx == fsv_data[0]);
|
775 |
|
|
assert(lcl_data[6:0] == fsv_data[7:1]);
|
776 |
|
|
if (!fixd_parity)
|
777 |
|
|
assert(calc_parity == fsv_data[0] ^ parity_odd);
|
778 |
|
|
end
|
779 |
|
|
9'h004: begin
|
780 |
|
|
assert(state == 4'h2);
|
781 |
|
|
assert(o_uart_tx == fsv_data[1]);
|
782 |
|
|
assert(lcl_data[5:0] == fsv_data[7:2]);
|
783 |
|
|
if (!fixd_parity)
|
784 |
|
|
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd);
|
785 |
|
|
end
|
786 |
|
|
9'h008: begin
|
787 |
|
|
assert(state == 4'h3);
|
788 |
|
|
assert(o_uart_tx == fsv_data[2]);
|
789 |
|
|
assert(lcl_data[4:0] == fsv_data[7:3]);
|
790 |
|
|
if (!fixd_parity)
|
791 |
|
|
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd);
|
792 |
|
|
end
|
793 |
|
|
9'h010: begin
|
794 |
|
|
assert(state == 4'h4);
|
795 |
|
|
assert(o_uart_tx == fsv_data[3]);
|
796 |
|
|
assert(lcl_data[3:0] == fsv_data[7:4]);
|
797 |
|
|
if (!fixd_parity)
|
798 |
|
|
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd);
|
799 |
|
|
end
|
800 |
|
|
9'h020: begin
|
801 |
|
|
assert(state == 4'h5);
|
802 |
|
|
assert(o_uart_tx == fsv_data[4]);
|
803 |
|
|
assert(lcl_data[2:0] == fsv_data[7:5]);
|
804 |
|
|
if (!fixd_parity)
|
805 |
|
|
assert(calc_parity == (^fsv_data[4:0]) ^ parity_odd);
|
806 |
|
|
end
|
807 |
|
|
9'h040: begin
|
808 |
|
|
assert(state == 4'h6);
|
809 |
|
|
assert(o_uart_tx == fsv_data[5]);
|
810 |
|
|
assert(lcl_data[1:0] == fsv_data[7:6]);
|
811 |
|
|
if (!fixd_parity)
|
812 |
|
|
assert(calc_parity == (^fsv_data[5:0]) ^ parity_odd);
|
813 |
|
|
end
|
814 |
|
|
9'h080: begin
|
815 |
|
|
assert(state == 4'h7);
|
816 |
|
|
assert(o_uart_tx == fsv_data[6]);
|
817 |
|
|
assert(lcl_data[0] == fsv_data[7]);
|
818 |
|
|
if (!fixd_parity)
|
819 |
|
|
assert(calc_parity == ((^fsv_data[6:0]) ^ parity_odd));
|
820 |
|
|
end
|
821 |
|
|
9'h100: begin
|
822 |
|
|
if (use_parity)
|
823 |
|
|
assert(state == 4'h8);
|
824 |
|
|
else
|
825 |
|
|
assert(state == 4'h9);
|
826 |
|
|
assert(o_uart_tx == fsv_data[7]);
|
827 |
|
|
if (!fixd_parity)
|
828 |
|
|
assert(calc_parity == ((^fsv_data[7:0]) ^ parity_odd));
|
829 |
|
|
end
|
830 |
|
|
default: begin if (f_past_valid) assert(0); end
|
831 |
|
|
endcase
|
832 |
23 |
dgisselq |
|
833 |
26 |
dgisselq |
////////////////////////////////////////////////////////////////////////
|
834 |
|
|
//
|
835 |
|
|
// Combined properties for all of the data sequences
|
836 |
|
|
//
|
837 |
|
|
////////////////////////////////////////////////////////////////////////
|
838 |
|
|
always @(posedge i_clk)
|
839 |
|
|
if (((|f_five_seq[5:0]) || (|f_six_seq[6:0]) || (|f_seven_seq[7:0])
|
840 |
|
|
|| (|f_eight_seq[8:0]))
|
841 |
|
|
&& ($past(zero_baud_counter)))
|
842 |
|
|
assert(baud_counter == { 4'h0, fsv_setup[23:0] }-1);
|
843 |
23 |
dgisselq |
|
844 |
26 |
dgisselq |
|
845 |
|
|
////////////////////////////////////////////////////////////////////////
|
846 |
|
|
//
|
847 |
|
|
// The stop sequence
|
848 |
|
|
//
|
849 |
|
|
// This consists of any parity bit, as well as one or two stop bits
|
850 |
|
|
////////////////////////////////////////////////////////////////////////
|
851 |
|
|
initial f_stop_seq = 1'b0;
|
852 |
|
|
always @(posedge i_clk)
|
853 |
|
|
if ((i_reset)||(i_break))
|
854 |
|
|
f_stop_seq <= 0;
|
855 |
|
|
else if (zero_baud_counter)
|
856 |
|
|
begin
|
857 |
|
|
f_stop_seq <= 0;
|
858 |
|
|
if (f_stop_seq[0]) // Coming from a parity bit
|
859 |
|
|
begin
|
860 |
|
|
if (dblstop)
|
861 |
|
|
f_stop_seq[1] <= 1'b1;
|
862 |
|
|
else
|
863 |
|
|
f_stop_seq[2] <= 1'b1;
|
864 |
|
|
end
|
865 |
|
|
|
866 |
|
|
if (f_stop_seq[1])
|
867 |
|
|
f_stop_seq[2] <= 1'b1;
|
868 |
|
|
|
869 |
|
|
if (f_eight_seq[8] | f_seven_seq[7] | f_six_seq[6]
|
870 |
|
|
| f_five_seq[5])
|
871 |
|
|
begin
|
872 |
|
|
if (use_parity)
|
873 |
|
|
f_stop_seq[0] <= 1'b1;
|
874 |
|
|
else if (dblstop)
|
875 |
|
|
f_stop_seq[1] <= 1'b1;
|
876 |
|
|
else
|
877 |
|
|
f_stop_seq[2] <= 1'b1;
|
878 |
|
|
end
|
879 |
|
|
end
|
880 |
|
|
|
881 |
|
|
always @(*)
|
882 |
|
|
if (|f_stop_seq)
|
883 |
|
|
begin
|
884 |
|
|
assert(1'b0 == |f_five_seq[4:0]);
|
885 |
|
|
assert(1'b0 == |f_six_seq[5:0]);
|
886 |
|
|
assert(1'b0 == |f_seven_seq[6:0]);
|
887 |
|
|
assert(1'b0 == |f_eight_seq[7:0]);
|
888 |
|
|
|
889 |
|
|
assert(r_busy);
|
890 |
|
|
end
|
891 |
|
|
|
892 |
|
|
always @(*)
|
893 |
|
|
if (f_stop_seq[0])
|
894 |
|
|
begin
|
895 |
|
|
// 9 if dblstop and use_parity
|
896 |
|
|
if (dblstop)
|
897 |
|
|
assert(state == TXU_STOP);
|
898 |
|
|
else
|
899 |
|
|
assert(state == TXU_STOP);
|
900 |
|
|
assert(use_parity);
|
901 |
|
|
assert(o_uart_tx == fsv_parity);
|
902 |
|
|
end
|
903 |
|
|
|
904 |
|
|
always @(*)
|
905 |
|
|
if (f_stop_seq[1])
|
906 |
|
|
begin
|
907 |
|
|
// if (!use_parity)
|
908 |
|
|
assert(state == TXU_SECOND_STOP);
|
909 |
|
|
assert(dblstop);
|
910 |
|
|
assert(o_uart_tx);
|
911 |
|
|
end
|
912 |
|
|
|
913 |
|
|
always @(*)
|
914 |
|
|
if (f_stop_seq[2])
|
915 |
|
|
begin
|
916 |
|
|
assert(state == 4'hf);
|
917 |
|
|
assert(o_uart_tx);
|
918 |
|
|
assert(baud_counter < fsv_setup[23:0]-1'b1);
|
919 |
|
|
end
|
920 |
|
|
|
921 |
|
|
|
922 |
|
|
always @(*)
|
923 |
|
|
if (fsv_setup[25])
|
924 |
|
|
fsv_parity <= fsv_setup[24];
|
925 |
|
|
else
|
926 |
|
|
case(fsv_setup[29:28])
|
927 |
|
|
2'b00: fsv_parity = (^fsv_data[7:0]) ^ fsv_setup[24];
|
928 |
|
|
2'b01: fsv_parity = (^fsv_data[6:0]) ^ fsv_setup[24];
|
929 |
|
|
2'b10: fsv_parity = (^fsv_data[5:0]) ^ fsv_setup[24];
|
930 |
|
|
2'b11: fsv_parity = (^fsv_data[4:0]) ^ fsv_setup[24];
|
931 |
|
|
endcase
|
932 |
|
|
|
933 |
|
|
//////////////////////////////////////////////////////////////////////
|
934 |
|
|
//
|
935 |
|
|
// The break sequence
|
936 |
|
|
//
|
937 |
|
|
//////////////////////////////////////////////////////////////////////
|
938 |
|
|
reg [1:0] f_break_seq;
|
939 |
|
|
initial f_break_seq = 2'b00;
|
940 |
|
|
always @(posedge i_clk)
|
941 |
|
|
if (i_reset)
|
942 |
|
|
f_break_seq <= 2'b00;
|
943 |
|
|
else if (i_break)
|
944 |
|
|
f_break_seq <= 2'b01;
|
945 |
|
|
else if (!zero_baud_counter)
|
946 |
|
|
f_break_seq <= { |f_break_seq, 1'b0 };
|
947 |
|
|
else
|
948 |
|
|
f_break_seq <= 0;
|
949 |
|
|
|
950 |
|
|
always @(posedge i_clk)
|
951 |
|
|
if (f_break_seq[0])
|
952 |
|
|
assert(baud_counter == { $past(fsv_setup[23:0]), 4'h0 });
|
953 |
|
|
always @(posedge i_clk)
|
954 |
|
|
if ((f_past_valid)&&($past(f_break_seq[1]))&&(state != TXU_BREAK))
|
955 |
|
|
begin
|
956 |
|
|
assert(state == TXU_IDLE);
|
957 |
|
|
assert(o_uart_tx == 1'b1);
|
958 |
|
|
end
|
959 |
|
|
|
960 |
|
|
always @(*)
|
961 |
|
|
if (|f_break_seq)
|
962 |
|
|
begin
|
963 |
|
|
assert(state == TXU_BREAK);
|
964 |
|
|
assert(r_busy);
|
965 |
|
|
assert(o_uart_tx == 1'b0);
|
966 |
|
|
end
|
967 |
|
|
|
968 |
|
|
//////////////////////////////////////////////////////////////////////
|
969 |
|
|
//
|
970 |
|
|
// Properties for use during induction if we are made a submodule of
|
971 |
|
|
// the rxuart
|
972 |
|
|
//
|
973 |
|
|
//////////////////////////////////////////////////////////////////////
|
974 |
|
|
|
975 |
|
|
// Need enough bits for reset (24+4) plus enough bits for all of the
|
976 |
|
|
// various characters, 24+4, so 24+5 is a minimum of this counter
|
977 |
|
|
//
|
978 |
|
|
`ifndef TXUART
|
979 |
|
|
reg [28:0] f_counter;
|
980 |
|
|
initial f_counter = 0;
|
981 |
|
|
always @(posedge i_clk)
|
982 |
|
|
if (!o_busy)
|
983 |
|
|
f_counter <= 1'b0;
|
984 |
|
|
else
|
985 |
|
|
f_counter <= f_counter + 1'b1;
|
986 |
|
|
|
987 |
|
|
always @(*)
|
988 |
|
|
if (f_five_seq[0]|f_six_seq[0]|f_seven_seq[0]|f_eight_seq[0])
|
989 |
|
|
assert(f_counter == (fsv_setup[23:0] - baud_counter - 1));
|
990 |
|
|
else if (f_five_seq[1]|f_six_seq[1]|f_seven_seq[1]|f_eight_seq[1])
|
991 |
|
|
assert(f_counter == ({4'h0, fsv_setup[23:0], 1'b0} - baud_counter - 1));
|
992 |
|
|
else if (f_five_seq[2]|f_six_seq[2]|f_seven_seq[2]|f_eight_seq[2])
|
993 |
|
|
assert(f_counter == ({4'h0, fsv_setup[23:0], 1'b0}
|
994 |
|
|
+{5'h0, fsv_setup[23:0]}
|
995 |
|
|
- baud_counter - 1));
|
996 |
|
|
else if (f_five_seq[3]|f_six_seq[3]|f_seven_seq[3]|f_eight_seq[3])
|
997 |
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
998 |
|
|
- baud_counter - 1));
|
999 |
|
|
else if (f_five_seq[4]|f_six_seq[4]|f_seven_seq[4]|f_eight_seq[4])
|
1000 |
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
1001 |
|
|
+{5'h0, fsv_setup[23:0]}
|
1002 |
|
|
- baud_counter - 1));
|
1003 |
|
|
else if (f_five_seq[5]|f_six_seq[5]|f_seven_seq[5]|f_eight_seq[5])
|
1004 |
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
1005 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1006 |
|
|
- baud_counter - 1));
|
1007 |
|
|
else if (f_six_seq[6]|f_seven_seq[6]|f_eight_seq[6])
|
1008 |
|
|
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
1009 |
|
|
+{5'h0, fsv_setup[23:0]}
|
1010 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1011 |
|
|
- baud_counter - 1));
|
1012 |
|
|
else if (f_seven_seq[7]|f_eight_seq[7])
|
1013 |
|
|
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 8
|
1014 |
|
|
- baud_counter - 1));
|
1015 |
|
|
else if (f_eight_seq[8])
|
1016 |
|
|
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 9
|
1017 |
|
|
+{5'h0, fsv_setup[23:0]}
|
1018 |
|
|
- baud_counter - 1));
|
1019 |
|
|
else if (f_stop_seq[0] || (!use_parity && f_stop_seq[1]))
|
1020 |
|
|
begin
|
1021 |
|
|
// Parity bit, or first of two stop bits
|
1022 |
|
|
case(data_bits)
|
1023 |
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1024 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
1025 |
|
|
- baud_counter - 1));
|
1026 |
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1027 |
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
1028 |
|
|
- baud_counter - 1));
|
1029 |
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1030 |
|
|
- baud_counter - 1)); // 8
|
1031 |
|
|
2'b11: assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
1032 |
|
|
+{5'h0, fsv_setup[23:0]} // 7
|
1033 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1034 |
|
|
- baud_counter - 1));
|
1035 |
|
|
endcase
|
1036 |
|
|
end else if (!use_parity && !dblstop && f_stop_seq[2])
|
1037 |
|
|
begin
|
1038 |
|
|
// No parity, single stop bit
|
1039 |
|
|
// Different from the one above, since the last counter is has
|
1040 |
|
|
// one fewer items within it
|
1041 |
|
|
case(data_bits)
|
1042 |
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1043 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
1044 |
|
|
- baud_counter - 2));
|
1045 |
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1046 |
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
1047 |
|
|
- baud_counter - 2));
|
1048 |
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1049 |
|
|
- baud_counter - 2)); // 8
|
1050 |
|
|
2'b11: assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0}
|
1051 |
|
|
+{5'h0, fsv_setup[23:0]} // 7
|
1052 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1053 |
|
|
- baud_counter - 2));
|
1054 |
|
|
endcase
|
1055 |
|
|
end else if (f_stop_seq[1])
|
1056 |
|
|
begin
|
1057 |
|
|
// Parity and the first of two stop bits
|
1058 |
|
|
assert(dblstop && use_parity);
|
1059 |
|
|
case(data_bits)
|
1060 |
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1061 |
|
|
+{5'h0, fsv_setup[23:0]} // 11
|
1062 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1063 |
|
|
- baud_counter - 1));
|
1064 |
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1065 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
1066 |
|
|
- baud_counter - 1));
|
1067 |
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1068 |
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
1069 |
|
|
- baud_counter - 1));
|
1070 |
|
|
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1071 |
|
|
- baud_counter - 1)); // 8
|
1072 |
|
|
endcase
|
1073 |
|
|
end else if ((dblstop ^ use_parity) && f_stop_seq[2])
|
1074 |
|
|
begin
|
1075 |
|
|
// Parity and one stop bit
|
1076 |
|
|
// assert(!dblstop && use_parity);
|
1077 |
|
|
case(data_bits)
|
1078 |
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1079 |
|
|
+{5'h0, fsv_setup[23:0]} // 11
|
1080 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1081 |
|
|
- baud_counter - 2));
|
1082 |
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1083 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
1084 |
|
|
- baud_counter - 2));
|
1085 |
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1086 |
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
1087 |
|
|
- baud_counter - 2));
|
1088 |
|
|
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1089 |
|
|
- baud_counter - 2)); // 8
|
1090 |
|
|
endcase
|
1091 |
|
|
end else if (f_stop_seq[2])
|
1092 |
|
|
begin
|
1093 |
|
|
assert(dblstop);
|
1094 |
|
|
assert(use_parity);
|
1095 |
|
|
// Parity and two stop bits
|
1096 |
|
|
case(data_bits)
|
1097 |
|
|
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1098 |
|
|
+{3'h0, fsv_setup[23:0], 2'b00} // 12
|
1099 |
|
|
- baud_counter - 2));
|
1100 |
|
|
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1101 |
|
|
+{5'h0, fsv_setup[23:0]} // 11
|
1102 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0}
|
1103 |
|
|
- baud_counter - 2));
|
1104 |
|
|
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1105 |
|
|
+{4'h0, fsv_setup[23:0], 1'b0} // 10
|
1106 |
|
|
- baud_counter - 2));
|
1107 |
|
|
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0}
|
1108 |
|
|
+{5'h0, fsv_setup[23:0]} // 9
|
1109 |
|
|
- baud_counter - 2));
|
1110 |
|
|
endcase
|
1111 |
|
|
end
|
1112 |
|
|
`endif
|
1113 |
|
|
|
1114 |
|
|
//////////////////////////////////////////////////////////////////////
|
1115 |
|
|
//
|
1116 |
|
|
// Other properties, not necessarily associated with any sequences
|
1117 |
|
|
//
|
1118 |
|
|
//////////////////////////////////////////////////////////////////////
|
1119 |
|
|
always @(*)
|
1120 |
|
|
assert((state < 4'hb)||(state >= 4'he));
|
1121 |
|
|
//////////////////////////////////////////////////////////////////////
|
1122 |
|
|
//
|
1123 |
|
|
// Careless/limiting assumption section
|
1124 |
|
|
//
|
1125 |
|
|
//////////////////////////////////////////////////////////////////////
|
1126 |
|
|
always @(*)
|
1127 |
|
|
assume(i_setup[23:0] > 2);
|
1128 |
|
|
always @(*)
|
1129 |
|
|
assert(fsv_setup[23:0] > 2);
|
1130 |
|
|
|
1131 |
23 |
dgisselq |
`endif // FORMAL
|
1132 |
2 |
dgisselq |
endmodule
|
1133 |
|
|
|